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

<< >>

Определение:

Мы будем называть теорию непротиворечивой, если не найдется такой формулы [math]F[/math], что доказуемо как [math]F[/math], так и [math]\neg F[/math].

Лемма:

Если теория противоречива, то в ней доказуемо любая формула.

Доказательство:

[math]\triangleright[/math]

Если теория противоречива, то в ней есть утверждение [math]F[/math], что доказуемо [math]F[/math] и [math]\neg F[/math]. Воспользуемся доказуемой формулой [math]\neg F \rightarrow F \rightarrow \beta[/math].

[math]\triangleleft[/math]

Определение:

Мы будем называть теорию [math]\omega[/math]-непротиворечивой, если, какова бы ни была формула [math]P(x)[/math] со свободной переменной [math]x[/math], такая, что для любого натурального числа [math]p[/math] доказуемо [math]P(p)[/math], то формула [math]\exists p \neg P(p)[/math] недоказуема.

Лемма:

[math]\omega[/math]-непротиворечивость влечет непротиворечивость.

Доказательство:

[math]\triangleright[/math]

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

[math]\triangleleft[/math]

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

[math]W_1(f,p) := Free(f,[/math]«[math]x[/math]»[math]) \& Proof (Sub(f,[/math]«[math]x[/math]»[math],Num(f)),p)[/math].

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

Теорема (Первая теорема Геделя о неполноте арифметики):

1. Если формальная арифметика непротиворечива, то недоказуемо [math]\forall p \neg W_1(\overline{w},p)[/math]. 2. Если формальная арифметика [math]\omega[/math]-непротиворечива, то недоказуемо [math]\neg \forall p \neg W_1(\overline{w},p)[/math].

Доказательство:

[math]\triangleright[/math]

1. Пусть формула [math]\forall p \neg W_1(\overline{w},p)[/math] доказуема. Тогда найдется геделев номер ее доказательства [math]p[/math], и значит [math]W_1(\overline{w},\overline{p})[/math]. С другой стороны, по схеме аксиом для квантора всеобщности и правилу Modus Ponens из предположения можно показать [math]\neg W_1(\overline{w},\overline{p})[/math]. Значит, получается, что формальная арифметика противоречива, что не соответствует предположению. 2. Пусть [math]\vdash \neg \forall p \neg W_1 (\overline{w},p)[/math]. Значит, [math]\vdash \exists p W_1 (\overline{w},p)[/math]. Значит, по [math]\omega[/math]-непротиворечивости найдется такое натуральное число [math]p[/math], что [math]\vdash W_1(\overline{w},\overline{p})[/math]: иначе, если [math]\vdash \neg W_1 (\overline{w},\overline{p})[/math] для любого натурального [math]p[/math], то по [math]\omega[/math]-непротиворечивости [math]\exists p \neg \neg W_1(\overline{w},p)[/math] недоказуемо (напомним, что [math]W_1[/math] выразимо в формальной арифметике, значит, для любой пары [math]f[/math] и [math]p[/math] мы должны иметь либо доказательство [math]W_1(\overline{f},\overline{p})[/math], либо доказательство отрицания этого). Раз найдется [math]p[/math], что [math]W_1(w,p)[/math], то [math]\vdash \forall p \neg W_1 (w,p)[/math]. А, значит, доказуемо и [math]\neg \exists p \neg \neg W_1 (w,p)[/math]. Значит, формальная арифметика противоречива, что невозможно в силу предположения о ее [math]\omega[/math]-непротиворечивости.

[math]\triangleleft[/math]

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

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

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

Тогда рассмотрим такую формулу [math]R(a)[/math]: [math]\forall x (W_1 (a,x) \rightarrow \exists y (y \lt x \& W_2 (a,y)))[/math]. Неформальным языком она утверждает, что для любого доказательства самоприменения некоторой формулы с номером [math]a[/math] найдется доказательство (да еще и с меньшим геделевым номером) отрицания этой формулы. Ну и по традиции применим ее к своему номеру [math]r[/math]. Внимательное рассмотрение этой ситуации приводит к следующей теореме.

Теорема (Аналог I теоремы Гёделя о неполноте):

В любой "достаточно богатой системе" существует истинное недоказуемое утверждение.

Доказательство:

[math]\triangleright[/math]

Поясним, что это значит. Так как любой язык программирования эквивалентен машине Тьюринга, то всё связанное с ним кодируется в логике первого порядка с аксиомами Пеано (для этого достаточно, чтобы программа умела прибавлять к числу единицу и вызывать подпрограммы), поэтому можно в терминах программ получать утверждения, эквивалентные тем, что строил Гёдель. Можно переформулировать теорему следующим образом: невозможно доказать, что [math] p(x) = \perp [/math]. Тогда напишем такую программу: p(x): foreach q [math] \in ~ \Sigma^* [/math] if q proves "p(x) зависает" exit

[math]\triangleleft[/math]

Теорема (Теорема Геделя в форме Россера):

Если формальная арифметика непротиворечива, то найдется такая формула [math]F[/math], что как она сама, так и ее отрицание недоказуемы.

Доказательство:

[math]\triangleright[/math]

Обозначим геделев номер [math]R[/math] за [math]r[/math]. В качестве формулы [math]F[/math] возьмем формулу [math]R(r)[/math]. Рассмотрим варианты. Пусть [math]F[/math] доказуемо, т.е. [math]R(r)[/math] истинно, т.е. [math]\forall x (W_1 (\overline{r},x) \rightarrow \exists y (y \lt x \& W_2 (\overline{r},y)))[/math] истинно. Значит, есть такой [math]x[/math], что [math]\exists y (y \lt x \& W_2 (\overline{r},y))[/math] истинно. Значит, найдется такой [math]y[/math], что [math]W_2 (\overline{r},y)[/math], т.е., что существует опровержение [math]r[/math] с меньшим номером. Поэтому формула [math]R(r)[/math] истинной, а значит и доказуемой, быть не может. Пусть докауземо [math]\neg F[/math]. Пусть [math]p[/math] — геделев номер доказательства. Раз так, то [math]W_2 (r,p)[/math] истинно. По непротиворечивости формальной арифметики это значит, что [math]W_1 (r,x)[/math] при любом [math]x[/math] ложно (иначе окажется, что найдутся как доказательство, так и опровержение [math]R(r)[/math]). Поскольку отношение [math]W_1 (r,x)[/math] выразимо в формальной арифметике, то доказуемо [math]\neg W_1 (\overline{r},\overline{x})[/math] при любом [math]x[/math] (т.е. никакой из [math]x[/math] не является доказательством [math]R(r)[/math]). Как частный случай, [math]\neg W_1 (\overline{r},\overline{x})[/math] доказуемо для всех [math]x[/math], не превышающих [math]p[/math], поэтому доказуемо [math]\neg W_1 (\overline{r},1) \& \neg W_1 (\overline{r},2) \& ... \& \neg W_1 (\overline{r},\overline{p})[/math]. Отсюда можно показать доказуемость формулы [math]x \le p \rightarrow \neg W_1 (\overline{r},x)[/math]. Обозначим эту формулу за [math]P_\le(x)[/math]. Рассмотрим формулу [math](x \ge p) \rightarrow \exists y (y \le x \& W_2 (\overline{r},y))[/math] Формула утверждает следующее: «если некоторый [math]x[/math] больше чем [math]p[/math], то найдется такой [math]y[/math], меньший [math]x[/math], что [math]W_2 (r,y)[/math]». Очевидно, что данная формула истинна, ведь если мы возьмем [math]p[/math] в качестве такого [math]y[/math], то [math]W_2 (r,p)[/math] истинно по предположению. Обозначим рассмотренную формулу за [math]P_\ge(x)[/math] и заметим, что она также доказуема. Легко показать, что из этих утверждений и из того, что [math]x \le p \vee x \ge p[/math], можно вывести [math]\neg W_1 (\overline{r},x) \vee \exists y (y \lt x \& W_2 (\overline{r},y))[/math], а отсюда — [math]\forall x (W_1 (\overline{r},x) \rightarrow \exists y (y \lt x \& W_2 (\overline{r},y)))[/math], то есть [math]F[/math]. Однако, мы предположили доказуемость [math]\neg F[/math], и исходя из него, вывели [math]F[/math], т.е. показали противоречивость формальной арифметики. Значит, [math]\neg F[/math] также недоказуемо, если арифметика непротиворечива.

[math]\triangleleft[/math]

Теорема (Вторая теорема Геделя о неполноте арифметики):

Если в формальной арифметике удастся доказать ее непротиворечивость, то на основании этого доказательства можно построить противоречие в формальной арифметике.

Доказательство:

[math]\triangleright[/math]

Рассмотрим только схему доказательства. Возьмем [math]Consis[/math], некоторое утверждение, которое показывает непротиворечивость арифметики, т.е. показывает отсутствие такой формулы [math]S[/math], что и [math]S[/math] и [math]\neg S[/math] доказуемы (его можно выписать: [math]\forall s ((\forall p \neg Proof (s,p)) \vee (\forall p \neg Proof ([/math]«[math]\neg \$s[/math]»[math], p)))[/math]) Тогда рассмотрим формулу [math]Consis \rightarrow (\forall p \neg W_1(\overline{w},p))[/math]. Данная формула в точности соответствует условию 1й теоремы Геделя о неполноте арифметики (если формальная арифметика непротиворечива, то [math]\forall p \neg W_1(\overline{w},p)[/math] недоказуемо; напомним, что [math]w[/math] ведь и есть геделев номер формулы [math]\forall p \neg W_1(x,p)[/math] со свободной переменной [math]x[/math]). Рассуждение, доказывающее 1ю теорему, можно формализовать, получив доказательство данной импликации. Теперь, если у нас будет доказательство утверждения [math]Consis[/math], то по правилу Modus Ponens мы также получаем доказательство утверждения [math](\forall p \neg W_1(\overline{w},p))[/math]. Однако, существование такого доказательства влечет за собой противоречивость формальной арифметики.

[math]\triangleleft[/math]

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