lection5.tex

\section{Полнота исчисления предикатов}

Доказательство этого факта довольно объемно, поэтому мы разделим
его на три части. 
\begin{enumerate}
\item Мы научимся работать с произвольными
моделями, уйдя от чрезмерного разнообразия возможных предметных
множеств, предикатов и функциональных символов с помощью понятия
непротиворечивого множества формул.

\item Мы покажем полноту бескванторной части исчисления предикатов.

\item Мы сведем полноту исчисления предикатов к полноте
бескванторной его части.
\end{enumerate}

\subsection{Непротиворечивое множество формул}

Заметим, что само по себе предметное множество в анализе полноты
исчисления фигурирует в стороне от главного вопроса. После того как мы вычислили истинность или ложность конкретных формул в данной 
модели, мы о конкретном предметном множестве забываем. Соответственно, 
каждая модель для нашей цели исчерпывающе описывается списком формул,
которые в этой модели истинны
(в частности, если две разных модели
дают одинаковую оценку для каждой из формул --- нам нет смысла эти
модели разделять). 
Поэтому мы можем изучать свойства оценок и моделей не
прямо, а посредством набора истинных формул.
Следующие определения формализуют это понятие.

\begin{definition}
Назовём $\Gamma$ --- множество \emph{замкнутых} формул --- непротиворечивым, 
если ни для какой
формулы $\alpha$ невозможно показать, что $\Gamma \vdash \alpha$ и
$\Gamma \vdash \neg \alpha$.
\end{definition}

\begin{definition}
Полным непротиворечивым множеством (непротиворечивым бескванторным множеством)
формул назовем такое множество $\Gamma$,
что для любой замкнутой (замкнутой и бескванторной) формулы 
$\alpha$ либо $\alpha \in \Gamma$, либо
$(\neg \alpha) \in \Gamma$.
\end{definition}

\begin{lemma}
Если $\Gamma$ --- непротиворечивое множество замкнутых (бескванторных) формул, то для любой замкнутой (бексванторной) формулы
$\alpha$ либо $\Gamma \cup \{\alpha\}$, либо $\Gamma \cup \{\neg\alpha\}$
непротиворечиво.
\end{lemma}

\begin{proof}
Пусть это не так и найдутся такие $\beta$ и $\delta$, что
$\Gamma, \alpha \vdash \beta \with \neg \beta$ и
$\Gamma, \neg\alpha \vdash \delta \with \neg \delta$.
Без ограничения общности мы можем предположить, что $\beta \equiv \delta$,
поскольку если мы показали $\beta \with \neg \beta$, то мы можем показать и
$\delta \with \neg \delta$ (это можно показать на основании доказуемости формулы 
$\psi \rightarrow \neg\psi \rightarrow \phi$).

Тогда рассмотрим следующее доказательства в предположении $\Gamma$:

\begin{tabular}{lll}\\
$(1\dots k)$ & $\alpha \rightarrow \beta \with \neg\beta$ & Т. о дедукции\\
$(k+1 \dots l)$ & $\neg\alpha \rightarrow \beta \with \neg\beta$ & Т. о дедукции\\
$(l+1)$ & $(\alpha \rightarrow \beta \with \neg\beta) \rightarrow (\neg\alpha\rightarrow \beta \with \neg\beta) \rightarrow (\alpha\vee\neg\alpha\rightarrow \beta \with \neg\beta)$ & Сх. акс. 8\\
$(l+2)$ & $(\neg\alpha\rightarrow \beta \with \neg\beta) \rightarrow (\alpha\vee\neg\alpha\rightarrow \beta \with \neg\beta)$ & M.P. $k$,$l+1$\\
$(l+3)$ & $\alpha\vee\neg\alpha\rightarrow \beta \with \neg\beta$ & M.P. $l$,$l+2$\\
$(l+4 \dots m)$ & $\alpha\vee\neg\alpha$ & Лемма \ref{excluded_third}\\
$(m+1)$ & $\beta \with \neg\beta$ & M.P. $m$,$l+3$
\end{tabular}

Таким образом, имея доказательства противоречивости $\Gamma,\alpha$ и
$\Gamma,\neg\alpha$, мы можем построить доказательство противоречивости и 
самого $\Gamma$.

\end{proof}

\begin{theorem}\label{make_full_set}
Любое множество непротиворечивых формул $\Gamma$ мы можем дополнить до полного
(полного бескванторного) множества.
\end{theorem}

\begin{proof}
Упорядочим все возможные формулы (бескванторные формулы) 
исчисления (их, как не трудно заметить,
счётное количество, и мы можем их занумеровать целыми числами):
$\gamma_1, \gamma_2, \dots$. По данной последовательности построим
последовательность множеств $\Gamma_1, \Gamma_2, \dots$.
Положим $\Gamma_1 = \Gamma$.
Рассмотрим некоторую формулу $\gamma_n$. По предыдущей лемме, либо 
$\Gamma \cup \{\gamma_n\}$, либо $\Gamma \cup \{\neg\gamma_n\}$ 
непротиворечиво. Пусть для определенности это $\Gamma \cup \{\gamma_n\}$.
Тогда положим $\Gamma_{n+1} = \Gamma_n \cup \{\gamma_n\}$.

Возьмем множество $\Gamma^* = \cup \Gamma_n$. Ясно, что это множество
полное --- поскольку мы перебрали все формулы и рассмотрели каждую
формулу вместе со своим отрицанием.
Также ясно, что оно непротиворечиво: иначе есть
доказательство противоречия (оно, естественно, конечного размера),
использующего формулы $\gamma_{p_1} \dots \gamma_{p_n}$, каждая из которых
добавлена на каком-то шаге. Но тогда и множество 
$\Gamma_{\max(p_1, \dots p_n)+1}$ --- множество, построенное при добавлении
последней из формул $\gamma_{p_i}$ --- противоречиво, что доказывает 
утверждение.
\end{proof}

\begin{definition}
Моделью непротиворечивого множества формул мы назовем такие
оценки предикатов и функциональных символов, что каждая из формул данного
множества истинна. Также, по аналогии с исчислением высказываний,
введём обозначение: $\Gamma \models \alpha$ ($\alpha$ следует из $\Gamma$), 
если $\llbracket \alpha \rrbracket = \texttt{И}$ в любой модели
множества $\Gamma$.
\end{definition}

\begin{theorem}
Если $\Gamma \vdash \alpha$, то $\Gamma \models \alpha$.
\end{theorem}

\begin{proof}
Механическая проверка всех правил и схем аксиом.
\end{proof}

\begin{theorem}
Если $\Gamma$ имеет модель, то оно непротиворечиво.
\end{theorem}

\begin{proof}
Пусть это не так, то есть $\Gamma \vdash \alpha$ и $\Gamma \vdash \neg \alpha$.
Значит, $\Gamma \models \alpha$ и $\Gamma \models \neg \alpha$. То есть,
$\llbracket \alpha \rrbracket = \texttt{И}$
Значит, по определению оценки для отрицания, $\llbracket \neg\alpha \rrbracket = \texttt{Л}$.
Но это вступает в противоречие с $\Gamma \models \neg \alpha$.
\end{proof}

\subsection{Полнота бескванторной части исчисления предикатов}

\begin{lemma}\label{full_quantor_less}
Пусть $\Gamma$ --- полное непротиворечивое множество бескванторных
формул. Тогда существует модель для $\Gamma$.
\end{lemma}

\begin{proof}
Будем строить модель, структурной индукцией по сложности формул.
Для начала разберемся с предметным множеством.
В качестве значений для выражений из констант и функциональных 
символов зададим строки, содержащие выражения. Например,
$\llbracket c_1 \rrbracket = \texttt{<<} c_1 \texttt{>>}$,
$\llbracket f_1 (c_1, f_2(c_2)) \rrbracket = \texttt{<<} f_1 (c_1, f_2(c_2)) \texttt{>>}$
и так далее. 
Все здесь происходит аналогично тому, как $\sin(1)$
есть значение, которое мы не можем вычислить точно и предпочитаем
обозначать его своим именем.
Таким образом, в множестве $D$ находятся все возможные выражения,
составленные из констант и функциональных символов.

Теперь рассмотрим формулу --- некоторый предикат вида 
$\pi \equiv P(\theta_1, \dots \theta_n)$, 
где $\theta_i$ --- это некоторое выражение из 
функциональных символов и констант (поскольку все формулы замкнуты, 
в них не могут участвовать переменные). Будем считать его истинным,
если $\pi \in \Gamma$, иначе, если $\neg\pi \in \Gamma$, будем считать его ложным.

Все связки получат значения естественным образом.

Теперь покажем, что полученная модель действительно является моделью
для данного множества формул. Возьмем некоторую формулу $\gamma$ из
$\Gamma$. Докажем чуть более сильное свойство: 
$\llbracket \gamma \rrbracket = \texttt{И}$ тогда и только тогда, 
когда $\gamma \in \Gamma$.

База. Очевидно, что если атомарная формула принадлежит $\Gamma$, то
она имеет оценку истина.

Переход. Пусть дана некоторая составная формула $\gamma$.
Покажем, что ее оценка истинна тогда и только тогда, когда она входит в $\Gamma$
(при условии, что это свойство выполнено для составных частей).

Конструкция здесь похожа на конструкцию при доказательстве полноты
исчисления высказываний. Для примера рассмотрим конъюнкцию и отрицание:
\begin{itemize}
\item Пусть $\llbracket \alpha \with \beta \rrbracket = \texttt{И}$.
Покажем, что $\alpha \with \beta \in \Gamma$. 

В самом деле, пусть это не так и $\neg (\alpha\with\beta) \in \Gamma$,
а, значит, $\Gamma, \alpha \with \beta \vdash \psi \with \neg \psi$.
Тогда $\Gamma, \alpha, \beta \vdash \psi \with \neg \psi$ (доказуемое 
утверждение $(\psi \with \phi \rightarrow \pi) \rightarrow (\psi \rightarrow \phi \rightarrow \pi)$ 
и теорема о дедукции).

Из таблицы истинности конъюнкции следует, что она истинна только если обе ее составных 
части истинны. То есть
$\llbracket \alpha \rrbracket = \texttt{И}$ и $\llbracket \beta \rrbracket = \texttt{И}$.
Значит, $\alpha \in \Gamma$ и $\beta \in \Gamma$, что приводит к противоречивости $\Gamma$.

\item Пусть $\llbracket \alpha \with \beta \rrbracket = \texttt{Л}$.
Покажем, что $\neg(\alpha \with \beta) \in \Gamma$.

Из таблицы истинности следует, что один из параметров обязательно ложен. 
Пусть, например, $\llbracket \alpha \rrbracket = \texttt{Л}$ (случай 
$\llbracket \beta \rrbracket = \texttt{Л}$ рассматривается аналогично). 
Тогда $\alpha \notin \Gamma$, и поэтому $\neg\alpha \in \Gamma$.
Рассмотрим доказательство:

\begin{tabular}{lll}
(1) & $\neg\alpha$ & Предположение\\
(2) & $\neg\alpha \rightarrow \alpha\with\beta\rightarrow\neg\alpha$ & Сх. акс. 1\\
(3) & $\alpha\with\beta \rightarrow \neg\alpha$ & M.P. 1,2\\
(4) & $\alpha \with \beta \rightarrow \alpha$ & Сх. акс. 4\\
(5) & $(\alpha \with \beta \rightarrow \alpha) \rightarrow (\alpha \with \beta \rightarrow \neg\alpha) \rightarrow \neg(\alpha \with \beta)$ & Сх. акс. 9\\
(6) & $(\alpha \with \beta \rightarrow \neg\alpha) \rightarrow \neg(\alpha \with \beta)$ & M.P. 4,5\\
(7) & $\neg(\alpha \with \beta)$ & M.P. 3,6
\end{tabular}

Значит, невозможно, чтобы $\alpha\with\beta \in \Gamma$, поскольку иначе
получится, что $\Gamma$ противоречиво.

\item Пусть $\llbracket \neg\alpha \rrbracket = \texttt{И}$. Из оценки следует 
$\llbracket \alpha \rrbracket = \texttt{Л}$, то есть $\neg\alpha \in \Gamma$. 

\item Пусть $\llbracket \neg\alpha \rrbracket = \texttt{Л}$. Тогда $\llbracket \alpha \rrbracket = \texttt{И}$.
То есть $\alpha \in \Gamma$. Значит, невозможно $\neg\alpha \in \Gamma$, иначе $\Gamma$
было бы противоречиво.

\end{itemize}

\end{proof}

\subsection{Теорема Гёделя о полноте исчисления предикатов}

\begin{definition}
Назовём формулу $\alpha$ формулой с поверхностными кванторами,
если существует такой узел в дереве разбора формулы, не являющийся
квантором, ниже которого нет ни одного квантора, а выше --- 
нет ничего, кроме кванторов.
\end{definition}

Например, формулы $\forall x \exists y \forall z (P(x,y,z) \with P(z,y,x))$ и 
$A \with B$ --- это формулы с поверхностными кванторами, а формулы 
$A \with \forall x B(x)$, $\exists a P(a) \vee \exists b P(b)$
или $\neg \forall x (P (x) \rightarrow P(y))$
формулами с поверхностными кванторами не являются.

\begin{lemma}
Для любой формулы исчисления предикатов найдётся эквивалентная
ей формула с поверхностными кванторами.
\end{lemma}

\begin{proof}Доказательство индукцией по структуре формулы.
Будем пошагово переносить кванторы на один уровень выше, при 
необходимости переименовывая переменные (если формула имеет вид
$\exists x \alpha \with \exists x \beta$, мы ее в итоге преобразуем к виду
$\exists x_1 \exists x_2 (\alpha [x \coloneqq  x_1] \with \beta [x \coloneqq  x_2])$ 
и раскрывая отрицания
($\neg \exists x \alpha$ превратится в $\forall x \neg \alpha$).
\end{proof}

\begin{theorem}{Теорема Гёделя о полноте исчисления предикатов.}
Пусть $\Gamma$ --- непротиворечивое множество формул исчисления предикатов.
Тогда существует модель для $\Gamma$.
\end{theorem}

\begin{proof}
Без потери общности мы будем предполагать, что $\Gamma$ содержит
только формулы с поверхностными кванторами.

Для доказательства теоремы нам достаточно 
избавиться от кванторов, не потеряв непротиворечивости, и сослаться на
\ref{full_quantor_less}. Для этого мы определим следующий процесс
избавления от одного квантора.
Мы построим новый язык, отличающийся от исходного дополнительными 
константами. Пусть эти новые константы имеют имена $d_i^j$
(верхний индекс означает поколение --- мы сперва добавим константы $d_i^1$,
потом $d_i^2$ и т.п.).

Возьмем непротиворечивое множество формул $\Gamma_g$ и пополним его
дополнительными формулами, получив непротиворечивое множество $\Gamma_{g+1}$,
такое что $\Gamma_g \subseteq \Gamma_{g+1}$. 

Возьмем формулу $\gamma \in \Gamma_g$. Возможны такие варианты:
\begin{itemize}
\item $\gamma$ не содержит кванторов. Оставим ее как есть.

\item $\gamma \equiv \forall x \alpha$.
Возьмем все константы, использующиеся в $\Gamma_g$
(это будут $c_i$ и только те $d_i^j$, которые добавлены раньше, т.е. $j \le g$), и 
все выражения, которые мы можем из них построить с участием функциональных
символов (их всё равно счётное количество), 
занумеруем их ($\theta_1, \theta_2, \dots$) и добавим формулы 
$\alpha_1 \equiv \alpha[x \coloneqq  \theta_1], \alpha_2 \equiv \alpha[x \coloneqq  \theta_2], \dots$ 
к $\Gamma_{g+1}$.

\item $\gamma \equiv \exists x \alpha$.
Возьмем новую константу $d_k^{g+1}$, не использовавшуюся ранее, и 
добавим формулу $\alpha [x \coloneqq  d_k^{g+1}]$ к $\Gamma_{g+1}$.
\end{itemize}

Заметим, что все формулы с кванторами пока остаются в $\Gamma_{g+1}$,
мы только добавляем бескванторные формулы.
Такая схема позволяет сделать процесс управляемым
(мы всегда добавляем новые переменные, что упрощает доказательства),
но при этом корректным: ведь нам нужно добавлять по формуле $\forall x \alpha$
все возможные выражения $\alpha[x \coloneqq  \theta]$, не только 
с упоминаемыми в $\Gamma_g$ константами.
При данной схеме мы вернёмся неизбежно к новым (только что добавленным) 
константам при следующей итерации и добавим недостающие формулы.

Покажем, что так построенное множество формул останется
непротиворечивым. Пусть это не так, и существует доказательство
противоречия $\Gamma_{g+1} \vdash \beta \with \neg\beta$. Это доказательство
использует конечное количество шагов, и, следовательно, мы можем явно
выписать все его новые по сравнению с $\Gamma$ посылки, 
перенеся их в правую часть по теореме о
дедукции: $\Gamma_g \vdash \gamma_1 \rightarrow \dots \gamma_n \rightarrow \beta \with \neg\beta$.

Раз мы оставили справа только новые для $\Gamma_g$ формулы,
то каждая из формул $\gamma_i$ была получена из какой-то исходной формулы 
из $\Gamma_g$ путем удаления одного квантора. Мы будем, последовательно перебирая
формулы и перестраивая доказательство,
исключать формулы из правой части, пока не окажется, что предположив противоречивость
$\Gamma_{g+1}$, мы получим противоречивость $\Gamma_g$.

Возможны два варианта:
\begin{itemize}
\item $\gamma_1 \equiv \alpha[x \coloneqq  \theta]$ 
получено из $\forall x \alpha$. Тогда рассмотрим доказательство:

\begin{tabular}{lll}
$(1)$ & $\forall x \alpha \rightarrow \alpha [x \coloneqq  \theta]$ & Сх. акс. $\forall$\\
$(2)$ & $\forall x \alpha$ & $\forall x \alpha$ из $\Gamma_g$\\
$(3)$ & $\alpha [x \coloneqq  \theta]$ & M.P. $2,1$\\
$(4 \dots k)$ & $\alpha [x \coloneqq  \theta] \rightarrow (\gamma_2 \rightarrow \dots \gamma_n \rightarrow \beta \with \neg \beta)$ & Исх. формула\\
$(k+1)$ & $\gamma_2 \rightarrow \dots \gamma_n \rightarrow \beta \with \neg \beta$ & M.P. $3,k$
\end{tabular}

\item $\gamma_1 \equiv \alpha[x \coloneqq  d_k^{g+1}]$ получено из $\exists x \alpha$.
Выберем какую-нибудь переменную, которая не участвует в выводе противоречия --- пусть это $y$.
Заменим все вхождения $d_k^{g+1}$ в доказательстве на $y$. Поскольку
$d_k^{g+1}$ --- константа, то никаких правил для кванторов мы не заденем, и доказательство
останется верным.
Заметим, что поскольку $d_k^{g+1}$ --- константа, введенная специально для замены 
переменной $x$ в данной формуле на шаге $g$
и ранее не встречавшаяся --- то она отсутствует в формулах $\gamma_2 \dots \gamma_n$.
Также, мы можем правильно выбрать $\beta$, чтобы и в нем отсутствовала $d_k^{g+1}$.
Значит, мы можем применить правило для введения $\exists$:

\begin{tabular}{lll}
$(1 \dots k)$ & $\alpha [x \coloneqq  y] \rightarrow (\gamma_2 \rightarrow \dots \gamma_n \rightarrow \beta \with \neg \beta)$ & Исх. формула\\
$(k+1)$ & $\exists y \alpha [x \coloneqq  y] \rightarrow (\gamma_2 \rightarrow \dots \gamma_n \rightarrow \beta \with \neg \beta)$ & Правило для $\exists$\\
$(k+2)$ & $\exists x \alpha$ & Т.к. $\exists x \alpha$ из $\Gamma_g$ \\
$(k+3 \dots l)$ & $\exists y \alpha [x \coloneqq  y]$ & Доказуемо \\
$(l+1)$ & $\gamma_2 \rightarrow \dots \gamma_n \rightarrow \beta \with \neg \beta$ & M.P. $l, k+1$
\end{tabular}

\end{itemize}

Взяв $\Gamma_0 \equiv \Gamma$, получим последовательность
$\Gamma_0 \subseteq \Gamma_1 \subseteq \Gamma_2 \subseteq \dots$. Положим
$\Gamma^* \equiv \cup \Gamma_i$.
$\Gamma^*$ также не может быть противоречиво, поскольку доказательство
использует конечное количество предположений, добавленных, максимум, на шаге $g$. Значит,
множество $\Gamma_g$ тоже противоречиво, что невозможно.
Выделив в $\Gamma^*$ бескванторное подмножество, 
пополнив его по теореме \ref{make_full_set}, по лемме \ref{full_quantor_less}
мы получаем модель для него.

Теперь покажем, что это модель и для всего $\Gamma^*$ (а, значит, и для $\Gamma$).

Рассмотрим некоторую формулу $\gamma \in \Gamma^*$,
покажем, что $\llbracket \gamma \rrbracket = \texttt{И}$.
Проверку мы будем вести индукцией по структуре <<кванторного>> префикса формулы. 

База. Формула не содержит кванторов. В этом случае истинность гарантирует лемма
\ref{full_quantor_less}. 

Переход. Пусть это модель для любой формулы из $\Gamma^*$ с $r$ кванторами.
Покажем, что она остаётся моделью и для формул из $\Gamma^*$ c $r+1$ квантором.
Пусть формула $\gamma$ впервые добавлена на шаге $p$ к $\Gamma_p$. 
Тогда рассмотрим случаи:

\begin{itemize}
\item $\gamma \equiv \forall x \psi$. 
Нам нужно показать, что формула истинна при любом $t \in D$. 
Возьмём некоторый $t$. По построению модели, есть такое $\theta$ ---
выражение из констант и функциональных символов, что 
$\texttt{<<} \theta \texttt{>>} \equiv t$. 

По построению же $\Gamma^*$, начиная с шага $p+1$
мы будем добавлять все формулы вида $\psi [x \coloneqq  \kappa]$, где $\kappa$ ---
некоторая конструкция из констант и функциональных символов.

Также, каждая из констант $c_i$ или $d_i^j$ из $\theta$ добавлена на некотором 
шаге $s_k$. То есть, как только и константы и формула окажутся в $\Gamma_l$
(понятно, что $l = \max(\max(s_k),p)$), так сразу, начиная с $\Gamma_{l+1}$ 
в нём будет присутствовать и $\psi [x \coloneqq  \theta]$. В формуле $\psi$ 
на один квантор меньше --- и, по предположению индукции, поэтому она истинна.

\item $\gamma \equiv \exists x \psi$.
Аналогично, по построению $\Gamma^*$, как только $\psi$ добавляется к $\Gamma_g$,
так сразу формула $\psi[x \coloneqq  d_k^{g+1}]$ появляется в $\Gamma_{g+1}$.
Значит, $\psi$ истинна на значении $\texttt{<<}d_k^{g+1}\texttt{>>}$,
то есть $\gamma$ истинна.
\end{itemize}
\end{proof}

\begin{theorem}
Если $\models \alpha$, то $\vdash \alpha$.
\end{theorem}
\begin{proof}
Рассмотрим множество $\Gamma \equiv \{\neg\alpha\}$. Если $\alpha$ недоказуемо, то 
$\Gamma$ непротиворечиво, и у $\Gamma$ есть модель, причём $\Gamma \models \neg\alpha$.
Значит, неверно, что $\models \alpha$.
\end{proof}