1632
правки
Изменения
м
|about = Первая теорема Геделя о неполноте арифметики
|about = Аналог I теоремы Гёделя о неполноте|statement = В любой "'''достаточно богатой системе" ''' существует истинное недоказуемое утверждение.
|about=Теорема Геделя в форме Россера
|about=Вторая теорема Геделя о неполноте арифметики
rollbackEdits.php mass rollback
[[Категория: Математическая логика]]
==Определения==
{{Определение
|definition=
геделев номер. Тогда рассмотрим формулу <tex>\forall p \neg W_1(\overline{w},p)</tex>
==Первая теорема Геделя о неполноте арифметики==
{{Теорема
|statement=
1. Если формальная арифметика непротиворечива, то недоказуемо <tex>\forall p \neg W_1(\overline{w},p)</tex>.<br>
отрицания этой формулы. Ну и по традиции применим ее к своему номеру <tex>r</tex>.
Внимательное рассмотрение этой ситуации приводит к следующей теореме.
===Аналог I теоремы Гёделя о неполноте===
{{Теорема
|proof =
Поясним, что это значит. Так как любой язык программирования эквивалентен [[Машина Тьюринга | машине Тьюринга]], то всё связанное с ним кодируется в [[Теории первого порядка | логике первого порядка]] с [[Классы_чисел#Аксиомы_Пеано | аксиомами Пеано]] (для этого достаточно, чтобы программа умела прибавлять к числу единицу и вызывать подпрограммы), поэтому можно в терминах программ получать утверждения, эквивалентные тем, что строил Гёдель.
<code>
<tex>p(x){:}</tex>
'''foreach''' <tex>q </tex> <tex> \in ~ \Sigma^* </tex> <span style="color:Green">//перебираем утверждения</span> '''if''' <tex>q </tex> proves "<tex>p(x)</tex> зависает"<span style="color:Green">//если утверждение доказывает зависание программы</span>
'''exit'''
</code>
}}
==Теорема Геделя в форме Россера==
{{Теорема
|statement=
Если формальная арифметика непротиворечива, то
<tex>\neg F</tex> также недоказуемо, если арифметика непротиворечива.
}}
==Вторая теорема Геделя о неполноте арифметики==
{{Теорема
|statement=
Если в формальной арифметике удастся доказать ее непротиворечивость, то
