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

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

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

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

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

Общий

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

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

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

p → q , ¬ q ⊢ ¬ p [Метод удаления (MTT)]
Успенский номер	Номер строки	Формула ( вфф )	Используемые линии и обоснование
1	(1)	п → д	А
2	(2)	¬ q	А
3	(3)	п	А (для РАА)
1, 3	(4)	д	1, 3, МПП
1, 2, 3	(5)	д ∧ ¬ д	2, 4, ∧I
1, 2	(6)	¬ p	3, 5, РАА
КЭД

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

Правила исчисления

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

1. Правило предположения (А): «А» оправдывает любые ошибки. Единственное предположение — это собственный номер строки.
2. Modus Ponendo Ponens (MPP): если ранее в доказательстве были строки a и b, содержащие P→Q и P соответственно, «a,b MPP» оправдывает Q. Допущения представляют собой коллективный пул строк a и b.
3. Правило условного доказательства (CP): если строка с предложением P имеет строку предположения b с предложением Q, «b,a CP» оправдывает Q→P. Все предположения a, за исключением b, сохраняются.
4. Правило двойного отрицания (DN): «DN» оправдывает добавление или вычитание двух символов отрицания из wff в строке a ранее в доказательстве, что делает это правило двуусловным. Пул предположений соответствует указанной строке.
5. Правило ∧-введения (∧I): если предложения P и Q находятся в строках a и b, «a,b ∧I» оправдывает P∧Q. Предположения представляют собой совокупность соединенных предложений.
6. Правило ∧-исключения (∧E): если линия a представляет собой союз P∧Q, можно заключить либо P, либо Q, используя «a ∧E». Допущения представляют собой линию А. ∧I и ∧E допускают монотонность следствия , поскольку, когда предложение P соединяется с Q с помощью ∧I и разделяется с помощью ∧E, оно сохраняет предположения Q.
7. Правило ∨-введения (∨I): Для строки a с предложением P можно ввести P∨Q со ссылкой на «a ∨I». Предположения являются пятерками.
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, за вычетом линий 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): для предиката $Ra$ в строке а можно указать «пользовательский интерфейс», чтобы оправдать универсальную количественную оценку, $(\forall x)Rx$, при условии, что ни одно из допущений в строке a не имеет члена $a$ где угодно. Допущения соответствуют строке a.
12. Универсальное устранение (UE): для универсального количественного предиката. $(\forall x)Rx$ в строке а можно указать «UE», чтобы оправдать $Ra$. Допущения соответствуют строке a. UE представляет собой двойственность пользовательского интерфейса в том смысле, что с помощью этих правил можно переключаться между количественными и свободными переменными.
13. Экзистенциальное введение (ЭИ): для предиката $Ra$ онлайн можно ссылаться на «ЭИ», чтобы оправдать экзистенциальную количественную оценку, $(\exists x)Rx$. Допущения соответствуют строке a.
14. Экзистенциальное устранение (EE): для экзистенциально квантифицированного предиката. $(\exists x)Rx$ в строке а, если предположить $Ra$ Чтобы быть истинным в строке b и вывести P с его помощью в строке c, мы можем процитировать «a,b,c EE», чтобы оправдать P. Термин $a$ не может появиться в заключении P, ни в одном из его предположений, кроме строки b или строки a. По этой причине EE и EI находятся в двойственности, как можно предположить. $Ra$ и использовать EI, чтобы прийти к выводу из $(\exists x)Rx$, так как EI избавит от заключения срока $a$. Допущения — это предположения в строке a и любые предположения в строке c, кроме b.
15. Введение равенства (=I): в любой момент можно ввести $a=a$ цитируя «=I» без каких-либо предположений.
16. Устранение равенства (=E): Для предложений $a=b$ и P в строках a и b, можно указать «a,b =E», чтобы оправдать изменение любых терминов. $a$ термины от P до $b$. Предположения представляют собой совокупность a и b.
17. Экземпляр замены (SI(S)): для последующего $P,Q\vdash R$ доказано в доказательстве X и примерах замены $P$ и $Q$ в строках a и b можно указать «a,b SI(S) X», чтобы оправдать введение экземпляра замены $R$. Допущения аналогичны строкам a и b. Производное правило без каких-либо предположений является теоремой и может быть введено в любое время без каких-либо предположений. Некоторые называют это «TI (S)», что означает «теорема» вместо «секвенция». Кроме того, некоторые ссылаются только на «SI» или «TI» в любом случае, когда пример замены не нужен, поскольку их предложения точно соответствуют предложениям упомянутого доказательства.

Примеры

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

⊢ p ∨ ¬ p
Успенский номер	Номер строки	Формула ( вфф )	Используемые линии и обоснование
1	(1)	¬( п ∨ ¬ п )	А (для РАА)
2	(2)	п	А (для РАА)
2	(3)	( п ∨ ¬ п )	2, ∨I
1, 2	(4)	( п ∨ ¬ п ) ∧ ¬( п ∨ ¬ п )	3, 1, ∧I
1	(5)	¬ p	2, 4, РАА
1	(6)	( п ∨ ¬ п )	5, ∨I
1	(7)	( п ∨ ¬ п ) ∧ ¬( п ∨ ¬ п )	1, 6, ∧I
	(8)	¬¬( п ∨ ¬ п )	1, 7, РАА
	(9)	( п ∨ ¬ п )	8, ДН
КЭД

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

п , ¬ п ⊢ q
Успенский номер	Номер строки	Формула ( вфф )	Используемые линии и обоснование
1	(1)	п	А (для РАА)
2	(2)	¬ p	А (для РАА)
1, 2	(3)	п ∧ ¬ р	1, 2, ∧I
4	(4)	¬ q	А (для DN)
1, 2, 4	(5)	( п ∧ ¬ п ) ∧ ¬ q	3, 4, ∧I
1, 2, 4	(6)	п ∧ ¬ р	5, ∨E
1, 2	(7)	¬¬ q	4, 6, РАА
1, 2	(8)	д	7, ДН
КЭД

Пример замены и ∨E:

( п ∧ ¬ п ) ∨ ( q ∧ ¬ q ) ⊢ р
Успенский номер	Номер строки	Формула ( вфф )	Используемые линии и обоснование
1	(1)	( п ∧ ¬ п ) ∨ ( q ∧ ¬ q )	А
2	(2)	п ∧ ¬ р	А (для ∨E)
2	(3)	п	2 ∧E
2	(4)	¬ p	2 ∧E
2	(5)	р	3, 4 SI(S) см. доказательство выше
6	(6)	д ∧ ¬ д	А (для ∨E)
6	(7)	д	6 ∧E
6	(8)	¬ q	2 ∧E
6	(9)	р	7, 8 SI(S) см. доказательство выше
1	(10)	р	1, 2, 5, 6, 9, ∨E
КЭД

История табличных

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

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

См. также

• Естественный вычет
• Секвенционное исчисление
• Дедуктивные системы

Ссылки

• Генцен, Герхард Карл Эрих (1934). «Исследования по логическим рассуждениям. I» . Математический журнал . 39 (2): 176–210. дои : 10.1007/BF01201353 . (Английский перевод «Исследования логической дедукции в Сабо».)
• Генцен, Герхард Карл Эрих (1935). «Исследования по логическим рассуждениям. II» . Математический журнал . 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 .
• Суппес, Патрик Полковник (1999) [1957]. Введение в логику . Минеола, Нью-Йорк: Dover Publications. ISBN  978-0-486-40687-9 .
• Сабо, Мэн (1969). Сборник статей Герхарда Генцена . Амстердам: Северная Голландия.

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

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