lection10.tex

\section{Гёделева нумерация. Арифметизация доказательств}

Ранее мы показали, что любое рекурсивное арифметическое отношение 
выразимо в формальной арифметике. Теперь мы покажем, что 
любое выразимое в формальной арифметике отношение является рекурсивным.

\begin{definition} Ограниченные кванторы $\exists_{x<y} \phi(x)$ и
$\forall_{x<y} \phi(x)$ --- сокращения записи для выражений вида 
$\exists x (x < y \with \phi(x))$ и $\forall x (x \ge y \vee \phi (x))$
\end{definition}

\begin{theorem}\label{recursive_relation_logic} Пусть $P_1$ и $P_2$ --- рекурсивные отношения.
Тогда следующие комбинации отношений также являются рекурсивными отношениями:

\begin{enumerate}
\item $F(x_1,\dots x_n,z) \coloneqq  \forall_{y<z} P_1(x_1,\dots x_n,y)$
\item $E(x_1, \dots x_n,z) \coloneqq  \exists_{y<z} P_1(x_1,\dots x_n,y)$
\item $P_1(x_1,\dots x_n) \rightarrow P_2(x_1,\dots x_n)$
\item $P_1(x_1,\dots x_n) \vee P_2(x_1,\dots x_n)$
\item $P_1(x_1,\dots x_n) \with P_2(x_1,\dots x_n)$
\item $\neg P_1(x_1, \dots x_n)$
\end{enumerate}
\end{theorem}

\begin{proof}Упражнение.
\end{proof}

Теперь мы перенесем понятие вывода формулы на язык рекурсивных отношений
и, следовательно, внутрь языка формальной арифметики.

\begin{definition}{Гёделева нумерация.}Дадим следующие номера символам языка
формальной арифметики:

\begin{tabular}{lll}
3 & (\\
5 & )\\
7 & ,\\
9 & $\neg$ \\
11 & $\rightarrow$ \\
13 & $\vee$ \\
15 & $\with$ \\
17 & $\forall$ \\
19 & $\exists$ \\
$21 + 6\cdot k$ & $x_k$ & переменные\\
$23 + 6\cdot 2^k \cdot 3^n$ & $f_k^n$ & n-местные функциональные символы: $(')$, $(+)$ и т.п.\\
$25 + 6\cdot 2^k \cdot 3^n$ & $P_k^n$ & n-местные предикаты, в т.ч. $(=)$
\end{tabular}
\end{definition}

Уточним язык --- обяжем всегда писать скобки вокруг двуместной
операции, и только в этом случае. 
Также укажем номера для предопределенных функций и предикатов:
$f_0^1 \equiv (')$, $f_0^2 \equiv (+)$, $f_1^2 \equiv (\cdot)$, $P_0^2 \equiv (=)$.

Научимся записывать выражения в виде чисел. Пусть $p_1, \dots p_k, \dots$ --- список простых
чисел, при этом $p_1 = 2, p_2 = 3, \dots$. 

Тогда текст из $n$ символов с гёделевыми номерами $c_1, \dots c_n$ запишем как число
$t = p_1^{c_1} \cdot p_2^{c_2} \cdot \dots \cdot p_n^{c_n}$. Ясно, что такое представление
однозначно позволяет установить длину строки (гёделева нумерация не содержит 0, поэтому
можно определить длину строки как максимальный номер простого числа, на которое делится $t$;
будем записывать эту функцию как $\mathit{Len}(s)$),
и каждый символ строки в отдельности (будем записывать функцию как $(s)_n$).
Также ясно, что функции $\mathit{Len}$ и $(x)_n$ --- рекурсивны.

Чтобы удобнее работать со строками, введем следующие обозначения, за которыми скрываются
рекурсивные функции:

\begin{itemize}
\item запись $\texttt{<<}c_1 c_2 c_3 \dots \texttt{>>}$ (где $c_i$ --- какие-то символы языка формальной арифметики)
задает рекурсивную функцию $f: N \rightarrow N$, при этом $f(x) = p_1^{c_1} \cdot \dots \cdot p_n^{c_n}$.

\item Операцию конкатенации строк определим так. Пусть $S$ и $T$ --- рекурсивные функции,
результат вычисления которых являются числа $s = p_1^{s_1} \cdot \dots \cdot p_n^{s_n}$ и
$t = p_1^{t_1} \cdot \dots \cdot p_m^{s_m}$ соответственно. 
Тогда $S @ T$ --- это рекурсивная функция, вычисляющая функции $S$ и $T$, 
результатом работы которой будет
$p_1^{s_1} \cdot \dots \cdot p_n^{s_n} \cdot p_{n+1}^{t_1} \cdot \dots \cdot p_{n+m}^{t_m}$.

\end{itemize}

Чтобы представить доказательства, мы будем объединять строки вместе так же, как
объединяем символы в строки: $2^{2^3} \cdot 3^{2^5}$ --- это последовательность
из двух строк, первая --- это <<(>>, а вторая --- <<)>>.

Теперь мы можем понять, как написать программу, проверяющую корректность доказательства 
некоторого утверждения в формальной арифметике. Наметим общую идею. Программа будет состоять из набора
рекурсивных отношений и функций, каждое из которых выражает некоторое 
отношение, содержательное для проверки доказательства. Ниже мы покажем идею 
данной конструкции, приведя несколько из них.

\begin{itemize}
\item Проверка того, что a - строка, состоящая только из переменной.
$\mathit{Var}(a) \equiv \exists_{z < a} (a = 2 ^ {21 + 6\cdot z})$

\item Проверка того, что выражение с номером $a$ получено из выражений $b$ и $c$ 
путем применения правила Modus Ponens.
$\mathit{MP} (b,c,a) \equiv c = \gq{(} ~@~ b ~@~ \gq{\rightarrow} ~@~ a ~@~ \gq{)}$

\item Проверка того, что $b$ получается из $a$ подстановкой $y$ вместо $x$:
$\mathit{Subst} (a,b,x,y)$ --- без реализации

\item Функция, подставляющая $y$ вместо $x$ в формуле $a$:\\
$\mathit{Sub} (a,x,y) \equiv \mu \langle{}S\langle{}\mathit{Subst},U^4_1,U^4_4,U^4_2,U^4_3\rangle\rangle(a,x,y)$

\item Проверка того, что переменная номер $x$ входит свободно в формулу $f$.\\
$\mathit{Free} (f,x) \equiv \neg \mathit{Subst}(a,a,x,21 + 6x)$

\item Функция, выдающая гёделев номер выражения, соответствующего целому числу:
$\mathit{Num} \equiv S\langle{}R\langle{}\gq{0},S\langle{}@,U^3_3,S\langle{}\gq{'},U^3_1\rangle{}\rangle{}\rangle,U^1_1,U^1_1\rangle{}$

\end{itemize}

Путем некоторых усилий мы можем выписать формулу, представляющую
двухместное отношение $\mathit{Proof}(f,p)$ такое, что $f$ и $p$ состоят в отношении тогда и только тогда, когда
$p$ --- гёделев номер доказательства формулы с гёделевым номером $f$.

\begin{theorem}
Любая представимая в формальной арифметике функция является рекурсивной.
\end{theorem}
\begin{proof}
Возьмем некоторую представимую функцию $f: N^n \rightarrow N$. Значит, для нее существует
формула формальной арифметики, представляющая ее. Пусть $\phi$ --- эта формула
(со свободными переменными $x_1, \dots x_n, y$); при этом в случае 
$f(u_1, \dots u_n) = v$ должно быть доказуемо $\phi(\overline{u_1}, \dots \overline{u_n}, \overline{v})$.
По формуле можно построить рекурсивную функцию, $C_\phi (u_1, \dots u_n, v, p)$, 
выражающую тот факт, что $p$ --- гёделев номер вывода формулы 
$\phi(\overline{u_1}, \dots \overline{u_n}, \overline{v})$. Тогда 
возьмем $$f (x_1, \dots x_n) \equiv (\mu \langle{}S\langle{}C_\phi,U^{n+1}_1,\dots U^{n+1}_n,(U^{n+1}_{n+1})_1, (U^{n+1}_{n+1})_2\rangle\rangle (x_1, \dots x_n))_1$$.
\end{proof}