Изменения
Нет описания правки
[[Лекция 7 | <<]][[Лекция 9 | >>]]
= Геделева нумерация. Арифметизация доказательств =
Ранее мы показали, что любое рекурсивное арифметическое отношение выразимо в формальной арифметике. Теперь мы покажем, что наоборот, любое выразимое в формальной арифметике отношение является рекурсивным.
{{Определение
|definition=
Ограниченные кванторы <tex>\exists_{x<y} \phi(x)</tex> и <tex>\forall_{x<y} \phi(x)</tex> — сокращения записи для выражений вида <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> — рекурсивные отношения. Тогда следующие формулы, задающие некоторые отношения, также являются рекурсивными отношениями:
# <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>
}}
