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

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

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

Самый простой для описания перевод двойного отрицания происходит от Теорема Гливенко, доказано Валерий Гливенко в 1929 году. Он отображает каждую классическую формулу φ на ее двойное отрицание ¬¬φ.

Теорема Гливенко утверждает:

Если φ - пропозициональная формула, то φ - классическая тавтология тогда и только тогда, когда ¬¬φ - интуиционистская тавтология.

Теорема Гливенко влечет более общее утверждение:

Если Т набор пропозициональных формул, Т * набор, состоящий из дважды отрицательных формул Т, а φ пропозициональная формула, то Т ⊢ φ в классической логике тогда и только тогда, когда Т * ⊢ ¬¬φ в интуиционистской логике.

В частности, набор пропозициональных формул интуиционистски непротиворечив тогда и только тогда, когда он классически выполним.

Логика первого порядка

В Перевод Гёделя – Генцена (названный в честь Курт Гёдель и Герхард Гентцен ) каждой формуле φ в языке первого порядка сопоставляет другую формулу φN, который определяется индуктивно:

  • Если φ атомный, то φN это ¬¬φ
  • (φ ∧ θ)N это φN ∧ θN
  • (φ ∨ θ)N есть ¬ (¬φN ∧ ¬θN)
  • (φ → θ)N это φN → θN
  • (¬φ)N это ¬φN
  • (∀Икс φ)N является ∀Икс φN
  • (∃Икс φ)N это ¬∀Икс ¬φN

Этот перевод обладает тем свойством, что φN классически эквивалентен φ. Фундаментальная теорема о надежности (Авигад и Феферман 1998, стр. 342; Басс 1998 стр. 66) гласит:

Если Т - набор аксиом, а φ - формула, то Т доказывает φ с помощью классической логики тогда и только тогда, когда ТN доказывает φN используя интуиционистскую логику.

Вот ТN состоит из переводов двойного отрицания формул в Т.

Предложение φ не может подразумевать его отрицательный перевод φN в интуиционистской логике первого порядка. Трельстра и Ван Дален (1988, гл. 2, раздел 3) дают описание (принадлежащее Лейванту) формул, которые действительно подразумевают их перевод Гёделя – Гентцена.

Варианты

Есть несколько альтернативных определений отрицательного перевода. Все они доказуемо эквивалентны в интуиционистской логике, но могут быть проще применимы в определенных контекстах.

Одна из возможностей - изменить условия для дизъюнкция и экзистенциальный квантор к

  • (φ ∨ θ)N есть ¬¬ (φN ∨ θN)
  • (∃Икс φ)N это ¬¬∃Икс φN

Тогда перевод можно кратко описать как: префикс ¬¬ для каждой атомарной формулы, дизъюнкции и экзистенциального квантора.

Другая возможность (известная как Курода перевод) состоит в построении φN от φ, положив ¬¬ перед всей формулой и после каждого универсальный квантор. Обратите внимание, что это сводится к простому переводу ¬¬φ, если φ пропозиционально.

Также можно определить φN поставив префикс ¬¬ перед каждой подформулой φ, как это сделано Колмогоров. Такой перевод является логическим аналогом вызов по имени стиль передачи перевод функциональные языки программирования по линиям Переписка Карри – Ховарда между доказательствами и программами.

Результаты

Перевод двойного отрицания был использован Геделем (1933) для изучения взаимосвязи между классической и интуиционистской теориями натуральных чисел («арифметикой»). Он получает следующий результат:

Если формула φ выводима из аксиом Арифметика Пеано тогда φN доказуемо из аксиом интуиционистского Арифметика Гейтинга.

Этот результат показывает, что если арифметика Гейтинга непротиворечива, то последовательна и арифметика Пеано. Это потому, что противоречивая формула θ ∧ ¬θ интерпретируется как θN ∧ ¬θN, что до сих пор противоречиво. Более того, доказательство связи является полностью конструктивным, что позволяет преобразовать доказательство θ ∧ ¬θ в арифметике Пеано в доказательство θN ∧ ¬θN в арифметике Гейтинга. (Объединив перевод двойного отрицания с Перевод Фридмана, фактически можно доказать, что арифметика Пеано Π02 -консервативный над арифметикой Гейтинга.)

Пропозициональное отображение φ в ¬¬φ не распространяется на звуковой перевод логики первого порядка, потому что ∀Икс ¬¬φ (Икс) → ¬¬∀Икс φ (Икс) не является теоремой интуиционистской логики предикатов. Это объясняет, почему φN в случае первого порядка должно быть определено более сложным образом.

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

использованная литература

  • Дж. Авигад и С. Феферман (1998), "Функциональная (" Диалектическая ") интерпретация Гёделя", Справочник по теории доказательств »', S. Buss, ed., Elsevier. ISBN  0-444-89840-9
  • С. Басс (1998), "Введение в теорию доказательства", Справочник по теории доказательств, S. Buss, ed., Elsevier. ISBN  0-444-89840-9
  • Г. Генцен (1936), "Die Widerspruchfreiheit der reinen Zahlentheorie", Mathematische Annalen, v. 112, pp. 493–565 (немецкий). Перепечатано в английском переводе как «Непротиворечивость арифметики» в Сборник статей Герхарда Гентцена, М. Э. Сабо, изд.
  • В. Гливенко (1929), Sur quelques points de la logique de M. Brouwer, Бык. Soc. Математика. Бельг. 15, 183–188
  • К. Гёдель (1933), "Zur intuitionistischen Arithmetik und Zahlentheorie", Ergebnisse eines Mathematischen Kolloquiums, v. 4, pp. 34–38 (немецкий). Перепечатано в английском переводе как «Об интуиционистской арифметике и теории чисел» в Неразрешимый, М. Дэвис, изд., Стр. 75–81.
  • Колмогоров А. Н. (1925), «O principe tertium non datur» (рус.). Перепечатано в английском переводе как «По принципу исключенного среднего» в От Фреге до Гёделя, van Heijenoort, ed., pp. 414–447.
  • A. S. Troelstra (1977), «Аспекты конструктивной математики», Справочник по математической логике », Дж. Барвайз, изд., Северная Голландия. ISBN  0-7204-2285-X
  • A. S. Troelstra и Д. ван Дален (1988), Конструктивизм в математике. Введение, тома 121, 123 из Исследования по логике и основам математики, Северная Голландия.

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