Линейная логика V: Двойное отрицание

Лекция на филфаке. Старый профессор говорит:

— В русском языке двойное отрицание может означать утверждение. Но ни в одном языке мира двойное утверждение не может означать отрицание.

Раздается голос с задней парты:
— Ну да, конечно…

Старый анекдот

Однажды во время лекции оксфордский философ Джон Ленгшо Остин высказал мысль, что хотя двойное отрицание в английском языке означает утверждение, нет такого языка, в котором двойное утверждение означало бы отрицание. На что Сидни Моргенбессер, в то время студент, ответил с пренебрежением в голосе: "Да, да...".

Английский вариант анекдота как случай, произошедший с философом Сидни Моргенбессером

Как уже упоминалось в интуиционистской логике отсутствует закон двойного отрицания:

¬¬A ⇏ A

Однако, доказуемо противоположное утверждение:

A ⇒ ¬¬A

Это достаточно легко показать, если вспомнить, что конструктивное отрицание представляет собой функцию, а ¬¬A означает (A ⇒ ⊥) ⇒ ⊥, то есть "дайте мне функцию из A в абсурдный тип, и я получу абсурд". Если при этом есть свидетельство a : A, то такую функцию написать легко:

f : (A ⇒ ⊥) ⇒ ⊥

f ( g : A ⇒ ⊥) =  g ( a ) 

То есть, функция f принимает в качестве параметра функцию g :  A ⇒ ⊥ и, имея свидетельство a,  передаёт его в g, приходя к абсурду. Не так уж важно сейчас, что функция f не может быть вызвана, важно то, что мы можем её задать. Согласно соответствию Карри‒Ховарда это означает доказуемость нашего утверждения. Кроме того, доказуемо

 ¬¬¬A ⇒ ¬A 

Доказательство достаточно просто следует из предыдущего утверждения. Положим у нас есть функция h, которая из ¬¬A конструирует ⊥ (это, напоминаю, и есть свидетельство  ¬¬¬A). Как из этого получить функцию, которая из A конструирует ⊥? Достаточно из A сконструировать ¬¬A и передать его в h. 

То есть, для некоторых конструктивных утверждений выполняются классические законы. Для логики высказываний справедлива теорема, что если в классической логике доказуемо A, то в интуиционистской логике доказуемо ¬¬A. Она носит название теорема Гливенко. 

Когда рассматривается логика предикатов, то теорема Гливенко неверна. Тем не менее, существует способ преобразовать классическую теорему в конструктивную. Один из методов преобразования придуман Гёделем и Генценом. Грубо говоря, он заключается в том, чтоб подобавлять отрицания в разные места высказывания (под кванторы, в том числе). 

Получается, что неконструктивные доказательства  классической математики не являются неверными с точки зрения математики конструктивной, они просто доказывают другие утверждения. Если конструктивная теорема существования должна презентовать в качестве свидетельства искомый объект, то классической достаточно предъявить свидетельство непротиворечивости. В конструктивной математике такими свидетельствами можно оперировать почти также как обычными объектами (они, можно сказать, задают модальность "не исключено, что ..."). Классическая же математика одно от другого просто не отличает. Таким образом, конструктивная логика не обладает меньшей доказательной силой, но различает больше утверждений. 

Означает ли это, что классическая математика может считаться частным случаем конструктивной? Увы, на сегодняшний момент не может. В классической математике используются существенно неконструктивные приёмы. За них отвечает так называемая аксиома выбора. Например, такое обыденное утверждение как «действительные числа можно упорядочить», доказываемое с помощью аксиомы выбора, есть пример утверждения, которому пока не удалось приписать конструктивный смысл. 

Что интересно, что, если немного расширить возможности языка программирования, с которым проводится соответствие, то утверждениям классической логики  можно придать конструктивный смысл напрямую, не прибегая к преобразованиям. Продолжение следует...