1632
правки
Изменения
м
= Геделева нумерация. Арифметизация доказательств =[[Категория: Математическая логика]]
rollbackEdits.php mass rollback
[[Лекция 7 Арифметические функции и отношения. Их выразимость в формальной арифметике | <<]][[Лекция 9 1я и 2я теоремы Геделя о неполноте арифметики | >>]]
Ранее мы показали, что любое рекурсивное арифметическое отношение выразимо в формальной арифметике. Теперь мы покажем, что наоборот, любое выразимое в формальной арифметике отношение является рекурсивным.
Тогда текст из <tex>n</tex> символов с геделевыми номерами <tex>c_1, \dots c_n</tex> запишем как число <tex>t = p_1^{c_1} \cdot p_2^{c_2} \cdot \dots \cdot p_n^{c_n}</tex>. Ясно, что такое представление однозначно позволяет установить длину строки (геделева нумерация не содержит 0, поэтому можно определить длину строки как максимальный номер простого числа, на которое делится <tex>t</tex>; будем записывать эту функцию как <tex>Len(s)</tex>), и каждый символ строки в отдельности (будем записывать функцию как <tex>(s)_n</tex>). Также ясно, что функции <tex>Len</tex> и <tex>(x)_n</tex> — рекурсивны.
Чтобы удобнее работать со строками, введем следующую запись. Пусть есть запись вида <<"<tex>с_1 , c_2 , c_3 \dots</tex>>>", здесь <tex>c_i</tex> — какие-то символы языка формальной арифметики, заключенные в кавычки. Эта запись задает число <tex>p_1^{c_1} \cdot \dots \cdot p_n^{c_n}</tex>.
Операцию конкатенации строк <tex>s \star t</tex> определим так. Пусть первая строка имеет символы <tex>s_1, \dots s_n</tex>, а вторая — <tex>t_1, \dots t_m</tex>. Тогда результат их конкатенации — <tex>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}</tex>.
Чтобы представить доказательства, мы будем объединять строки вместе так же, как
объединяем символы в строки: <tex>2^{2^3} \cdot 3^{2^5}</tex> — это последовательность из двух строк, первая — это <<"(>>", а вторая — <<")>>".
Теперь мы можем понять, как написать программу, проверяющую корректность доказательства некоторого утверждения в формальной арифметике. Наметим общую идею. Программа будет состоять из набора рекурсивных отношений и функций, каждое из которых выражает некоторое отношение, содержательное для проверки доказательства. Ниже мы покажем идею данной конструкции, приведя несколько из них.
Путем некоторых усилий мы можем выписать формулу, представляющую двуместное отношение <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>
}}
