Просмотр исходного текста страницы Геделева нумерация. Арифметизация доказательств

[[Арифметические функции и отношения. Их выразимость в формальной арифметике | <<]][[1я и 2я теоремы Геделя о неполноте арифметики | >>]]

[[Категория: Математическая логика]]

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

{{Определение 
|definition=
Ограниченные кванторы <tex>\exists_{x<y} \phi(x)</tex> и <tex>\forall_{x<y} \phi(x)</tex> &mdash; сокращения записи для выражений вида <tex>\exists x (x < y \& \phi(x))</tex> и <tex>\forall x (x \ge y \vee \phi (x))</tex>
}}

{{Теорема
|statement=
Пусть <tex>P_1</tex> и <tex>P_2</tex> &mdash; рекурсивные отношения. Тогда следующие формулы, задающие некоторые отношения, также являются рекурсивными отношениями:

# <tex>F(x_1,\dots x_n,z) := \forall_{y<z} P_1(x_1,\dots x_n,y)</tex>
# <tex>E(x_1, \dots x_n,z) := \exists_{y<z} P_1(x_1,\dots x_n,y)</tex>
# <tex>P_1(x_1,\dots x_n) \rightarrow P_2(x_1,\dots x_n)</tex>
# <tex>P_1(x_1,\dots x_n) \vee P_2(x_1,\dots x_n)</tex>
# <tex>P_1(x_1,\dots x_n) \& P_2(x_1,\dots x_n)</tex>
# <tex>\neg P_1(x_1, \dots x_n)</tex>
|proof=
Упражнение.
}}

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

{{Определение 
|definition=
(Гёделева нумерация)
Дадим следующие номера символам языка формальной арифметики:

3               (<br />
5              )<br />
7                ,<br />
9              <tex>\neg</tex> <br />
11       <tex>\rightarrow</tex> <br />
13            <tex>\vee</tex> <br />
15          <tex>\&</tex> <br />
17         <tex>\forall</tex> <br />
19          <tex>\exists</tex> <br />
<tex>13 + 8\cdot k</tex>    <tex>x_k</tex>   переменные<br />
<tex>15 + 8\cdot k</tex>    <tex>a_k</tex>   константы<br />
<tex>17 + 8\cdot 2^k \cdot 3^n</tex>    <tex>f_k^n</tex>   n-местные функциональные символы: <tex>(')</tex>, <tex>(+)</tex> и т.п.<br />
<tex>19 + 8\cdot 2^k \cdot 3^n</tex>    <tex>P_k^n</tex>   n-местные предикаты, в т.ч. <tex>(=)</tex>
}}

Уточним язык &mdash; обяжем всегда писать скобки всегда и только вокруг двуместной операции. В принципе, иначе мы могли бы определить правильно операцию равенства Eq, но это лишние технические сложности.

Научимся записывать выражения в виде чисел. Пусть <tex>p_1, \dots p_k, \dots</tex> &mdash; список простых чисел, при этом <tex>p_1 = 2, p_2 = 3, \dots</tex>.

Комментарии: 

Также, пусть <tex>Rm(a, b, c) </tex> --- это формула, представляющая отношение <tex>c = a \% b </tex>


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

Чтобы удобнее работать со строками, введем следующую запись. Пусть есть запись вида "<tex> с_1, c_2, c_3 \dots</tex>", здесь <tex>c_i</tex> &mdash; какие-то символы языка формальной арифметики, заключенные в кавычки. Эта запись задает число <tex>p_1^{c_1} \cdot \dots \cdot p_n^{c_n}</tex>.

Операцию конкатенации строк <tex>s \star t</tex> определим так. Пусть первая строка имеет символы <tex>s_1, \dots s_n</tex>, а вторая &mdash; <tex>t_1, \dots t_m</tex>. Тогда результат их конкатенации &mdash; <tex>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}</tex>.

Если в данной записи встретится символ с $ перед ним: "<tex> \neg </tex>$<tex>x \& y </tex>  ", тогда
это означает вставку "литерала" (ср. язык Perl) --- интерпретировать это надо
как конкатенацию строки до литерала, самого литерала, и строки после литерала.
В данном примере --- "<tex>\neg</tex>" <tex>\star x \star</tex> "<tex>\& y</tex>".

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

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

* Проверка того, что a - геделев номер выражения, являющегося переменной. <tex>Var(a) := \exists_{z < a} (a = 2 ^ {13 + z})</tex>
* Проверка того, что выражение с номером <tex>a</tex> получено из выражений <tex>b</tex> и <tex>c</tex> путем применения правила Modus Ponens. <tex> MP (b,c,a) := c = </tex> "<tex>(</tex> $<tex>b \rightarrow </tex> $ <tex>a  )</tex>"
* Проверка того, что <tex>b</tex> получается из <tex>a</tex> подстановкой <tex>y</tex> вместо <tex>x</tex>: <tex>Subst (a,b,x,y)</tex> &mdash; без реализации
*Функция, подставляющая <tex>y</tex> вместо <tex>x</tex> в формуле <tex>a</tex>:<br />
<tex>Sub (a,x,y) := \mu \langle{}S\langle{}Subst,U^4_1,U^4_4,U^4_2,U^4_3\rangle\rangle(a,x,y)</tex>
*Проверка того, что переменная <tex>x</tex> входит свободно в формулу <tex>f</tex>.<br />
<tex>Free (f,x) := \neg Subst(a,a,x,13 + 8^x)</tex>
*Функция, выдающая геделев номер выражения, соответствующего целому числу: <br />
<tex>Num (n) := R( "0", "</tex> $ <tex> U^3_1 ")(n,n)</tex>

Путем некоторых усилий мы можем выписать формулу, представляющую двуместное отношение <tex>Proof(f,p)</tex>, истинное тогда и только тогда, когда <tex>p</tex>  --  геделев номер доказательства формулы с геделевым номером <tex>f</tex>.

{{Теорема
|statement=
Любая представимая в формальной арифметике функция является рекурсивной.
|proof=
Возьмем некоторую представимую функцию <tex>f: N^n \rightarrow N</tex>. Значит, для нее существует формула формальной арифметики, представляющая ее. Пусть <tex>F</tex> &mdash; эта формула (со свободными переменными <tex>x_1, \dots x_n, y</tex>); при этом в случае <tex>f(u_1, \dots u_n) = v</tex> должно быть доказуемо <tex>F(\overline{u_1}, \dots \overline{u_n}, \overline{v})</tex>

По формуле можно построить рекурсивную функцию, <tex>C_F (u_1, \dots u_n, v, p)</tex>, выражающую тот факт, что <tex>p</tex> &mdash; геделев номер вывода формулы <tex>F(\overline{u_1}, \dots \overline{u_n}, \overline{v})</tex>. Тогда возьмем <tex>f (x_1, \dots x_n) := (\mu \langle{}S\langle{}C_F,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</tex>

}}