В теории доказательств - дисциплина в математической логике , перевод двойного отрицания , иногда называемый отрицательным переводом , - это общий подход для встраивания классической логики в интуиционистскую логику , обычно путем перевода формул в формулы, которые классически эквивалентны, но интуиционистски не эквивалентны. Особые случаи двойного отрицания перевода включают в себя перевод Гливенко в для пропозициональной логики , и перевод Геделя-Генцен и перевод Курода для логики первого порядка .
Логика высказываний [ править ]
Самый простой для описания перевод двойного отрицания исходит из теоремы Гливенко , доказанной Валерием Гливенко в 1929 году. Она отображает каждую классическую формулу φ в ее двойное отрицание ¬¬φ.
Теорема Гливенко утверждает:
- Если φ - пропозициональная формула, то φ - классическая тавтология тогда и только тогда, когда ¬¬φ - интуиционистская тавтология.
Из теоремы Гливенко следует более общее утверждение:
- Если T - множество пропозициональных формул, а φ - пропозициональная формула, то T ⊢ φ в классической логике тогда и только тогда, когда T ⊢ ¬¬φ в интуиционистской логике.
В частности, набор пропозициональных формул интуиционистски непротиворечив тогда и только тогда, когда он классически выполним.
Логика первого порядка [ править ]
Перевод Гёделя – Гентцена (названный в честь Курта Гёделя и Герхарда Гентцена ) связывает с каждой формулой φ в языке первого порядка другую формулу φ N , которая определяется индуктивно:
- Если φ атомный, то φ N является ¬¬φ
- (φ ∧ θ) N - это φ N ∧ θ N
- (φ ∨ θ) N есть ¬ (¬φ N ∧ ¬θ N )
- (φ → θ) N - это φ N → θ N
- (¬φ) N равно ¬φ N
- (∀ x φ) N равно ∀ x φ N
- (∃ x φ) N равно ¬∀ x ¬φ N
Этот перенос обладает тем свойством, что φ N классически эквивалентен φ. Фундаментальная теорема о надежности (Авигад и Феферман, 1998 г., стр. 342; Басс, 1998 г., стр. 66) гласит:
- Если T - набор аксиом, а φ - формула, то T доказывает φ, используя классическую логику, тогда и только тогда, когда T N доказывает φ N, используя интуиционистскую логику.
Здесь Т Н состоит из двойного отрицания переводов формул Т .
Предложение φ не может подразумевать его отрицательный перевод φ N в интуиционистской логике первого порядка. Трельстра и ван Дален (1988, гл. 2, раздел 3) дают описание (принадлежащее Лейванту) формул, из которых следует их перевод Гёделя – Генцена.
Варианты [ править ]
Есть несколько альтернативных определений отрицательного перевода. Все они доказуемо эквивалентны в интуиционистской логике, но могут быть проще применимы в определенных контекстах.
Одна из возможностей - изменить предложения дизъюнкции и экзистенциального квантора на
- (φ ∨ θ) N есть ¬¬ (φ N ∨ θ N )
- (∃ x φ) N равно ¬¬∃ x φ N
Тогда перевод можно кратко описать как: префикс ¬¬ для каждой атомарной формулы, дизъюнкции и экзистенциального квантора.
Другая возможность (известная как перевод Куроды ) состоит в том, чтобы построить φ N из φ, поместив ¬¬ перед всей формулой и после каждого универсального квантора . Обратите внимание, что это сводится к простому переводу ¬¬φ, если φ пропозициональный.
Также возможно определить φ N , добавив префикс ¬¬ перед каждой подформулой φ, как это сделал Колмогоров . Такой перевод является логическим аналогом вызова по имени продолжения обходя стиль перевод функциональных языков программирования вдоль линий переписки Карри-Говарда между доказательствами и программами.
Результаты [ править ]
Перевод двойного отрицания был использован Геделем (1933) для изучения взаимосвязи между классической и интуиционистской теориями натуральных чисел («арифметикой»). Он получает следующий результат:
- Если формула φ выводима из аксиом арифметики Пеано, то φ N выводима из аксиом арифметики Гейтинга .
Этот результат показывает, что если арифметика Гейтинга непротиворечива, то последовательна и арифметика Пеано. Это связано с тем, что противоречащая формула θ ∧ ¬θ интерпретируется как θ N ∧ ¬θ N , что по-прежнему противоречиво. Более того, доказательство связи является полностью конструктивным, позволяя преобразовать доказательство θ ∧ ¬θ в арифметике Пеано в доказательство θ N ∧ ¬θ N в арифметике Гейтинга. (Комбинируя перевод двойного отрицания с переводом Фридмана , на самом деле можно доказать, что арифметика Пеано Π 0 2 - консервативна по сравнению с арифметикой Гейтинга.)
Пропозициональное отображение φ в ¬¬φ не распространяется на звуковой перевод логики первого порядка, потому что ∀ x ¬¬φ ( x ) → ¬¬∀ x φ ( x ) не является теоремой интуиционистской логики предикатов. Это объясняет, почему в случае первого порядка φ N нужно определять более сложным образом.
См. Также [ править ]
Ссылки [ править ]
- Дж. Авигад и С. Феферман (1998), «Функциональная (« Диалектическая ») интерпретация Гёделя», Справочник по теории доказательств » , изд. С. Бусс, Elsevier. ISBN 0-444-89840-9
- С. Бусс (1998), "Введение в теорию доказательства", Справочник по теории доказательств , изд. С. Бусс, Elsevier. ISBN 0-444-89840-9
- Г. Генцен (1936), «Die Widerspruchfreiheit der reinen Zahlentheorie», Mathematische Annalen , т. 112, стр. 493–565 (немецкий). Перепечатано в английском переводе как «Непротиворечивость арифметики» в Сборнике статей Герхарда Гентцена , М. Е. Сабо, изд.
- В. Гливенко (1929), Sur quelques points de la logique de M. Brouwer , Bull. Soc. Математика. Бельг. 15, 183–188
- К. Гёдель (1933), «Zur intuitionistischen Arithmetik und Zahlentheorie», Ergebnisse eines Mathematischen Kolloquiums , т. 4, стр. 34–38 (на немецком языке). Перепечатано в английском переводе как «Об интуиционистской арифметике и теории чисел» в The Undecidable , M. Davis, ed., Pp. 75–81.
- Колмогоров А.Н. (1925), «O principe tertium non datur» (русск.). Перепечатано в английском переводе как «По принципу исключенного третьего » в « От Фреге к Геделю» , van Heijenoort, ed., Pp. 414–447.
- AS Troelstra (1977), "Аспекты конструктивной математики", Справочник по математической логике " , изд. Дж. Барвайз , Северная Голландия. ISBN 0-7204-2285-X
- С. Трульстра и Д. ван Дален (1988), Конструктивизм в математике. Введение , тома 121, 123 исследований по логике и основам математики , Северная Голландия.
Внешние ссылки [ править ]
- « Интуиционистская логика », Стэнфордская философская энциклопедия.
