Перевод двойного отрицания - Double-negation translation

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

Логика высказываний

Самый простой для описания перевод двойного отрицания исходит из теоремы Гливенко , доказанной Валерием Гливенко в 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 исследований по логике и основам математики , Северная Голландия.

внешняя ссылка