lection4.tex

\section{Интуиционистское исчисление высказываний}

Одна из главных причин возникновения математической логики --- кризис в математике
начала XX века. Классический пример такого --- парадокс Рассела, утверждающий,
что понятие <<множества всех не принадлежащих себе множеств>> противоречиво.
В самом деле, пусть $X = \{ t \mid t \notin t \}$. Рассмотрим $X \in X$.
Обе возможных альтернативы --- $X \in X$ и $X \notin X$ --- вступают в противоречие с 
определением множества $X$. Значит, мы можем сделать вывод, что множества $X$ не существует.

С одной стороны, в этом нет проблемы: мы не переживаем, если не найдём числа $t \in \mathbb{N}$ 
такого, что $t=t$ и $t \ne t$ одновременно. Но, с другой стороны, в формальном определении
множества $X$ на первый взгляд нет никаких проблем. Единственная, по-видимому, для современного
читателя непривычная деталь в данном определении --- множество, принадлежащее самому себе, но 
если вспомнить язык Java, то это возражение не должно вызывать никаких серьёзных сомнений.
Просто рассмотрите следующее определение:

\begin{verbatim}
class IntList {
   IntList next;
   int value;
}
\end{verbatim}

Парадокс Рассела был получен не сразу,
а через несколько лет после появления теории множеств и построения значительного количества
математических теорий на её основе. Из этого возникает сомнение, нет ли таких 
же противоречий и в определении, например, вещественных чисел, просто глубже скрытых.
Вдруг через несколько лет какой-то математик найдёт противоречия в математическом анализе --- 
и значительную часть теории придётся пересмотреть или вообще признать ошибочной.

Было предложено много подходов к решению этой проблемы. Современный (классический) подход 
состоит в том, чтобы так формализовать теорию множеств, чтобы в ней не возникало парадоксов.
Была сформулирована программа, предполагавшая своей целью доказательство непротиворечивости
такой формальной теории. Однако в 30-е годы Куртом Гёделем было показано, что такое 
доказательство минимально удовлетворительной надёжности построить невозможно. Конечно,
самая распространённая формализация теории множеств --- аксиоматика Цермело-Френкеля ---
оформилась в современном виде в 1925 году, почти 100 лет назад, и пока никаких противоречий
в ней не было найдено. Но здесь всегда остаётся место для сомнений.

Поэтому интерес представляют альтернативные подходы к проблеме. Данный раздел посвящён 
интуиционистской логике. Математики, стоявшие у истоков данной логики, видели решение в том,
чтобы исключить из рассмотрения <<неконструктивные>> объекты --- объекты, метода построения
которых не предложено. В частности, множество $X$ из примера выше является примером 
неконструктивного объекта. Мы слишком легко приняли на веру возможность его существования и
получили противоречие.

Столь резкие результаты получаются не всегда, но в целом в математике имеет место 
довольно много утверждений, пусть и не противоречивых, но выглядящих совершенно антиинтуитивно.
Например, широко известна теорема Банаха-Тарского, утверждающая, что трёхмерный шар можно 
разрезать на конечное число попарно непересекающихся частей, из которых потом можно составить
два шара того же размера.

\subsection*{BHK-интерпретация}

BHK-интерпретация логики названа по именам математиков, её предложивших 
(Л. Брауэр, А. Гейтинг и А. Колмогоров). 
Они решили изменить сам подход к математическому рассуждению, предположив,
что математик не думает в стиле классической логики и что 
правильно поэтому попробовать формализовать <<интуитивный>> стиль.

Попробуем сформулировать эти соображения применительно к 
логическим связкам исчисления высказываний. Будем определять интерпретацию индуктивно. 
Пусть даны высказывания $P$ и $Q$, тогда:

\begin{itemize}
\item мы считаем $P \& Q$ доказанным, если у нас есть доказательство 
высказывания $P$ и доказательство высказывания $Q$;
\item мы считаем $P \vee Q$ доказанным, если у нас есть доказательство $P$ или 
есть доказательство $Q$ (т.е. мы знаем, какая из двух альтернатив выполнена);
\item мы считаем $P \rightarrow Q$ доказанным, если мы умеем перестраивать любое 
доказательство высказывания $P$ в доказательство высказывания $Q$;
\item мы считаем $\bot$ утверждением, не имеющим доказательства;
\item $\neg P$ есть сокращение для $P \rightarrow \bot$. Иными словами, мы считаем 
$\neg P$ доказанным, если мы умеем из доказательства $P$ получить противоречие.
\end{itemize}

Проиллюстрировать подход можно на примере следующей теоремы.

\begin{theorem}
Существуют два таких вещественных иррациональных числа $p$ и $q$, что $p^q \in \mathbb{Q}$.
\end{theorem}

\begin{proof}
Рассмотрим два случая:
\begin{enumerate}
\item если $\sqrt{2}^{\sqrt{2}} \in \mathbb{Q}$, то мы нашли требуемые числа: $p = q = \sqrt{2}$;
\item если же $\sqrt{2}^{\sqrt{2}} \notin \mathbb{Q}$, то рассмотрим $p = \sqrt{2}^{\sqrt{2}}$
и $q = \sqrt{2}$, тогда $p^q = {\sqrt{2}^{\sqrt{2}}}^{\sqrt{2}} = 2 \in \mathbb{Q}$.
\end{enumerate}
\end{proof}

Данная теорема, хоть и доказывает факт существования таких чисел, но ничего не говорит по поводу
того, какой из двух случаев имеет место --- то есть она неконструктивна. 
В самом деле, 
обозначим факт того, что $\sqrt{2}^{\sqrt{2}} \in \mathbb{Q}$ за $P$, а итоговое утверждение теоремы
--- за $S$. Мы показываем, что $P \rightarrow S$ и что $\neg P \rightarrow S$.
Однако, чтобы перейти к просто $S$, нам нужно показать $P \vee \neg P$. Несложно видеть,
что в BHK-интерпретации нет простого способа это сделать: чтобы считать дизъюнкцию доказанной,
мы должны знать, какой из случаев имеет место. Поэтому данное рассуждение не является
доказательством в BHK-интерпретации.

Для программистов же здесь важным является следующее соображение: эта теорема не 
позволяет написать программу, ищущую эти два числа. Скажем, теорема о дедукции не такова: 
её доказательство позволяет построить такую программу, предъявляющую объект,
существование которого утверждает теорема. 

\subsection*{Формализация интуиционистской логики}

Исходный постулат интуиционистской логики состоит в том, что никакая формализация не является
первичной. Мы выбираем те или иные правила только потому, что они соответствуют заявленным
целям. Мы также вольны в любой момент правила поменять, если на то будут серьёзные основания.

У интуиционистской логики есть несколько формализаций, рассмотрим наиболее распространённую.
Заменим аксиому устранения двойного отрицания (10-ю) на 
$\alpha \rightarrow \neg \alpha \rightarrow \beta$.
Полученную систему назовём аксиоматикой интуиционистского исчисления высказываний.

У данной аксиоматики есть интересные свойства, отсутствующие в классическом исчислении
высказываний. Например, если $\vdash_\texttt{И} \alpha \vee \beta$, то $\vdash_\texttt{И} \alpha$, либо
$\vdash_\texttt{И} \beta$ --- сравните с BHK-интерпретацией дизъюнкции. 
Данное следствие поясняет обоснованность замены аксиомы, в дальнейшем оно будет доказано
формально.