Изменения

[[Лекция 7 Арифметические функции и отношения. Их выразимость в формальной арифметике | <<]][[Лекция 9 1я и 2я теоремы Геделя о неполноте арифметики | >>]]

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>}} Уточним язык &mdash; обяжем всегда писать скобки всегда и только вокруг двуместной операции. В принципе, иначе мы могли бы определить правильно операцию равенства Eq, но это лишние технические сложности. Научимся записывать выражения в виде чисел. Пусть <tex>p_1, \dots p_k, \dots</tex> &mdash; список простых чисел, при этом <tex>p_1 = 2, p_2 = 3, \dots</tex>. Комментарии:  Также, пусть <tex>Rm(a, b, c) </tex> --- это формула, представляющая отношение <tex>c = a \% b </tex>  Тогда текст из <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> &mdash; рекурсивны. Чтобы удобнее работать со строками, введем следующую запись. Пусть есть запись вида "<tex> с_1, c_2, c_3 \dots</tex>", здесь <tex>c_i</tex> &mdash; какие-то символы языка формальной арифметики, заключенные в кавычки. Эта запись задает число <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>, а вторая &mdash; <tex>t_1, \dots t_m</tex>. Тогда результат их конкатенации &mdash; <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> \neg </tex>$<tex>x \& y </tex> ", тогдаэто означает вставку "литерала" (ср. язык Perl) --- интерпретировать это надокак конкатенацию строки до литерала, самого литерала, и строки после литерала.В данном примере --- "<tex>\neg</tex>" <tex>\star x \star</tex> "<tex>\& y</tex>". Чтобы представить доказательства, мы будем объединять строки вместе так же, какобъединяем символы в строки: <tex>2^{2^3} \cdot 3^{2^5}</tex> &mdash; это последовательность из двух строк, первая &mdash; это "(", а вторая &mdash; ")". Теперь мы можем понять, как написать программу, проверяющую корректность доказательства некоторого утверждения в формальной арифметике. Наметим общую идею. Программа будет состоять из набора рекурсивных отношений и функций, каждое из которых выражает некоторое отношение, содержательное для проверки доказательства. Ниже мы покажем идею данной конструкции, приведя несколько из них. * Проверка того, что a - геделев номер выражения, являющегося переменной. <tex>Var(a) := \exists_{z < a} (a = 2 ^ {13 + z})</tex>* Проверка того, что выражение с номером <tex>a</tex> получено из выражений <tex>b</tex> и <tex>c</tex> путем применения правила Modus Ponens. <tex> MP (b,c,a) := c = </tex> "<tex>(</tex> $<tex>b \rightarrow </tex> $ <tex>a )</tex>"* Проверка того, что <tex>b</tex> получается из <tex>a</tex> подстановкой <tex>y</tex> вместо <tex>x</tex>: <tex>Subst (a,b,x,y)</tex> &mdash; без реализации*Функция, подставляющая <tex>y</tex> вместо <tex>x</tex> в формуле <tex>a</tex>:<br /><tex>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)</tex>*Проверка того, что переменная <tex>x</tex> входит свободно в формулу <tex>f</tex>.<br /><tex>Free (f,x) := \neg Subst(a,a,x,13 + 8^x)</tex>*Функция, выдающая геделев номер выражения, соответствующего целому числу: <br /><tex>Num (n) := R( "0", "</tex> $ <tex> U^3_1 ")(n,n)</tex> Путем некоторых усилий мы можем выписать формулу, представляющую двуместное отношение <tex>Proof(f,p)</tex>, истинное тогда и только тогда, когда <tex>p</tex> -- геделев номер доказательства формулы с геделевым номером <tex>f</tex>. {{Теорема|statement=Любая представимая в формальной арифметике функция является рекурсивной.|proof=Возьмем некоторую представимую функцию <tex>f: N^n \rightarrow N</tex>. Значит, для нее существует формула формальной арифметики, представляющая ее. Пусть <tex>F</tex> &mdash; эта формула (со свободными переменными <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> &mdash; геделев номер вывода формулы <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>