В теории доказательств , дисциплине в математической логике , перевод с двойным отрицанием , иногда называемый отрицательным переводом , является общим подходом для встраивания классической логики в интуиционистскую логику . Обычно это делается путем перевода формул в формулы, которые являются классически эквивалентными, но интуиционистски неэквивалентными. Конкретные примеры переводов с двойным отрицанием включают перевод Гливенко для пропозициональной логики , а также перевод Гёделя–Гентцена и перевод Куроды для логики первого порядка .
Самый простой для описания перевод с двойным отрицанием исходит из теоремы Гливенко , доказанной Валерием Гливенко в 1929 году. Она отображает каждую классическую формулу φ в ее двойное отрицание ¬¬φ.
Теорема Гливенко гласит:
Теорема Гливенко подразумевает более общее утверждение:
В частности, набор пропозициональных формул интуиционистски непротиворечив тогда и только тогда, когда он классически выполним .
Перевод Гёделя –Гентцена (названный в честь Курта Гёделя и Герхарда Генцена ) связывает с каждой формулой φ в языке первого порядка другую формулу φ N , которая определяется индуктивно:
как указано выше, но кроме того
и в противном случае
Этот перевод обладает тем свойством, что φ N классически эквивалентен φ. Троелстра и Ван Дален (1988, гл. 2, секция 3) дают описание, принадлежащее Лейванту, формул, которые подразумевают их перевод Гёделя–Гентцена в интуиционистской логике первого порядка. Там это не относится ко всем формулам. (Это связано с тем фактом, что предложения с дополнительными двойными отрицаниями могут быть сильнее, чем их более простой вариант. Например, ¬¬φ → θ всегда подразумевает φ → θ, но схема в другом направлении подразумевала бы устранение двойного отрицания.)
Из-за конструктивных эквивалентностей существует несколько альтернативных определений перевода. Например, действительный закон Де Моргана позволяет переписать отрицательную дизъюнкцию . Таким образом, одну возможность можно кратко описать следующим образом: Префикс "¬¬" перед каждой атомарной формулой, но также и перед каждой дизъюнкцией и квантором существования ,
Другая процедура, известная как перевод Куроды , заключается в построении переведенного φ путем помещения "¬¬" перед всей формулой и после каждого квантора всеобщности . Эта процедура в точности сводится к пропозициональному переводу всякий раз, когда φ является пропозициональным.
В-третьих, вместо этого можно ставить префикс "¬¬" перед каждой подформулой φ, как это сделал Колмогоров . Такой перевод является логическим аналогом перевода в стиле вызова по имени с передачей продолжения функциональных языков программирования в соответствии с соответствием Карри–Ховарда между доказательствами и программами.
Формулы каждого φ, переведенные Гёделем-Гентценом и Куродой, доказано эквивалентны друг другу, и этот результат выполняется уже в минимальной пропозициональной логике . И далее, в интуиционистской пропозициональной логике, формулы, переведенные Куродой и Колмогоровом, также эквивалентны.
Простое пропозициональное отображение φ в ¬¬φ не распространяется на звуковой перевод логики первого порядка, как так называемый двойной отрицательный сдвиг
не является теоремой интуиционистской предикатной логики. Поэтому отрицания в φ N должны быть размещены более определенным образом.
Пусть T N состоит из двойных отрицательных переводов формул в T .
Основная теорема о надежности (Авигад и Феферман, 1998, стр. 342; Бусс, 1998, стр. 66) гласит:
Перевод с двойным отрицанием был использован Гёделем (1933) для изучения взаимосвязи между классическими и интуиционистскими теориями натуральных чисел («арифметикой»). Он получил следующий результат:
Этот результат показывает, что если арифметика Гейтинга непротиворечива, то непротиворечива и арифметика Пеано. Это происходит потому, что противоречивая формула θ ∧ ¬θ интерпретируется как θ N ∧ ¬θ N , что по-прежнему противоречиво. Более того, доказательство этой связи полностью конструктивно, что позволяет преобразовать доказательство θ ∧ ¬θ в арифметике Пеано в доказательство θ N ∧ ¬θ N в арифметике Гейтинга.
Объединив перевод двойного отрицания с переводом Фридмана , можно фактически доказать, что арифметика Пеано является Π02 - консервативной по сравнению с арифметикой Гейтинга.