313
правок
Изменения
Нет описания правки
отрицания этой формулы. Ну и по традиции применим ее к своему номеру <tex>r</tex>.
Внимательное рассмотрение этой ситуации приводит к следующей теореме.
{{Теорема
|about = Аналог I теоремы Гёделя о неполноте
|statement = В любой "достаточно богатой системе" существует истинное недоказуемое утверждение.
|proof =
Поясним, что это значит. Так как любой язык программирования эквивалентен [[Машина Тьюринга | машине Тьюринга]], то всё связанное с ним кодируется в [[Теории первого порядка | логике первого порядка]] с [[Классы_чисел#Аксиомы_Пеано | аксиомами Пеано]] (для этого достаточно, чтобы программа умела прибавлять к числу единицу и вызывать подпрограммы), поэтому можно в терминах программ получать утверждения, эквивалентные тем, что строил Гёдель.
Можно переформулировать теорему следующим образом: невозможно доказать, что <tex> p(x) = \perp </tex>.
Тогда напишем такую программу:
<code>
p(x):
'''foreach''' q <tex> \in ~ \Sigma^* </tex>
'''if''' q proves "p(x) зависает"
exit
</code>
}}
{{Теорема
