Обозначение Саппса–Леммона

Нотация Суппса–Леммона ^[1] — это естественная дедуктивная логическая система обозначений, разработанная Э. Дж. Леммоном . ^[2] Производная от метода Суппса , ^[3] она представляет доказательства естественной дедукции как последовательности обоснованных шагов. Оба метода используют правила вывода, полученные из системы естественной дедукции Генцена 1934/1935 годов, ^[4] в которой доказательства были представлены в виде древовидной диаграммы, а не в табличной форме Суппса и Леммона. Хотя схема древовидной диаграммы имеет преимущества для философских и образовательных целей, табличная схема гораздо удобнее для практических приложений.

Похожая табличная структура представлена ​​Клини. ^[5] Главное отличие заключается в том, что Клини не сокращает левые части утверждений до номеров строк, предпочитая вместо этого либо давать полные списки прецедентных предложений, либо альтернативно указывать левые части чертами, идущими вниз по левой стороне таблицы, чтобы обозначить зависимости. Однако версия Клини имеет то преимущество, что она представлена, хотя и очень схематично, в строгой структуре метаматематической теории, тогда как книги Суппеса ^[3] и Леммона ^[2] являются приложениями табличной структуры для обучения вводной логике.

Описание дедуктивной системы

Нотация Суппеса–Леммона представляет собой нотацию для исчисления предикатов с равенством, поэтому ее описание можно разделить на две части: общий синтаксис доказательства и контекстно-зависимые правила .

Синтаксис общего доказательства

Доказательство представляет собой таблицу с 4 столбцами и неограниченным количеством упорядоченных строк. Слева направо столбцы содержат:

1. Набор положительных целых чисел, возможно пустой
2. Положительное целое число
3. Правильно сформированная формула ( или wff)
4. Набор чисел, возможно пустой; правило; и, возможно, ссылка на другое доказательство

Ниже приведен пример:

Во втором столбце содержатся номера строк. В третьем столбце содержится wff, который обосновывается правилом, содержащимся в четвертом, вместе со вспомогательной информацией о других wff, возможно, в других доказательствах. В первом столбце представлены номера строк предположений, на которых основывается wff, определяемые применением цитируемого правила в контексте. Любая строка любого допустимого доказательства может быть преобразована в секвенцию путем перечисления wff в цитируемых строках в качестве посылок, а wff в строке в качестве заключения. Аналогично их можно преобразовать в условные предложения, где антецедентом является конъюнкция. Эти секвенции часто перечисляются над доказательством, как Modus Tollens выше.

Правила исчисления предикатов с равенством

Приведенное выше доказательство является допустимым, но доказательства не обязательно должны соответствовать общему синтаксису системы доказательств. Однако, чтобы гарантировать допустимость секвенции, мы должны соответствовать тщательно определенным правилам. Правила можно разделить на четыре группы: пропозициональные правила (1-10), предикатные правила (11-14), правила равенства (15-16) и правило подстановки ( 17). Добавление этих групп по порядку позволяет построить пропозициональное исчисление, затем предикатное исчисление, затем предикатное исчисление с равенством, затем предикатное исчисление с равенством, что позволяет выводить новые правила. Некоторые из правил пропозиционального исчисления, такие как MTT, являются избыточными и могут быть выведены как правила из других правил.

1. Правило предположения (A): "A" оправдывает любой wff. Единственное предположение - это его собственный номер строки.
2. Modus Ponendo Ponens (MPP): Если в доказательстве ранее встречались строки a и b, содержащие P → Q и P соответственно, то « a , b MPP» оправдывает Q. Предположения представляют собой коллективный набор строк a и b .
3. Правило условного доказательства (CP): Если строка a с предложением P имеет предположение строки b с предложением Q, то « b , a CP» оправдывает Q→P. Все предположения a, кроме b , сохраняются.
4. Правило двойного отрицания (DN): " a DN" оправдывает добавление или вычитание двух символов отрицания из wff в строке a ранее в доказательстве, делая это правило двуусловным. Пул предположений - один из цитируемой строки.
5. Правило ∧-введения (∧I): Если предложения P и Q находятся на строках a и b , « a , b ∧I» оправдывает P ∧ Q. Предположения представляют собой коллективный пул соединенных предложений.
6. Правило ∧-элиминации (∧E): Если строка a является конъюнкцией P∧Q, можно заключить либо P, либо Q, используя « a ∧E». Предположения являются предположениями строки a . ∧I и ∧E допускают монотонность вывода , так как когда предложение P соединяется с Q с помощью ∧I и разделяется с помощью ∧E, оно сохраняет предположения Q.
7. Правило ∨-введения (∨I): Для строки a с предложением P можно ввести P∨Q, ссылаясь на « a ∨I». Предположениями являются a 's.
8. Правило ∨-устранения (∨E): Для дизъюнкции P∨Q, если предположить P и Q и по отдельности прийти к выводу R из каждого, то можно заключить R. Правило записывается как « a , b , c , d , e∨E », где строка a имеет начальную дизъюнкцию P∨Q, строки b и d предполагают P и Q соответственно, а строки c и e заключают R с P и Q в их соответствующих пулах предположений. Предположения представляют собой коллективные пулы двух строк, заключающих R, c и e , за вычетом строк, предполагающих P и Q, b и d .
9. Reductio Ad Absurdum (RAA): Для предложения P∧¬P в строке a, ссылающегося на предположение Q в строке b , можно сослаться на « b , a RAA» и вывести ¬Q из предположений строки a помимо b .
10. Modus Tollens (MTT): Для предложений P→Q и ¬Q на строках a и b можно сослаться на " a , b MTT", чтобы вывести ¬P. Предположения те же, что и в строках a и b . Это доказывается другими правилами выше.
11. Универсальное введение (UI): Для предиката в строке a можно сослаться на « UI », чтобы оправдать универсальную квантификацию, при условии, что ни одно из предположений в строке a не содержит термина нигде. Предположения те же, что и в строке a . ${\displaystyle Ra}$ ${\displaystyle (\forall x)Rx}$ ${\displaystyle a}$
12. Универсальное исключение (UE): Для универсально квантифицированного предиката в строке a можно сослаться на « UE » для обоснования . Предположения те же, что и в строке a . UE является дуальностью с UI в том смысле, что можно переключаться между квантифицированными и свободными переменными, используя эти правила. ${\displaystyle (\forall x)Rx}$ ${\displaystyle Ra}$
13. Экзистенциальное введение (ЭВ): Для предиката в строке а можно сослаться на « ЭВ », чтобы обосновать экзистенциальную квантификацию. Предположения те же, что и в строке а . ${\displaystyle Ra}$ ${\displaystyle (\exists x)Rx}$
14. Экзистенциальное исключение (EE): Для экзистенциально квантифицированного предиката в строке a , если мы предполагаем , что он истинен в строке b и выводим P из него в строке c , мы можем сослаться на « a , b , c EE» для обоснования P. Термин не может появляться в заключении P, любом из его предположений, кроме строки b , или в строке a . По этой причине EE и EI находятся в дуальности, поскольку можно предположить и использовать EI, чтобы прийти к заключению из , поскольку EI избавит заключение от термина . Предположениями являются предположения в строке a и любые предположения в строке c, кроме b . ${\displaystyle (\exists x)Rx}$ ${\displaystyle Ra}$ ${\displaystyle a}$ ${\displaystyle Ra}$ ${\displaystyle (\exists x)Rx}$ ${\displaystyle a}$
15. Введение равенства (=I): В любой момент можно ввести цитирование «=I» без каких-либо предположений. ${\displaystyle a=a}$
16. Устранение равенства (=E): Для предложений и P в строках a и b можно сослаться на " a , b =E", чтобы оправдать замену любых терминов в P на . Предположениями являются пул строк a и b . ${\displaystyle a=b}$ ${\displaystyle a}$ ${\displaystyle b}$
17. Подстановочный экземпляр (SI(S)): Для секвенции, доказанной в доказательстве X, и подстановочных экземпляров и в строках a и b можно сослаться на " a , b SI(S) X", чтобы оправдать введение подстановочного экземпляра . Предположения те же, что и в строках a и b . Производное правило без предположений является теоремой и может быть введено в любое время без предположений. Некоторые ссылаются на это как на "TI(S)", вместо "теоремы" вместо "секвенции". Кроме того, некоторые ссылаются только на "SI" или "TI" в любом случае, когда подстановочный экземпляр не нужен, поскольку их предложения точно соответствуют предложениям указанного доказательства. ${\displaystyle P,Q\vdash R}$ ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle R}$

Примеры

Пример доказательства секвенции (в данном случае теоремы):

Доказательство принципа взрыва с использованием монотонности вывода. Некоторые называют следующую технику, продемонстрированную в строках 3-6, Правилом (конечного) увеличения посылок: ^[6]

Пример подстановки и ∨E:

История табличных систем натурального вычета

Историческое развитие табличных систем естественного вывода, основанных на правилах и указывающих предшествующие суждения номерами строк (и связанными с ними методами, такими как вертикальные черты или звездочки), включает следующие публикации.

• 1940: В учебнике Куайн ^[7] обозначил предшествующие зависимости номерами строк в квадратных скобках, предвосхитив обозначение номеров строк Саппса 1957 года.
• 1950: В учебнике Куайн (1982, стр. 241–255) продемонстрировал метод использования одной или нескольких звездочек слева от каждой строки доказательства для обозначения зависимостей. Это эквивалентно вертикальным чертам Клини. (Не совсем ясно, появилась ли звездочка Куайна в оригинальном издании 1950 года или была добавлена ​​в более позднем издании.)
• 1957: Введение в доказательство теорем практической логики в учебнике Суппеса (1999, стр. 25–150). В нем зависимости (т. е. предшествующие предложения) обозначались номерами строк слева от каждой строки.
• 1963: Столл (1979, стр. 183–190, 215–219) использует наборы номеров строк для указания предшествующих зависимостей строк последовательных логических аргументов, основанных на правилах вывода естественной дедукции.
• 1965: Весь учебник Леммона (1965) представляет собой введение в логические доказательства с использованием метода, основанного на методе Саппса.
• 1967: В учебнике Клини (2002, стр. 50–58, 128–130) кратко продемонстрировал два вида практических логических доказательств: одна система использует явные цитаты предшествующих предложений слева от каждой строки, другая система использует вертикальные линии слева для обозначения зависимостей. ^[8]

Смотрите также

• Натуральный вычет
• Последовательное исчисление
• Дедуктивные системы

Примечания

1. Пеллетье, Фрэнсис Джеффри; Хазен, Аллен (2024), Залта, Эдвард Н.; Нодельман, Ури (ред.), «Естественные системы дедукции в логике», Стэнфордская энциклопедия философии (весеннее издание 2024 г.), Исследовательская лаборатория метафизики, Стэнфордский университет , дата обращения 01.05.2024
2. См. Lemmon 1965 для вводного представления системы естественной дедукции Леммона.
3. См. Suppes 1999, стр. 25–150, для вводного представления системы естественной дедукции Suppes.
4. Генцен 1934, Генцен 1935.
5. Клини 2002, стр. 50–56, 128–130.
6. Коберн, Барри; Миллер, Дэвид (октябрь 1977 г.). «Два комментария к «Начальной логике» Леммона». Notre Dame Journal of Formal Logic . 18 (4): 607–610. doi : 10.1305/ndjfl/1093888128 . ISSN  0029-4527.
7. Куайн (1981). См., в частности, страницы 91–93 для обозначения номеров строк Куайна для зависимостей антецедентов.
8. Особое преимущество табличных систем естественной дедукции Клини заключается в том, что он доказывает справедливость правил вывода как для исчисления высказываний, так и для исчисления предикатов. См. Kleene 2002, стр. 44–45, 118–119.

Ссылки

• Генцен, Герхард Карл Эрих (1934). «Untersuchungen über das logische Schließen. I». Mathematische Zeitschrift . 39 (2): 176–210. дои : 10.1007/BF01201353. (Английский перевод Исследования логической дедукции в Сабо.)
• Генцен, Герхард Карл Эрих (1935). «Untersuchungen über das logische Schließen. II». Mathematische Zeitschrift . 39 (3): 405–431. дои : 10.1007/bf01201363.
• Клини, Стивен Коул (2002) [1967]. Математическая логика . Минеола, Нью-Йорк: Dover Publications. ISBN 978-0-486-42533-7.
• Леммон, Эдвард Джон (1965). Начало логики . Томас Нельсон. ISBN 0-17-712040-1.
• Куайн, Уиллард Ван Орман (1981) [1940]. Математическая логика (пересмотренное издание). Кембридж, Массачусетс: Издательство Гарвардского университета. ISBN 978-0-674-55451-1.
• Куайн, Уиллард Ван Орман (1982) [1950]. Методы логики (Четвертое изд.). Кембридж, Массачусетс: Издательство Гарвардского университета. ISBN 978-0-674-57176-1.
• Столл, Роберт Рот (1979) [1963]. Теория множеств и логика . Минеола, Нью-Йорк: Dover Publications. ISBN 978-0-486-63829-4.
• Suppes, Patrick Colonel (1999) [1957]. Введение в логику . Минеола, Нью-Йорк: Dover Publications. ISBN 978-0-486-40687-9.
• Сабо, М. Э. (1969). Собрание статей Герхарда Генцена . Амстердам: Северная Голландия.

Внешние ссылки

• Пеллетье, Джефф, «История естественной дедукции и учебники по элементарной логике».