Редактирование: 1я и 2я теоремы Геделя о неполноте арифметики

[[Геделева нумерация. Арифметизация доказательств | <<]][[Теория множеств | >>]]

[[Категория: Математическая логика]]
==Определения==
{{Определение 
|definition=
Мы будем называть теорию непротиворечивой, если
не найдется такой формулы <tex>F</tex>, что доказуемо как <tex>F</tex>, так и <tex>\neg F</tex>.
}}

{{Лемма
|statement=
Если теория противоречива, то в ней доказуемо любая формула.
|proof=
Если теория противоречива, то в ней есть утверждение <tex>F</tex>, что доказуемо <tex>F</tex> и <tex>\neg F</tex>.
Воспользуемся доказуемой формулой <tex>\neg F \rightarrow F \rightarrow \beta</tex>.
}}

{{Определение
|definition=
Мы будем называть теорию <tex>\omega</tex>-непротиворечивой,
если, какова бы ни была формула <tex>P(x)</tex> со свободной переменной <tex>x</tex>, 
такая, что для любого натурального числа <tex>p</tex> доказуемо <tex>P(p)</tex>, 
то формула <tex>\exists p \neg P(p)</tex> недоказуема.
}}

{{Лемма
|statement=
<tex>\omega</tex>-непротиворечивость влечет непротиворечивость.
|proof=
Рассмотрим выводимую формулу <tex>x=x \rightarrow x=x</tex>.
При подстановке любого натурального числа вместо <tex>x</tex>
формула будет по-прежнему выводима: <tex>\overline{k} = \overline{k} \rightarrow \overline{k}=\overline{k}</tex>.
Значит, по <tex>\omega</tex>-непротиворечивости формула <tex>\exists p \neg (x=x \rightarrow x=x)</tex> невыводима.
Значит, теория непротиворечива (поскольку в противоречивой теории выводится любая формула).
}}

Пусть формула <tex>F</tex> со свободной переменной «x» имеет геделев номер <tex>f</tex>. 
Тогда определим рекурсивное отношение <tex>W_1</tex>, такое, что <tex>W_1(f,p)</tex> 
истинно тогда и только тогда, когда <tex>p</tex> есть геделев номер 
доказательства <tex>F(f)</tex>, то есть доказательства самоприменения <tex>F</tex>. То есть в некотором
приближении это будет формула вида:

<tex>W_1(f,p) := Free(f,</tex>«<tex>x</tex>»<tex>) \& Proof (Sub(f,</tex>«<tex>x</tex>»<tex>,Num(f)),p)</tex>.

Рассмотрим формулу <tex>\forall p \neg W_1(f,p)</tex>. Пусть <tex>w</tex> — ее 
геделев номер. Тогда рассмотрим формулу <tex>\forall p \neg W_1(\overline{w},p)</tex>

==Первая теорема Геделя о неполноте арифметики==
{{Теорема
|statement=
1. Если формальная арифметика непротиворечива, то недоказуемо <tex>\forall p \neg W_1(\overline{w},p)</tex>.<br>
2. Если формальная арифметика <tex>\omega</tex>-непротиворечива, то недоказуемо <tex>\neg \forall p \neg W_1(\overline{w},p)</tex>.
|proof=
1. Пусть формула <tex>\forall p \neg W_1(\overline{w},p)</tex> доказуема. Тогда найдется геделев номер ее 
доказательства <tex>p</tex>, и значит <tex>W_1(\overline{w},\overline{p})</tex>. С другой стороны, по схеме аксиом для квантора 
всеобщности и правилу Modus Ponens из предположения можно показать <tex>\neg W_1(\overline{w},\overline{p})</tex>. Значит, 
получается, что формальная арифметика противоречива, что не соответствует предположению.

2. Пусть <tex>\vdash \neg \forall p \neg W_1 (\overline{w},p)</tex>. 
Значит, <tex>\vdash \exists p W_1 (\overline{w},p)</tex>. 
Значит, по <tex>\omega</tex>-непротиворечивости найдется такое натуральное число <tex>p</tex>, что
<tex>\vdash W_1(\overline{w},\overline{p})</tex>: иначе, если <tex>\vdash \neg W_1 (\overline{w},\overline{p})</tex> 
для любого натурального <tex>p</tex>, то по <tex>\omega</tex>-непротиворечивости <tex>\exists p \neg \neg W_1(\overline{w},p)</tex> недоказуемо
(напомним, что <tex>W_1</tex> выразимо в формальной арифметике, значит, для любой пары <tex>f</tex> и <tex>p</tex> мы должны иметь 
либо доказательство <tex>W_1(\overline{f},\overline{p})</tex>, либо доказательство отрицания этого).

Раз найдется <tex>p</tex>, что <tex>W_1(w,p)</tex>, то <tex>\vdash \forall p \neg W_1 (w,p)</tex>.
А, значит, доказуемо и <tex>\neg \exists p \neg \neg W_1 (w,p)</tex>. Значит, формальная
арифметика противоречива, что невозможно в силу предположения о ее 
<tex>\omega</tex>-непротиворечивости.
}}

Формула <tex>\forall p \neg W_1(w,p)</tex>, говоря простым языком, утверждает 
собственную недоказуемость. Мы показали, что эта формула (при условии 
<tex>\omega</tex>-непротиворечивости формальной арифметики) действительно 
недоказуема — а, значит, верна. Таким образом, мы нашли некоторое
выражение в формальной арифметике, которое истинно, но недоказуемо,
и тем самым показали, что если формальная арифметика <tex>\omega</tex>-непротиворечива, 
то она неполна.

В данном рассуждении используется сложное понятие
<tex>\omega</tex>-непротиворечивости, что смущает. Теорема Геделя в форме 
Россера снимает эту сложность.

Рассмотрим отношение <tex>W_2 (f,p)</tex> — <tex>f</tex> и <tex>p</tex> состоят в отношении <tex>W_2</tex> тогда и только тогда, когда
<tex>p</tex> — геделев номер доказательства ''отрицания'' самоприменения <tex>f</tex> (если <tex>F</tex> — формула с
геделевым номером <tex>f</tex>, то <tex>p</tex> — номер доказательства <tex>\neg F(f)</tex>). Мы можем определить его 
аналогично <tex>W_1 (w,p)</tex>.

Тогда рассмотрим такую формулу <tex>R(a)</tex>: <tex>\forall x (W_1 (a,x) \rightarrow \exists y (y < x \& W_2 (a,y)))</tex>.
Неформальным языком она утверждает, что для любого доказательства самоприменения некоторой 
формулы с номером <tex>a</tex> найдется доказательство (да еще и с меньшим геделевым номером) 
отрицания этой формулы. Ну и по традиции применим ее к своему номеру <tex>r</tex>. 
Внимательное рассмотрение этой ситуации приводит к следующей теореме.
===Аналог I теоремы Гёделя о неполноте===
{{Теорема
|statement = В любой '''достаточно богатой системе''' существует истинное недоказуемое утверждение.
|proof =
Поясним, что это значит. Так как любой язык программирования эквивалентен [[Машина Тьюринга | машине Тьюринга]], то всё связанное с ним кодируется в [[Теории первого порядка | логике первого порядка]] с [[Классы_чисел#Аксиомы_Пеано | аксиомами Пеано]] (для этого достаточно, чтобы программа умела прибавлять к числу единицу и вызывать подпрограммы), поэтому можно в терминах программ получать утверждения, эквивалентные тем, что строил Гёдель.

Можно переформулировать теорему следующим образом: невозможно доказать, что <tex> p(x) = \perp </tex>.

Тогда напишем такую программу:
<code>
  <tex>p(x){:}</tex>
    '''foreach''' <tex>q</tex> <tex> \in ~ \Sigma^* </tex>
      '''if''' <tex>q</tex> proves "<tex>p(x)</tex> зависает"
        '''exit'''    
</code>
}}
==Теорема Геделя в форме Россера==
{{Теорема
|statement=
Если формальная арифметика непротиворечива, то 
найдется такая формула <tex>F</tex>, что как она сама, так и ее отрицание
недоказуемы.
|proof=
Обозначим геделев номер <tex>R</tex> за <tex>r</tex>. В качестве формулы <tex>F</tex> возьмем формулу <tex>R(r)</tex>.

Рассмотрим варианты. Пусть <tex>F</tex> доказуемо, т.е. <tex>R(r)</tex> истинно, 
т.е. <tex>\forall x (W_1 (\overline{r},x) \rightarrow \exists y (y < x \& W_2 (\overline{r},y)))</tex>
истинно. Значит, есть такой <tex>x</tex>, что <tex>\exists y (y < x \& W_2 (\overline{r},y))</tex> истинно.
Значит, найдется такой <tex>y</tex>, что <tex>W_2 (\overline{r},y)</tex>, т.е., что существует опровержение
<tex>r</tex> с меньшим номером. Поэтому формула <tex>R(r)</tex> истинной, а значит и доказуемой,
быть не может.

Пусть докауземо <tex>\neg F</tex>. Пусть <tex>p</tex> — геделев номер доказательства.
Раз так, то <tex>W_2 (r,p)</tex> истинно. По непротиворечивости формальной арифметики
это значит, что <tex>W_1 (r,x)</tex> при любом <tex>x</tex> ложно (иначе окажется, что 
найдутся как доказательство, так и опровержение <tex>R(r)</tex>). Поскольку
отношение <tex>W_1 (r,x)</tex> выразимо в формальной арифметике, то
доказуемо <tex>\neg W_1 (\overline{r},\overline{x})</tex> при любом <tex>x</tex> (т.е. никакой из <tex>x</tex> не является
доказательством <tex>R(r)</tex>). Как частный случай, <tex>\neg W_1 (\overline{r},\overline{x})</tex> доказуемо для
всех <tex>x</tex>, не превышающих <tex>p</tex>, поэтому доказуемо 
<tex>\neg W_1 (\overline{r},1) \& \neg W_1 (\overline{r},2) \& ... \& \neg W_1 (\overline{r},\overline{p})</tex>.
Отсюда можно показать доказуемость формулы <tex>x \le p \rightarrow \neg W_1 (\overline{r},x)</tex>.
Обозначим эту формулу за <tex>P_\le(x)</tex>.

Рассмотрим формулу <tex>(x \ge p) \rightarrow \exists y (y \le x \& W_2 (\overline{r},y))</tex>
Формула утверждает следующее: «если некоторый <tex>x</tex> больше чем <tex>p</tex>, то найдется
такой <tex>y</tex>, меньший <tex>x</tex>, что <tex>W_2 (r,y)</tex>». Очевидно, что данная формула истинна,
ведь если мы возьмем <tex>p</tex> в качестве такого <tex>y</tex>, то <tex>W_2 (r,p)</tex> истинно 
по предположению.  Обозначим рассмотренную формулу за <tex>P_\ge(x)</tex> и заметим, 
что она также доказуема.

Легко показать, что из этих утверждений и из того, что <tex>x \le p \vee x \ge p</tex>,
можно вывести <tex>\neg W_1 (\overline{r},x) \vee \exists y (y < x \& W_2 (\overline{r},y))</tex>,
а отсюда — <tex>\forall x (W_1 (\overline{r},x) \rightarrow \exists y (y < x \& W_2 (\overline{r},y)))</tex>,
то есть <tex>F</tex>. Однако, мы предположили доказуемость <tex>\neg F</tex>, и исходя из него,
вывели <tex>F</tex>, т.е. показали противоречивость формальной арифметики. Значит, 
<tex>\neg F</tex> также недоказуемо, если арифметика непротиворечива.
}}
==Вторая теорема Геделя о неполноте арифметики==
{{Теорема
|statement=
Если в формальной арифметике удастся доказать ее непротиворечивость, то
на основании этого доказательства можно построить противоречие в формальной
арифметике.
|proof=
Рассмотрим только схему доказательства. Возьмем <tex>Consis</tex>, некоторое 
утверждение, которое показывает непротиворечивость арифметики, т.е. 
показывает отсутствие такой формулы <tex>S</tex>, что и <tex>S</tex> и <tex>\neg S</tex> доказуемы
(его можно выписать:
<tex>\forall s ((\forall p \neg Proof (s,p)) \vee (\forall p \neg Proof (</tex>«<tex>\neg \$s</tex>»<tex>, p)))</tex>)

Тогда рассмотрим формулу <tex>Consis \rightarrow (\forall p \neg W_1(\overline{w},p))</tex>.
Данная формула в точности соответствует условию 1й теоремы Геделя 
о неполноте арифметики (если формальная арифметика непротиворечива, 
то <tex>\forall p \neg W_1(\overline{w},p)</tex> недоказуемо; напомним, что <tex>w</tex> ведь и есть
геделев номер формулы <tex>\forall p \neg W_1(x,p)</tex> со свободной переменной <tex>x</tex>).
Рассуждение, доказывающее 1ю теорему, можно формализовать, получив доказательство
данной импликации. Теперь, если у нас будет доказательство утверждения <tex>Consis</tex>,
то по правилу Modus Ponens мы также получаем доказательство утверждения <tex>(\forall p \neg W_1(\overline{w},p))</tex>. 
Однако, существование такого доказательства влечет за собой противоречивость формальной арифметики.
}}

Последним в данном разделе заметим, что данные доказательства естественно
обобщаются на случай произвольной формальной теории, включающей формальную
арифметику. Достаточно только расширить правила, проверяющие доказательства
формул на корректность (т.е. добавить в них новые аксиомы, схемы аксиом,
и правила или схемы правил вывода).