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

<< >>

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

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

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

Ограниченные кванторы [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]