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

==Вторая теорема Геделя о неполноте арифметики==
{{Теорема
|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>. 
Однако, существование такого доказательства влечет за собой противоречивость формальной арифметики.
}}

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