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

Материал из Викиконспекты
Перейти к: навигация, поиск
Строка 67: Строка 67:
  
 
Чтобы представить доказательства, мы будем объединять строки вместе так же, как
 
Чтобы представить доказательства, мы будем объединять строки вместе так же, как
объединяем символы в строки: <tex>2^{2^3} \cdot 3^{2^5}</tex> &mdash; это последовательность из двух строк, первая &mdash; это &lt;&lt;(&gt;&gt;, а вторая &mdash; &lt;&lt;)&gt;&gt;.
+
объединяем символы в строки: <tex>2^{2^3} \cdot 3^{2^5}</tex> &mdash; это последовательность из двух строк, первая &mdash; это "(", а вторая &mdash; ")".
  
 
Теперь мы можем понять, как написать программу, проверяющую корректность доказательства некоторого утверждения в формальной арифметике. Наметим общую идею. Программа будет состоять из набора рекурсивных отношений и функций, каждое из которых выражает некоторое отношение, содержательное для проверки доказательства. Ниже мы покажем идею данной конструкции, приведя несколько из них.
 
Теперь мы можем понять, как написать программу, проверяющую корректность доказательства некоторого утверждения в формальной арифметике. Наметим общую идею. Программа будет состоять из набора рекурсивных отношений и функций, каждое из которых выражает некоторое отношение, содержательное для проверки доказательства. Ниже мы покажем идею данной конструкции, приведя несколько из них.

Версия 00:57, 14 января 2012

<< >>

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

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


Определение:
Ограниченные кванторы [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] — рекурсивные отношения. Тогда следующие формулы, задающие некоторые отношения, также являются рекурсивными отношениями:
  1. [math]F(x_1,\dots x_n,z) := \forall_{y\lt z} P_1(x_1,\dots x_n,y)[/math]
  2. [math]E(x_1, \dots x_n,z) := \exists_{y\lt z} P_1(x_1,\dots x_n,y)[/math]
  3. [math]P_1(x_1,\dots x_n) \rightarrow P_2(x_1,\dots x_n)[/math]
  4. [math]P_1(x_1,\dots x_n) \vee P_2(x_1,\dots x_n)[/math]
  5. [math]P_1(x_1,\dots x_n) \& P_2(x_1,\dots x_n)[/math]
  6. [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]