lection7.tex

\section{Теории первого порядка}

Мы занимались до этого момента только логическими рассуждениями самими по 
себе. Это интересно, но не очень практически полезно: мы все-таки
используем логические рассуждения для доказательства утверждений о каких-то
объектах. Было бы разумно каким-то образом включить эти объекты в рамки
формальной теории.

%\subsection{Формальная арифметика. Аксиоматика Пеано.}

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

Рассмотрим некоторое множество $N$. Будем говорить, что оно удовлетворяет
\emph{аксиомам Пеано}, если выполнено следующее:

\begin{itemize}
\item В нем существует некоторый выделенный элемент 0.
\item Для каждого элемента множества определена операция $'$, результат ее
также принадлежит множеству $N$.
\end{itemize}

Кроме того, эти элемент и операция должны удовлетворять следующим требованиям:
\begin{itemize}
\item Не существует такого $x$ из $N$, что $x'=0$.
\item Если при $x$ и $y$ из $N$ верно $x'=y'$, то $x=y$.
\item Если некоторое утверждение, зависящее от некоторого параметра из $N$, 
верно для $0$, и если из допущения его для $n$ можно вывести его истинность 
для $n'$, то утверждение верно для любого элемента из $N$.
\end{itemize}

Данная аксиоматика позволяет определить натуральные числа (множество натуральных
чисел --- это множество, удовлетворяющее аксиомам Пеано; заметим, что тут натуральные
числа содержат 0, так оказывается удобнее) и операции над
ними. Например, сложение можно задать следующими уравнениями:

$$a+0 = a$$
$$a+b' = (a+b)'$$

\begin{theorem}Так определенное сложение коммутативно.
\end{theorem}
\begin{proof}Упражнение.\end{proof}

Но данная аксиоматика сформулирована неформально, поэтому мы не сможем
доказать никаких содержательных утверждений про нее, пользуясь формальными
средствами. Поэтому мы построим \emph{формальную арифметику}, теорию,
базирующуюся на исчислении предикатов, в которой также формализована и
аксиоматика Пеано.

\begin{definition}Теорией первого порядка мы назовем исчисление предикатов
с расширенным языком (к стандартным конструкциям мы добавляем функции и 
предикаты, возможно, с особым синтаксисом) и дополнительными аксиомами. 
Эти дополнения к исчислению предикатов мы назовем \emph{нелогическими} или 
\emph{математическими}. В противоположность им, стандартные конструкции и 
аксиомы исчисления предикатов мы назовем \emph{логическими}.
\end{definition}

Возьмем язык исчисления предикатов со следующими изменениями и особенностями:

\begin{itemize}
\item Маленькими латинскими буквами $a,b,\dots$ (возможно, с индексами) будем 
обозначать индивидные переменные. 
\item К логическим связкам добавляются такие нелогические конструкции языка: 
($=$) --- двуместный предикат, ($+$) и ($\cdot$) --- двуместные функции, и 
($'$) --- одноместная функция. Все двуместные новые конструкции левоассоциативны, 
приоритеты в порядке убывания: ($'$), потом ($\cdot$), потом ($+$). 
Все логические связки имеют приоритет ниже. Например, $a= b'+b'+c \cdot c \with b = c$ 
надо интерпретировать как $(a = (((b') + (b')) + (c \cdot c))) \with (b = c)$.
\item Вводится 0-местная функция $0$.
\end{itemize}

К стандартным аксиомам исчисления предикатов добавим следующие 8 аксиом и одну схему аксиом.

\begin{tabular}{ll}
(A1) & $a = b \rightarrow a' = b'$\\
(A2) & $a = b \rightarrow a = c \rightarrow b = c$\\
(A3) & $a' = b' \rightarrow a = b$\\
(A4) & $\neg a' = 0$\\
(A5) & $a + b' = (a+b)'$\\
(A6) & $a + 0 = a$\\
(A7) & $a \cdot 0 = 0$\\
(A8) & $a \cdot b' = a \cdot b + a$\\
(A9) & $(\psi [x \coloneqq  0]) \with \forall{x}((\psi) \rightarrow (\psi) [x \coloneqq  x']) \rightarrow (\psi)$
\end{tabular}

В схеме аксиом (A9) $\psi$ --- некоторая формула исчисления предикатов и $x$ --- некоторая
переменная, входящая свободно в $\psi$. Данное ограничение объясняется желанием избежать
избыточности, поскольку если $\psi$ не зависит от переменной $x$, то тогда выражение 
$\psi \with \forall{x}(\psi\rightarrow\psi) \rightarrow \psi$ является частным случаем схемы 
аксиом (4).

\begin{theorem}
$\vdash a = a$
\end{theorem}
\begin{proof}
Упражнение. Клини, стр. 254.
\end{proof}

\begin{definition}{Структура.} 
Структурой теории первого порядка мы назовем упорядоченную тройку $\langle{}D, F, P\rangle$,
где $F = \langle{}F_0, F_1, ... \rangle$ --- списки оценок для 0-местных, 1-местных и т.д. функций, 
и $P = \langle{}P_0, P_1, ... \rangle$ --- списки оценок для 0-местных, 1-местных и т.д. предикатов,
$D$ --- предметное множество. 
%Например, функции $f_n^k$ соответствует $k$-й элемент списка $F$
\end{definition}

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

\begin{definition}
Назовем структуру корректной, если любая доказуемая формула истинна в данной структуре.
\end{definition}

\begin{definition}Моделью теории мы назовем любую корректную структуру.\end{definition}

Еще одним примером теории первого порядка может являться теория групп.
К исчислению предикатов добавим двуместный предикат ($=$), 
двуместную функцию ($\cdot$), одноместную функцию ($x^{-1}$), константу (т.е. 0-местную функцию) $1$
и следующие аксиомы:

\begin{tabular}{ll}
(E1) & $a = b \rightarrow (a = c \rightarrow b = c)$\\
(E2) & $a = b \rightarrow (a \cdot c = b \cdot c)$\\
(E3) & $a = b \rightarrow (c \cdot a = c \cdot b)$\\
(G1) & $a \cdot (b \cdot c) = (a \cdot b) \cdot c$\\
(G2) & $a \cdot 1 = a$\\
(G3) & $a \cdot a ^ {-1} = 1$
\end{tabular}

\begin{theorem}Доказуемо, что $a=b \rightarrow b=a$ и что $a^{-1} \cdot a = 1$.
\end{theorem}
\begin{proof} Упражнение. \end{proof}