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

<< >>

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

Определение:

Ограниченные кванторы [math]\exists_{x\lt y} \phi(x)[/math] и [math]\forall_{x\lt y} \phi(x)[/math] — сокращения записи для выражений вида [math]\exists x (x \lt y \& \phi(x))[/math] и [math]\forall x (x \ge y \vee \phi (x))[/math]

Теорема:

Пусть [math]P_1[/math] и [math]P_2[/math] — рекурсивные отношения. Тогда следующие формулы, задающие некоторые отношения, также являются рекурсивными отношениями: [math]F(x_1,\dots x_n,z) := \forall_{y\lt z} P_1(x_1,\dots x_n,y)[/math] [math]E(x_1, \dots x_n,z) := \exists_{y\lt z} P_1(x_1,\dots x_n,y)[/math] [math]P_1(x_1,\dots x_n) \rightarrow P_2(x_1,\dots x_n)[/math] [math]P_1(x_1,\dots x_n) \vee P_2(x_1,\dots x_n)[/math] [math]P_1(x_1,\dots x_n) \& P_2(x_1,\dots x_n)[/math] [math]\neg P_1(x_1, \dots x_n)[/math]

Доказательство:

[math]\triangleright[/math]

Упражнение.

[math]\triangleleft[/math]

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

Определение:

(Гёделева нумерация) Дадим следующие номера символам языка формальной арифметики: 3 ( 5 ) 7 , 9 [math]\neg[/math] 11 [math]\rightarrow[/math] 13 [math]\vee[/math] 15 [math]\&[/math] 17 [math]\forall[/math] 19 [math]\exists[/math] [math]13 + 8\cdot k[/math] [math]x_k[/math] переменные [math]15 + 8\cdot k[/math] [math]a_k[/math] константы [math]17 + 8\cdot 2^k \cdot 3^n[/math] [math]f_k^n[/math] n-местные функциональные символы: [math](')[/math], [math](+)[/math] и т.п. [math]19 + 8\cdot 2^k \cdot 3^n[/math] [math]P_k^n[/math] n-местные предикаты, в т.ч. [math](=)[/math]

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

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

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

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

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

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

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

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

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

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

• Проверка того, что a - геделев номер выражения, являющегося переменной. [math]Var(a) := \exists_{z \lt a} (a = 2 ^ {13 + z})[/math]
• Проверка того, что выражение с номером [math]a[/math] получено из выражений [math]b[/math] и [math]c[/math] путем применения правила Modus Ponens. [math] MP (b,c,a) := c = [/math] "[math]([/math] $[math]b \rightarrow [/math] $ [math]a )[/math]"
• Проверка того, что [math]b[/math] получается из [math]a[/math] подстановкой [math]y[/math] вместо [math]x[/math]: [math]Subst (a,b,x,y)[/math] — без реализации
• Функция, подставляющая [math]y[/math] вместо [math]x[/math] в формуле [math]a[/math]:
  

[math]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)[/math]

• Проверка того, что переменная [math]x[/math] входит свободно в формулу [math]f[/math].
  

[math]Free (f,x) := \neg Subst(a,a,x,13 + 8^x)[/math]

• Функция, выдающая геделев номер выражения, соответствующего целому числу:
  

[math]Num (n) := R( "0", "[/math] $ [math] U^3_1 ")(n,n)[/math]

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

Теорема:

Любая представимая в формальной арифметике функция является рекурсивной.

Доказательство:

[math]\triangleright[/math]

Возьмем некоторую представимую функцию [math]f: N^n \rightarrow N[/math]. Значит, для нее существует формула формальной арифметики, представляющая ее. Пусть [math]F[/math] — эта формула (со свободными переменными [math]x_1, \dots x_n, y[/math]); при этом в случае [math]f(u_1, \dots u_n) = v[/math] должно быть доказуемо [math]F(\overline{u_1}, \dots \overline{u_n}, \overline{v})[/math] По формуле можно построить рекурсивную функцию, [math]C_F (u_1, \dots u_n, v, p)[/math], выражающую тот факт, что [math]p[/math] — геделев номер вывода формулы [math]F(\overline{u_1}, \dots \overline{u_n}, \overline{v})[/math]. Тогда возьмем [math]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[/math]

[math]\triangleleft[/math]