Изменения
Нет описания правки
Путем некоторых усилий мы можем выписать формулу, представляющую двуместное отношение <tex>Proof(f,p)</tex>, истинное тогда и только тогда, когда <tex>p</tex> -- геделев номер доказательства формулы с геделевым номером <tex>f</tex>.
{{Теорема
|statement=
Любая представимая в формальной арифметике функция является рекурсивной.
|proof=
Возьмем некоторую представимую функцию <tex>f: N^n \rightarrow N</tex>. Значит, для нее существует формула формальной арифметики, представляющая ее. Пусть <tex>F</tex> — эта формула (со свободными переменными <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> — геделев номер вывода формулы <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>
}}
