Изменения
Нет описания правки
Дадим следующие номера символам языка формальной арифметики:
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>
}}
Уточним язык — обяжем всегда писать скобки всегда и только вокруг двуместной операции. В принципе, иначе мы могли бы определить правильно операцию равенства Eq, но это лишние технические сложности.
Научимся записывать выражения в виде чисел. Пусть <tex>p_1, \dots p_k, \dots</tex> — список простых чисел, при этом <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> — рекурсивны.
Чтобы удобнее работать со строками, введем следующую запись. Пусть есть запись вида <<<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> \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> — это последовательность из двух строк, первая — это <<(>>, а вторая — <<)>>.
Теперь мы можем понять, как написать программу, проверяющую корректность доказательства некоторого утверждения в формальной арифметике. Наметим общую идею. Программа будет состоять из набора рекурсивных отношений и функций, каждое из которых выражает некоторое отношение, содержательное для проверки доказательства. Ниже мы покажем идею данной конструкции, приведя несколько из них.
* Проверка того, что 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> — без реализации
*Функция, подставляющая <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>.
