lection4.tex

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

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

Сперва объясним эти понятия на языке теории моделей:
если мы строим теорию о некоторых объектах (например, о натуральных 
числах или о множествах), то изучаемые объекты все вместе образуют 
некоторое \emph{предметное} множество (будем его обозначать буквой $D$). 
На данном множестве могут быть заданы \emph{функции}, отображающие элементы
$D$ в $D$, и \emph{предикаты} --- отображающие элементы $D$ в 
истинностные значения.

Например, если мы изучаем арифметические выражения над целыми числами, 
то предментным множеством будет множество целых чисел, сложение и 
вычитание --- это двуместные функции, константу $0$ мы можем при желании
рассмотреть, как нуль-местную функцию, а отношения $(<)$ или $(=)$ ---
это двуместные предикаты.

Теперь рассмотрим эту же конструкцию более формально, с точки зрения теории 
доказательств.

\begin{definition}\emph{Терм} исчисления предикатов (еще мы его будем
называть предметным выражением) --- это:
\begin{itemize}
\item предметная переменная --- маленькая буква начала или конца латинского 
алфавита, возможно, с индексом или апострофом.
\item применение функции (функции мы будем обозначать латинскими 
буквами середины алфавита: $f, g, h, \dots$):
если $\theta_1 \dots \theta_n$ --- термы и $f$ --- 
\emph{функциональный символ} (то есть символ, обозначающий некоторую
функцию), то $f (\theta_1, \dots \theta_n)$ 
--- тоже терм. Также, частным случаем функций являются константы ---
это нульместные функции. Обычно мы их будем обозначать маленькими 
буквами $c$ или $d$, возможно, с индексами.
\end{itemize}
\end{definition}

\begin{definition}\emph{Формула} исчисления предикатов (еще мы ее будем
называть логическим выражением) --- это:
\begin{itemize}
\item если $\alpha$ и $\beta$ --- формулы исчисления предикатов, то 
$\neg \alpha$, $\alpha \with \beta$, $\alpha \vee \beta$, 
$\alpha \rightarrow \beta$ --- также формула. Связки расставлены
в порядке убывания приоритета. Как и в исчислении высказываний,
импликация правоассоциативна, остальные операции --- левоассоциативны.
\item если $\alpha$ --- формула и $x$ --- предметная переменная, то
$\forall x \alpha$ и $\exists x \alpha$ --- также формулы. Кванторы действуют жадно на всё следующее за ними логическое выражение. Например, формула 
$\forall x P(x,5) \vee P(x,7)$ соответствует формуле $\forall x (P(x,5) \vee P(x,7))$.
\item применение предиката (предикаты мы будем обозначать большими
латинскими буквами, возможно, с индексами): если 
$\theta_1 \dots \theta_n$ --- термы, и $P$ --- \emph{предикатный символ}, 
то $P (\theta_1, \dots \theta_n)$ --- формула. В частности, при $n=0$
предикат становится аналогом предметной переменной из исчисления высказываний.
\end{itemize}
\end{definition}

Обратите внимание на понятия предикатный символ и функциональный символ.
Предикат и функция --- это обычные математические функции, отображающие
$D^n$ в $V$ или $D$. Предикатные и функциональные символы же --- это 
некоторые значки в формуле. Им можно сопоставить различные предикаты и 
функции, в зависимости от обстоятельств. Мы иногда будем для краткости
опускать слово <<символ>>, когда будем говорить о тексте формул, но 
это различие всегда надо иметь в виду.

Также заметим, что ничего не мешает нам сделать синтаксис выражений более
приближенным к традиционному при необходимости (это будет, естественно,
всякий раз оговариваться). Например, в выражении $5 = x+2$, понимаемом в
смысле исчисления предикатов, имеется один предикатный символ $(=)$ и
три функциональных символа: два нульместных --- $2$, $5$ --- и один 
двуместный --- $(+)$.

\subsection{Доказательства в исчислении предикатов}
\begin{definition}Дана некоторая формула $s$.
Будем говорить, что подстрока $s_1$ строки $s$ является подформулой, 
если она в точности соответствует какому-то одному нетерминалу
в дереве разбора строки $s$.\end{definition}

\begin{definition}Если в формулу входит подформула, полученная по правилам
для кванторов (то есть, $\forall x \alpha$ или $\exists x \alpha$), то 
мы будем говорить, что формула $\alpha$ находится в области действия 
данного квантора по переменной $x$. Также, будем говорить, что любая подформула 
формулы $\alpha$ находится в области действия данного квантора.
\end{definition}

\begin{definition}Если некоторое вхождение переменной $x$ находится
в области действия квантора по переменной $x$, то такое вхождение
мы назовем \emph{связанным}. Вхождение переменной $x$ непосредственно рядом 
с квантором ($\forall x \dots$) мы назовем \emph{связывающим}.
Те вхождения переменных, которые не являются связанными 
или связывающими, назовем \emph{свободными}. Формула, не имеющая 
свободных вхождений переменных, называется \emph{замкнутой}.
\end{definition}

\begin{definition}Будем говорить, что терм $\theta$ свободен для
подстановки в формулу $\psi$ вместо $x$ (или просто свободен для 
подстановки вместо $x$), если после подстановки $\theta$ вместо 
свободных вхождений $x$ ни одно вхождение свободной переменной
в $\theta$ не станет связанным.
\end{definition}

Чтобы получить список аксиом для исчисления предикатов, возьмем все схемы
аксиом исчисления высказываний и дополним их следующими двумя схемами.
Здесь $x$ - переменная, $\psi$ - некоторая формула, $y$ - некоторая переменная.
Запись $\psi[x \coloneqq  \theta]$ будет означать результат подстановки 
$\theta$ в $\psi$ вместо всех свободных вхождений $x$. Пусть $\theta$ 
свободно для подстановки вместо $x$.

\begin{tabular}{lll}
(11) & $(\forall{x}(\psi)) \rightarrow (\psi[x \coloneqq  \theta])$\\ 
(12) & $(\psi[x \coloneqq  \theta]) \rightarrow \exists{x}(\psi)$
\end{tabular}

Заметим, что если взять формулу $\exists x A(x,y)$, то по схеме аксиом (11),
если игнорировать ограничение на свободу для подстановки, 
следующее утверждение должно быть тавтологией: 
$(\forall y \exists x A(x,y)) \rightarrow \exists x A (x,x)$. Однако, оно ей не является.

Все аксиомы, порожденные данными схемами в новом языке, мы назовем аксиомами исчисления
предикатов.

Правила вывода.
Пусть $x$ не входит свободно в $\phi$. Тогда рассмотрим следующие дополнительные
правила вывода исчисления предикатов:

\begin{tabular}{lll}
$\infer{(\phi) \rightarrow \forall{x}(\psi)}{(\phi) \rightarrow (\psi)}$ &
$\infer{(\exists{x}(\psi)) \rightarrow (\phi)}{(\psi) \rightarrow (\phi)}$
\end{tabular}

Добавив эти схемы к схеме для правила Modus ponens исчисления высказываний,
мы сможем породить множество правил вывода.

%<<Не входит свободно>> - это также важный вопрос.
%Рассмотрим формулу $A(x) \rightarrow A(x)$. Легко показать, что такая
%формула общезначима и доказуема. Однако, $(\exists{x}A(x)) \rightarrow A(x)$
%не является общезначимой, если $A(x)$ не общезначима: достаточно взять в качестве 
%оценки свободной переменной $x$ то значение, на котором $A(x)$ ложна.
%Вывод из гипотез также вполне можно расширить на исчисление предикатов.

\subsection{Оценка выражений в исчислении предикатов}

Для задания оценки для выражения в исчислении предикатов необходимо
вместо оценки для пропозициональных переменных $v_P$ в исчислении 
высказываний ввести оценку для предикатных символов: для каждого 
$k$-местного предикатного символа $P^k_n$ определить функцию 
$v_{P^k_n}: D^k \rightarrow V$. Аналогично, для каждого $k$-местного 
функционального символа $f^k_n$ также надо определить функцию 
$v_{f^k_n}$.

\begin{definition}Формула в исчислении предикатов общезначима, если она 
истинна на любом предметном множестве $D$, при любой оценке предикатных
и функциональных символов, и при любых оценках свободных предметных
переменных.
\end{definition}

\begin{definition}Пусть имеется некоторое исчисление предикатов с множеством
аксиом $A$, и пусть дан некоторый (возможно, пустой) список $\Gamma$ 
формул исчисления предикатов. Тогда, вывод формулы $\alpha$
в исчислении с аксиомами $A \cup \Gamma$ мы назовем выводом из 
допущений $\Gamma$, и будем записывать это как $\Gamma \vdash \alpha$.
\end{definition}

Формулы в списке формул не обязаны быть замкнутыми: например, легко 
показать, что $P(x,y), P(x,y)\rightarrow P(y,x) \vdash P(y,x)$. Однако,
со свободными переменными в допущениях надо быть осторожными, что 
находит своё отражение в теореме о дедукции для исчисления предикатов.

\begin{theorem}
Теорема о дедукции. Если $\Gamma, \alpha \vdash \beta$, 
и в доказательстве отстутствуют применения правил для кванторов, использующих
свободные переменные из формулы $\alpha$, то $\Gamma \vdash \alpha \rightarrow \beta$
Обратно, если $\Gamma \vdash \alpha\rightarrow\beta$, то $\Gamma,\alpha\rightarrow\beta$.
\end{theorem}

\begin{proof}
Доказательство обратного утверждения аналогично доказательству для теоремы о дедукции
для исчисления высказываний.

Доказательство прямого утверждения также проведём аналогично теореме о дедукции 
для исчисления высказываний --- индукцией и разбором случаев. 
3 старых случая остаются те же, что и в исчислении высказываний, 
добавилось 2 новых правила вывода. Упражнение.
\end{proof}

\begin{lemma}\label{free_substitution}
$\llbracket \psi \rrbracket^{x \coloneqq  \llbracket\theta\rrbracket} = \llbracket \psi[x \coloneqq  \theta] \rrbracket$,
если $\theta$ свободна для подстановки в $\psi$ вместо $x$.
\end{lemma}

\begin{proof}
Воспользуемся структурной индукцией по выражению $\psi$.

База индукции. Пусть $\psi$ --- это предикат. Тогда из способа вычисления значения предикатов 
очевидно, что
$\llbracket P(\theta,y_1,\dots y_n) \rrbracket = \llbracket P(x,y_1,\dots y_n)\rrbracket^{x \coloneqq  \llbracket \theta \rrbracket}$.

Переход индукции. Пусть $\psi$ составлено из одного или двух выражений, про которые
утверждение уже доказано. Рассмотрим варианты:

\begin{itemize}
\item $\psi \equiv \alpha \rightarrow \beta$, $\psi \equiv \alpha \with \beta$, $\psi \equiv \alpha \vee \beta$ или
$\psi \equiv \neg \alpha$. Рассмотрение всех этих случаев схоже, возьмем для примера конъюнкцию.

%\begin{tabular}{ll}
$\llbracket\alpha\with\beta\rrbracket^{x\coloneqq \llbracket\theta\rrbracket}
=\llbracket\alpha\rrbracket^{x\coloneqq \llbracket\theta\rrbracket}\with\llbracket\beta\rrbracket^{x\coloneqq \llbracket\theta\rrbracket}
=\llbracket\alpha[x \coloneqq  \theta]\rrbracket\with\llbracket\beta[x\coloneqq \theta]\rrbracket
=\llbracket\alpha[x \coloneqq  \theta]\with\beta[x \coloneqq  \theta]\rrbracket = \llbracket(\alpha\with\beta)[x \coloneqq  \theta]\rrbracket$
%\end{tabular}

\item $\psi \equiv \forall y \alpha$ или $\psi \equiv \exists y \alpha$. Опять же, рассмотрение случаев
аналогично. Покажем, что 
$\llbracket \forall y \alpha \rrbracket^{x \coloneqq  \llbracket\theta\rrbracket} = \llbracket (\forall y \alpha)[x\coloneqq \theta] \rrbracket$.

Без уменьшения общности можем предположить, что $x$ входит свободно в $\forall y\alpha$ --- иначе данная замена
не оказывает влияние на вычисление результата, и равенство очевидно.

Поскольку $\theta$ свободна для подстановки вместо $x$ в $\psi$, то, значит, 
$y$ не входит свободно в $\theta$ (иначе свободный $y$ стал бы связанным при подстановке,
а подстановки обязательно будут иметь место, раз $x$ входит свободно в $\forall y\alpha$).

%Вычислим $\llbracket\theta\rrbracket=v_\theta$ в некоторой фиксированной оценке.
%Если $\llbracket\forall y \alpha\rrbracket^{x \coloneqq  v_\theta} = \texttt{И}$, то не найдётся 
%такого $v_y$, что $\llbracket\alpha\rrbracket^{x \coloneqq  v_\theta, y \coloneqq  v_y} = \texttt{Л}$. 

По предположению индукции, $\llbracket\alpha\rrbracket^{x \coloneqq  \llbracket\theta\rrbracket} = 
\llbracket\alpha[x\coloneqq \theta]\rrbracket$. И, более того,
$\llbracket\alpha\rrbracket^{x \coloneqq  \llbracket\theta\rrbracket, y \coloneqq  v_y} = \llbracket\alpha[x\coloneqq \theta]\rrbracket^{y \coloneqq  v_y}$,
поскольку вычисление оценки $\theta$ не зависит от значения переменной $y$.
Значит, оценки полных формул с квантором также будут совпадать.
\end{itemize}

\end{proof}

\begin{theorem}
Исчисление предикатов корректно, т.е. любое доказуемое утверждение общезначимо.
\end{theorem}

\begin{proof}
Рассмотрим некоторое доказательство $\gamma_1, \dots \gamma_n$, и покажем, что
каждое из утверждений в доказательстве является общезначимым. Этим мы покажем 
утверждение теоремы.

Рассмотрим какое-то утверждение $\gamma_i$. Оно либо является частным случаем
какой-либо из схем аксиом, либо получено из предыдущих утверждений доказательства.
путем применения правил вывода.

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

Возможны следующие варианты:
\begin{enumerate}
\item $\gamma_i \equiv \forall{x}(\psi) \rightarrow (\psi[x \coloneqq  \theta])$ при 
некоторых $x$ (имя переменной тоже может быть разным), $\psi$ и $\theta$. 
Значит, нам необходимо показать, что при любых $x$, $\psi$ и $\theta$ 
(естественно, таких, что $\theta$ свободна для подстановки вместо $x$ в $\psi$) 
данное выражение будет истинным в любой оценке.

Фиксируем некоторую оценку и докажем утверждение от противного. 
Пусть это не так, и 
$\llbracket \forall{x}(\psi)\rightarrow(\psi[x \coloneqq  \theta])\rrbracket = \texttt{Л}$.
Тогда неизбежно, что $\llbracket \forall{x}(\psi) \rrbracket = \texttt{И}$, но
$\llbracket \psi[x\coloneqq \theta] \rrbracket = \texttt{Л}$ (поскольку при остальных значениях
подвыражений импликация будет истинна). 

Пусть в данной оценке $\llbracket\theta\rrbracket=v_\theta$. 
По лемме \ref{free_substitution} верно, что 
$\llbracket \psi[x\coloneqq \theta] \rrbracket = \llbracket\psi\rrbracket^{x\coloneqq v_\theta}$,
причём, поскольку $\llbracket \psi[x\coloneqq \theta] \rrbracket = \texttt{Л}$, то
$\llbracket\psi\rrbracket^{x\coloneqq v_\theta} = \texttt{Л}$.
Но тогда $\llbracket \forall{x}(\psi) \rrbracket = \texttt{И}$ означает, что 
при любом $v_x \in D$ будет выполнено $\llbracket \psi \rrbracket^{x \coloneqq  v_x} = \texttt{И}$. 
Противоречие.

\item $\gamma_i \equiv (\psi[x \coloneqq  \theta]) \rightarrow \exists{x}(\psi)$ при некоторых
$x$, $\psi$ и $\theta$. Рассмотрение аналогично предыдущему пункту: заметим, что импликация
опровергается только если $\llbracket \exists{x}(\psi) \rrbracket = \texttt{Л}$, но
$\llbracket \psi[x\coloneqq \theta] \rrbracket = \texttt{И}$. По лемме 
\ref{free_substitution} при вычислении оценки формулы мы можем отдельно вычислить
$v_\theta = \llbracket\theta\rrbracket$, и показать, что 
$\llbracket \psi[x\coloneqq \theta] \rrbracket = \llbracket\psi\rrbracket^{x\coloneqq v_\theta}$, что 
гарантирует существование элемента в $D$, на котором формула $\psi$ истинна.

\item $\gamma_i \equiv \phi \rightarrow \forall{x}\psi$ и существует такой $j < i$, что
$\gamma_j \equiv \phi \rightarrow \psi$, при этом $x$ не входит свободно в $\phi$.

Опять же, фиксируем некоторую оценку.
Нам нужно показать, что $\forall{x}\psi$ не бывает ложным, если $\phi$ истинно.

По предположению индукции мы знаем, что $\llbracket \phi \rightarrow \psi \rrbracket = \texttt{И}$.
Пусть $\llbracket\forall{x}\psi\rrbracket = \texttt{Л}$. То есть, найдётся такой $v_x$ из $D$, что
$\llbracket \psi \rrbracket^{x\coloneqq v_x} = \texttt{Л}$. 
Но заметим, что $x$ не входит свободно в $\phi$. Значит, $\llbracket \phi \rrbracket^{x\coloneqq v_x} = \texttt{И}$.
Значит, $\llbracket\phi \rightarrow \psi\rrbracket^{x\coloneqq v_x} = \texttt{Л}$. Противоречие с общезначимостью $\gamma_j$.

\item Правило для квантора существования доказывается аналогично.

\end{enumerate}

\end{proof}