Перевод с двойным отрицанием

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

Пропозициональная логика

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

Результаты

Теорема Гливенко гласит:

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

Из теоремы Гливенко следует более общее утверждение:

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

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

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

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

• Если φ атомарна, то φ ^Н это ¬¬φ

как указано выше, но кроме того

• (φ ∨ θ) ^Н есть ¬(¬φ ^Н ∧ ¬θ ^Н )
• (∃ х φ) ^Н есть ¬(∀ x ¬φ ^Н )

и в противном случае

• (φ ∧ θ) ^Н это φ ^Н ∧ я ^Н
• (φ → θ) ^Н это φ ^Н → я ^Н
• (¬φ) ^Н это ¬φ ^Н
• (∀ х φ) ^Н есть ∀ x φ ^Н

Этот перевод обладает тем свойством, что φ ^Н классически эквивалентен φ. Троелстра и Ван Дален (1988, гл. 2, раздел 3) дают описание, принадлежащее Лейванту, формул, которые также подразумевают их перевод Гёделя–Гентцена в интуиционистской логике первого порядка. Там это не для всех формул так. (Это связано с тем, что предложения с дополнительными двойными отрицаниями могут быть сильнее, чем их более простой вариант. Например, ¬¬φ → θ всегда подразумевает φ → θ, но схема в другом направлении будет подразумевать устранение двойного отрицания.)

Эквивалентные варианты

Ввиду конструктивной эквивалентности существует несколько альтернативных определений перевода. Например, действующий закон Де Моргана позволяет переписать отрицательную дизъюнкцию . Таким образом, одну из возможностей можно кратко описать следующим образом: префикс «¬¬» перед каждой атомарной формулой, а также перед каждой дизъюнкцией и квантором существования .

• (φ ∨ θ) ^Н есть ¬¬(φ ^Н ∨ я ^Н )
• (∃ х φ) ^Н есть ¬¬∃ x φ ^Н

Другая процедура, известная как перевод Куроды , заключается в построении переведенного φ путем добавления «¬¬» перед всей формулой и после каждого квантора универсальности . Эта процедура в точности сводится к пропозициональному переводу всякий раз, когда φ пропозициональна.

В-третьих, вместо этого можно поставить префикс «¬¬» перед каждой подформулой φ, как это сделал Колмогоров . Такой перевод является логическим аналогом по имени с передачей продолжения перевода в стиле функционального программирования в соответствии с соответствием Карри-Ховарда между доказательствами и программами.

Формулы каждого φ, переведенные Гёделем-Гентценом и Куродой, доказанно эквивалентны друг другу, и этот результат справедлив уже в минимальной логике высказываний . Более того, в интуиционистской пропозициональной логике формулы, переведенные Куродой и Колмогоровым, также эквивалентны.

Простое пропозициональное отображение φ в ¬¬φ не распространяется на разумный перевод логики первого порядка, поскольку так называемый сдвиг двойного отрицания

∀ Икс ¬¬φ( Икс ) → ¬¬∀ Икс φ( Икс )

не является теоремой интуиционистской логики предикатов. Итак, отрицания в φ ^Н должны быть размещены более особым образом.

Результаты

Пусть Т ^Н состоят из двойного отрицания перевода формул в T .

Фундаментальная теорема о надежности (Авигад и Феферман, 1998, стр. 342; Басс, 1998, стр. 66) гласит:

Если T — набор аксиом, а φ — формула, то T доказывает φ с использованием классической логики тогда и только тогда, когда T ^Н доказывает φ ^Н используя интуиционистскую логику.

Арифметика

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

Если формула φ доказуема из аксиом арифметики Пеано , то φ ^Н доказуемо на основе аксиом арифметики Гейтинга .

Этот результат показывает, что если арифметика Гейтинга непротиворечива, то и арифметика Пеано непротиворечива. Это связано с тем, что противоречивая формула θ ∧ ¬θ интерпретируется как θ ^Н ∧ ¬θ ^Н , что по-прежнему противоречиво. Более того, доказательство связи является полностью конструктивным, позволяя преобразовать доказательство θ ∧ ¬θ в арифметике Пеано в доказательство θ ^Н ∧ ¬θ ^Н в арифметике Гейтинга.

Комбинируя перевод двойного отрицания с переводом Фридмана , фактически можно доказать, что арифметика Пеано равна Π ⁰ ₂ - консервативная по гейтинговской арифметике.

См. также

• Диалектическая интерпретация
• Модальный компаньон

Ссылки

• Дж. Авигад и С. Феферман (1998), «Функциональная («Диалектика») интерпретация Гёделя», Справочник по теории доказательств , С. Басс, изд., Elsevier. ISBN   0-444-89840-9
• С. Басс (1998), «Введение в теорию доказательств», Справочник по теории доказательств , изд. С. Басса, Elsevier. ISBN   0-444-89840-9
• Г. Генцен (1936), «Непротиворечивость чистой теории чисел», Mathematical Annals , v. 112, стр. 493–565 (немецкий). Перепечатано в английском переводе как «Непротиворечивость арифметики» в Сборнике статей Герхарда Генцена , М. Е. Сабо, изд.
• В. Гливенко (1929), О некоторых пунктах логики М. Брауэра , Бюлл. Соц. Математика. Бельгия. 15, 183 – 188
• К. Гёдель (1933), «Об интуиционистской арифметике и теории чисел», результаты математического коллоквиума , v. 4, стр. 34–38 (немецкий). Перепечатано в английском переводе как «Об интуиционистской арифметике и теории чисел» в журнале «Неразрешимое » под ред. М. Дэвиса, стр. 75–81.
• А. Н. Колмогоров (1925), "O principe tertium non datur" (рус.). Перепечатано в английском переводе как «О принципе исключенного третьего» в книге « От Фреге до Гёделя » , ван Хейеноорт, изд., стр. 414–447.
• А. С. Троелстра (1977), «Аспекты конструктивной математики», Справочник по математической логике , Дж. Барвайз , изд., Северная Голландия. ISBN   0-7204-2285-X
• А.С. Троэльстра и Д. ван Дален (1988), Конструктивизм в математике. Введение , тома 121, 123 « Исследований по логике и основам математики» , Северная Голландия.

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

• « Интуиционистская логика », Стэнфордская энциклопедия философии.
• Мут, Ричард; Реторе, Кристиан (2016). «Классическая логика и интуиционистская логика: эквивалентные формулировки в естественной дедукции, перевод Гёделя-Колмогорова-Гливенко». arXiv : 1602.07608 [ math.LO ].