Классическая и модальная логики
Для простоты логика, представленная до сих пор, была интуитивистской . Классическая логика расширяет интуиционистскую логику дополнительной аксиомой или принципом исключенного среднего :
Для любого предложения p предложение p ∨ p истинно .
Очевидно, что это утверждение не является ни введением, ни устранением; на самом деле, оно включает в себя две различные связки. Оригинальная трактовка исключенного среднего Генценом предписывала одну из следующих трех (эквивалентных) формулировок, которые уже присутствовали в аналогичных формах в системах Гильберта и Хейтинга :
| ────────────── XM1 A ∨ A верно | Верно ────────── XM2 Верно | ──────u Истинный ⋮ p верно ────── XM3u, p Истинный |
( XM 3 - это просто XM 2 , выраженное в терминах E .) Такая трактовка исключенного среднего, помимо того, что она нежелательна с точки зрения пуриста, вносит дополнительные сложности в определение нормальных форм.
Сравнительно более удовлетворительная трактовка классической естественной дедукции с точки зрения одних только правил введения и исключения была впервые предложена Париго в 1992 году в форме классического лямбда-исчисления , называемого λμ . Ключевым моментом его подхода была замена суждения, ориентированного на истину, истинным, более классическим понятием, напоминающим последовательное исчисление : в локализованной форме вместо Γ ⊢ A он использовал Γ ⊢ Δ , где Δ - набор предложений , похожих на Γ . Γ рассматривалось как конъюнкция , а Δ - как дизъюнкция . Эта структура , по сути , заимствована непосредственно из классических последовательных исчислений , но нововведение в λμ заключалось в том, чтобы придать вычислительный смысл классическим доказательствам естественной дедукции в терминах callcc или механизма броска / захвата, наблюдаемого в LISP и его потомках. (Смотрите также: контроль первого класса .)
Другое важное расширение было для модальной и других логик, которым требуется нечто большее, чем просто базовое суждение об истине. Они были впервые описаны для алетических модальных логик S 4 и S 5 в стиле естественной дедукции Правицем в 1965 году [4] , и с тех пор накопилось большое количество связанных с ними работ. Чтобы привести простой пример, модальная логика S 4 требует одного нового суждения, "Действительного", которое является категоричным по отношению к истине: