Различные представления естественной дедукции
Древовидные представления
Выписных аннотаций Генцена, используемых для интернализации гипотетических суждений, можно избежать, представив доказательства в виде дерева последовательностей Γ ⊢ A вместо дерева истинных суждений.
Последовательные представления
Представления Ясковски о естественной дедукции привели к различным обозначениям, таким как исчисление в стиле Фитча (или диаграммы Фитча) или метод Суппеса , вариант которого Леммон предложил под названием system L . Такие системы представления, которые более точно описываются как табличные, включают следующее.
- 1940: В учебнике Куайн [9] указал предшествующие зависимости номерами строк в квадратных скобках, предвосхищая обозначение номеров строк Суппса 1957 года.
- 1950: В учебнике Куайн (1982 , стр. 241-255) продемонстрировал метод использования одной или нескольких звездочек слева от каждой строки доказательства для обозначения зависимостей. Это эквивалентно вертикальным полосам Клини. (Не совсем ясно, появилось ли обозначение звездочкой Куайна в оригинальном издании 1950 года или было добавлено в более позднем издании.)
- 1957: Введение в доказательство теоремы практической логики в учебнике Суппеса (1999 , стр. 25-150). Здесь зависимости (т.е. предшествующие предложения) обозначены номерами строк слева от каждой строки.
- 1963: Столл (1979 , стр. 183-190, 215-219) использует наборы номеров строк для указания предшествующих зависимостей строк последовательных логических аргументов, основанных на правилах вывода методом естественной дедукции.
- 1965: Весь учебник Леммона (1965) представляет собой введение в логические доказательства с использованием метода, основанного на методе Suppes .
- 1967: В учебнике Клини (2002 , стр. 50-58, 128-130) кратко продемонстрировал два вида практических логических доказательств: одна система использует явные цитаты предшествующих предложений слева от каждой строки, другая система использует вертикальные штриховые линии слева для обозначения зависимостей. [10]
Доказательства и теория типов
До сих пор изложение естественной дедукции было сосредоточено на природе утверждений, не давая формального определения доказательства. Чтобы формализовать понятие доказательства, мы немного изменим представление гипотетических выводов. Мы помечаем антецеденты доказательными переменными (из некоторого счетного множества V переменных) и украшаем последовательность фактическим доказательством. Предшествующие события или гипотезы отделены от последующих с помощью турникета ( ⊢ ). Эта модификация иногда называется локализованными гипотезами. Следующая диаграмма суммирует изменения.
| ──── u1 ──── u2 ... ──── un J1 J2 Jn ⋮ J | ⇒ | u1:J1, u2:J2, ..., un:Jn ⊢ J |
Набор гипотез будет записан как Γ , когда их точный состав не имеет значения. Чтобы сделать доказательства явными, мы переходим от бездоказательного суждения "Истинно" к суждению: " π является доказательством ( A true ) ", которое символически записывается как " π : A true ". Следуя стандартному подходу, доказательства задаются своими собственными правилами формирования суждения "доказательство". Простейшим возможным доказательством является использование помеченной гипотезы; в данном случае доказательством является сам ярлык.
| u ∈ V ─────── доказательство- F u доказательство | ───────────────────── hyp u: Истинно ⊢ u: истинно |
Для краткости мы оставим оценочный ярлык true в остальной части этой статьи, то есть, напишем " Γ ⊢ π : A ". Давайте повторно рассмотрим некоторые из связок с явными доказательствами. Что касается конъюнкции, мы смотрим на вводное правило ∧ I , чтобы определить форму доказательств конъюнкции : они должны быть парой доказательств двух конъюнктов. Таким образом:
| 1 доказательство 2 доказательства ──────────────────── пара- F ( π 1 , 2) доказательство | Γ ⊢ π 1 : A Γ ⊢ π 2 : B ───────────────────────── ∧ Я Γ ⊢ ( π 1 , π 2 ) : A ∧ B |