313
правок
Изменения
Нет описания правки
[[Лекция 8 Геделева нумерация. Арифметизация доказательств | <<]][[Лекция 10 Теория множеств | >>]] [[Категория: В разработке]]
[[Категория: Математическая логика]]
= 1я и 2я теоремы Геделя о неполноте арифметики =Определения==
{{Определение
|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 теоремы Гёделя о неполноте===
{{Теорема
|statement = В любой '''достаточно богатой системе''' существует истинное недоказуемое утверждение.
|proof =
Поясним, что это значит. Так как любой язык программирования эквивалентен [[Машина Тьюринга | машине Тьюринга]], то всё связанное с ним кодируется в [[Теории первого порядка | логике первого порядка]] с [[Классы_чисел#Аксиомы_Пеано | аксиомами Пеано]] (для этого достаточно, чтобы программа умела прибавлять к числу единицу и вызывать подпрограммы), поэтому можно в терминах программ получать утверждения, эквивалентные тем, что строил Гёдель.
Можно переформулировать теорему следующим образом: невозможно доказать, что <tex> p(x) = \perp </tex>.
Тогда напишем такую программу:
<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=
Если в формальной арифметике удастся доказать ее непротиворечивость, то
