Геделєва нумерація
Раніше ми показали, що будь-яке рекурсивне арифметичне відношення виразне у формальній арифметиці. Тепер ми покажемо, що навпаки, будь-яке виразне у формальній арифметиці ставлення є рекурсивним.
| Визначення: |
| Обмежені квантори [math]\exists_ \phi(x)[/math] і [math]\forall_ \phi(x)[/math] — скорочення запису для виразів виду [math]\exists x (x \lt y \& \phi(x))[/math] і [math]\forall x (x \ge y \vee \phi(x))[/math] |
| Теорема: |
Тепер ми перенесемо поняття виведення формули на мову рекурсивних відносин, а отже, всередину мови формальної арифметики.
| Визначення: |
| (Геделєва нумерація) |
Надамо наступні номери символам мови формальної арифметики:
3 ( 5 ) 7 , 9 [math]\neg[/math] 11 [math]\rightarrow[/math] 13 [math]\vee[/math ] 15 [math]\&[/math] 17 [math]\forall[/math] 19 [math]\exists[/math] [math]13 + 8 \cdot k[/math] [math]x_k[/math] змінні [math]15 + 8\cdot k[/math] [math]a_k[/math] константи [math]17 + 8 \cdot 2^k \cdot 3^n[/math] [math]f_k^n[/math] n-місцеві функціональні символи: [math](')[/math] , [math](+)[/math ] і т.п.
[math]19 + 8\cdot 2^k \cdot 3^n[/math] [math]P_k^n[/math] n-місцеві предикати, в т.ч. [math](=)[/math]
Уточнимо мову - зобов'яжемо завжди писати дужки завжди і тільки навколо двомісної операції. В принципі, інакше ми могли б правильно визначити операцію рівностіАле це зайві технічні складності.
Навчимося записувати вирази у вигляді чисел. Нехай [math]p_1, \dots p_k, \dots[/math] - Список простих чисел, при цьому [math]p_1 = 2, p_2 = 3, \dots[/math] .
Також, нехай [math]Rm(a, b, c) [/math] --- це формула, що представляє відношення [math]c = a \% b [/math]
Тоді текст із [math]n[/math] символів з геделевими номерами [math]c_1, \dots c_n[/math] запишемо як число [math]t = p_1^ \cdot p_2^ \cdot \dots \cdot p_n^[/math]. Зрозуміло, що таке уявлення однозначно дозволяє встановити довжину рядка (геделева нумерація не містить 0, тому можна визначити довжину рядка як максимальний номер простого числа, на яке ділиться [math]t[/math] ; записуватимемо цю функцію як [math]Len( s)[/math] ), і кожен символ рядка окремо (записуватимемо функцію як [math](s)_n[/math] ). Також ясно, що функції [math] Len [/ math] і [ math] (x) n [/ math] - рекурсивні.
Щоб зручніше працювати з рядками, введемо наступний запис. Нехай є запис виду "[math] с_1, c_2, c_3 \dots[/math]", тут [math]c_i[/math] - якісь символи мови формальної арифметики, укладені в лапки. Цей запис визначає число [math]p_1^ \cdot \dots \cdot p_n^[/math] .
Операцію конкатенації рядків [math] s \ star t [/ math] визначимо так. Нехай перший рядок має символи [math] s_1, \ dots s_n [/ math], а другий - [math] t_1, \ dots t_m [/ math]. Тоді результат їхньої конкатенації — [math]p_1^ \cdot \dots \cdot p_n^ \cdot p_^ \cdot \dots \cdot p_^[/math] .
Якщо в даному записі зустрінеться символ з $ перед ним: "[math] \neg[/math]$[math]x \& y[/math]", тоді це означає вставку "літералу" (пор. мова Perl) - - Інтерпретувати це треба як конкатенацію рядка до літерала, самого літерала, і рядки після літерала. Уданому прикладі --- "[math]\neg[/math]" [math]\star x \star[/math] "[math]\& y[/math]".
Щоб надати докази, ми об'єднуватимемо рядки разом так само, як об'єднуємо символи в рядки: [math]2^ \cdot 3^[/math] — це послідовність з двох рядків, перший — це "(", а другий — ") ".
Тепер ми можемо зрозуміти, як написати програму, яка перевіряє коректність доказу деякого затвердження у формальній арифметиці. Намітимо загальну ідею. Програма складатиметься з набору рекурсивних стосунків та функцій, кожне з яких виражає певне відношення, що є змістовним для перевірки доказу. Нижче ми покажемо ідею даної конструкції, навівши кілька їх.
- Перевірка того, що a - геделевий номер виразу, що є змінною. [math]Var(a) := \exists_ (a = 2 ^ )[/math]
- Перевірка того, що вираз із номером [math]a[/math] отримано з виразів [math]b[/math] та [math]c[/math] шляхом застосування правила Modus Ponens. [math] MP (b,c,a) := c = [/math] " [math]([/math] $ [math]b \rightarrow [/math] $ [math]a )[/math] "
- Перевірка того, що [math]b[/math] виходить з [math]a[/math] підстановкою [math]y[/math] замість [math]x[/math] : [math]Subst (a,b, x, y) [/ math] - без реалізації
- Функція, яка підставляє [math]y[/math] замість [math]x[/math] у формулі [math]a[/math] :
[math]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)[/math]
- Перевірка те, що змінна [math]x[/math] вільно входить у формулу [math]f[/math] .
[math] Free (f,x) := \neg Subst(a,a,x,13 + 8^x)[/math]
- Функція, що видає геделев номер виразу, відповідного цілого числа:
[math]Num (n) := R( "0", "[/math] $ [math] U^3_1 ")(n,n)[/math]
Шляхом деяких зусиль ми можемо виписати формулу, що представляє двомісне відношення [math]Proof(f,p)[/math] , істинне тоді і тільки тоді, коли [math]p[/math] - номер доказу формули з геделевим номером math] f [/ math] .
| Теорема: |
Візьмемо деяку функцію [math]f: N^n \rightarrow N[/math] . Значить, для неї існує формула формальної арифметики, яка її представляє. Нехай [math]F[/math] - ця формула (з вільними змінними [math]x_1, \dots x_n, y[/math]); при цьому у випадку [math] f (u_1, \ dots u_n) = v [/ math] має бути доведено [math] F (\ overline, \ dots \ overline, \ overline) [/ math]