Геделева нумерация. Арифметизация доказательств — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
(Новая страница: « << >>»)
 
м (rollbackEdits.php mass rollback)
 
(не показано 11 промежуточных версий 5 участников)
Строка 1: Строка 1:
[[Лекция 7 | <<]][[Лекция 9 | >>]]
+
[[Арифметические функции и отношения. Их выразимость в формальной арифметике | <<]][[1я и 2я теоремы Геделя о неполноте арифметики | >>]]
 +
 
 +
[[Категория: Математическая логика]]
 +
 
 +
Ранее мы показали, что любое рекурсивное арифметическое отношение выразимо в формальной арифметике. Теперь мы покажем, что наоборот, любое выразимое в формальной арифметике отношение является рекурсивным.
 +
 
 +
{{Определение
 +
|definition=
 +
Ограниченные кванторы <tex>\exists_{x<y} \phi(x)</tex> и <tex>\forall_{x<y} \phi(x)</tex> &mdash; сокращения записи для выражений вида <tex>\exists x (x < y \& \phi(x))</tex> и <tex>\forall x (x \ge y \vee \phi (x))</tex>
 +
}}
 +
 
 +
{{Теорема
 +
|statement=
 +
Пусть <tex>P_1</tex> и <tex>P_2</tex> &mdash; рекурсивные отношения. Тогда следующие формулы, задающие некоторые отношения, также являются рекурсивными отношениями:
 +
 
 +
# <tex>F(x_1,\dots x_n,z) := \forall_{y<z} P_1(x_1,\dots x_n,y)</tex>
 +
# <tex>E(x_1, \dots x_n,z) := \exists_{y<z} P_1(x_1,\dots x_n,y)</tex>
 +
# <tex>P_1(x_1,\dots x_n) \rightarrow P_2(x_1,\dots x_n)</tex>
 +
# <tex>P_1(x_1,\dots x_n) \vee P_2(x_1,\dots x_n)</tex>
 +
# <tex>P_1(x_1,\dots x_n) \& P_2(x_1,\dots x_n)</tex>
 +
# <tex>\neg P_1(x_1, \dots x_n)</tex>
 +
|proof=
 +
Упражнение.
 +
}}
 +
 
 +
Теперь мы перенесем понятие вывода формулы на язык рекурсивных отношений, и, следовательно, внутрь языка формальной арифметики.
 +
 
 +
{{Определение
 +
|definition=
 +
(Гёделева нумерация)
 +
Дадим следующие номера символам языка формальной арифметики:
 +
 
 +
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>
 +
 
 +
}}

Текущая версия на 19:19, 4 сентября 2022

<< >>

Ранее мы показали, что любое рекурсивное арифметическое отношение выразимо в формальной арифметике. Теперь мы покажем, что наоборот, любое выразимое в формальной арифметике отношение является рекурсивным.


Определение:
Ограниченные кванторы [math]\exists_{x\lt y} \phi(x)[/math] и [math]\forall_{x\lt y} \phi(x)[/math] — сокращения записи для выражений вида [math]\exists x (x \lt y \& \phi(x))[/math] и [math]\forall x (x \ge y \vee \phi (x))[/math]


Теорема:
Пусть [math]P_1[/math] и [math]P_2[/math] — рекурсивные отношения. Тогда следующие формулы, задающие некоторые отношения, также являются рекурсивными отношениями:
  1. [math]F(x_1,\dots x_n,z) := \forall_{y\lt z} P_1(x_1,\dots x_n,y)[/math]
  2. [math]E(x_1, \dots x_n,z) := \exists_{y\lt z} P_1(x_1,\dots x_n,y)[/math]
  3. [math]P_1(x_1,\dots x_n) \rightarrow P_2(x_1,\dots x_n)[/math]
  4. [math]P_1(x_1,\dots x_n) \vee P_2(x_1,\dots x_n)[/math]
  5. [math]P_1(x_1,\dots x_n) \& P_2(x_1,\dots x_n)[/math]
  6. [math]\neg P_1(x_1, \dots x_n)[/math]
Доказательство:
[math]\triangleright[/math]
Упражнение.
[math]\triangleleft[/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]


Уточним язык — обяжем всегда писать скобки всегда и только вокруг двуместной операции. В принципе, иначе мы могли бы определить правильно операцию равенства Eq, но это лишние технические сложности.

Научимся записывать выражения в виде чисел. Пусть [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^{c_1} \cdot p_2^{c_2} \cdot \dots \cdot p_n^{c_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^{c_1} \cdot \dots \cdot p_n^{c_n}[/math].

Операцию конкатенации строк [math]s \star t[/math] определим так. Пусть первая строка имеет символы [math]s_1, \dots s_n[/math], а вторая — [math]t_1, \dots t_m[/math]. Тогда результат их конкатенации — [math]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}[/math].

Если в данной записи встретится символ с $ перед ним: "[math] \neg [/math]$[math]x \& y [/math] ", тогда это означает вставку "литерала" (ср. язык Perl) --- интерпретировать это надо как конкатенацию строки до литерала, самого литерала, и строки после литерала. В данном примере --- "[math]\neg[/math]" [math]\star x \star[/math] "[math]\& y[/math]".

Чтобы представить доказательства, мы будем объединять строки вместе так же, как объединяем символы в строки: [math]2^{2^3} \cdot 3^{2^5}[/math] — это последовательность из двух строк, первая — это "(", а вторая — ")".

Теперь мы можем понять, как написать программу, проверяющую корректность доказательства некоторого утверждения в формальной арифметике. Наметим общую идею. Программа будет состоять из набора рекурсивных отношений и функций, каждое из которых выражает некоторое отношение, содержательное для проверки доказательства. Ниже мы покажем идею данной конструкции, приведя несколько из них.

  • Проверка того, что a - геделев номер выражения, являющегося переменной. [math]Var(a) := \exists_{z \lt a} (a = 2 ^ {13 + z})[/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]\triangleright[/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{u_1}, \dots \overline{u_n}, \overline{v})[/math]

По формуле можно построить рекурсивную функцию, [math]C_F (u_1, \dots u_n, v, p)[/math], выражающую тот факт, что [math]p[/math] — геделев номер вывода формулы [math]F(\overline{u_1}, \dots \overline{u_n}, \overline{v})[/math]. Тогда возьмем [math]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[/math]
[math]\triangleleft[/math]