39
правок
Изменения
Нет описания правки
[[Категория: Математическая логика]]
= 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>
{{Теорема
|about = Первая теорема Геделя о неполноте арифметики
|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>.
Внимательное рассмотрение этой ситуации приводит к следующей теореме.
{{Теорема
|about=Теорема Геделя в форме Россера
|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> также недоказуемо, если арифметика непротиворечива.
}}
{{Теорема
|about=Вторая теорема Геделя о неполноте арифметики
|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>.
Однако, существование такого доказательства влечет за собой противоречивость формальной арифметики.
}}
Последним в данном разделе заметим, что данные доказательства естественно
обобщаются на случай произвольной формальной теории, включающей формальную
арифметику. Достаточно только расширить правила, проверяющие доказательства
формул на корректность (т.е. добавить в них новые аксиомы, схемы аксиом,
и правила или схемы правил вывода).
