Непротиворечивость теории

[Someone]

epros в сообщении #168749 писал(а):

Причём под неполнотой понимается существование недоказуемого (и непопровержимого) истинного высказывания.

Под неполнотой понимается существование такого высказывания $A$, что не доказуемы ни $A$, ни $\neg A$.

[epros]

маткиб писал(а):

epros в сообщении #168749 писал(а):

Что же тогда Вы называете первой теоремой Гёделя о неполноте?

Я так полагал, что это - утверждение о принципиальной неполноте любого непротиворечивого расширения арифметики. Причём под неполнотой понимается существование недоказуемого (и непопровержимого) истинного высказывания. И, как я понимаю, доказательство существования такого высказывания обычно заключается именно в его построении (точнее, в указании способа построения).

А можно под неполнотой понимать существование просто недоказуемого и неопровержимого утверждения (без требования истинности), которое уже не обязано быть эквивалентно собственной недоказуемости.

Теоремы в такой формулировке я, увы, не встречал. Нет, я против неё ничего не имею, но хотелось бы получить какие-нибудь подтверждения того, и в такой формулировке терема была доказана (ибо с моей точки зрения это уже совсем другая теорема).

[Someone]

Стефен К.Клини. Введение в метаматематику. "Иностранная литература", Москва, 1957.

§ 42. Теорема Гёделя.

Цитата:

Теорема 28. Если арифметическая формальная система гл. IV (просто) непротиворечива, то не $\vdash A_p(p)$; если эта система $\omega$-непротиворечива, то не $\vdash\neg A_p(p)$. Таким образом, если эта система $\omega$-непротиворечива, то она (просто) неполна, и $A_p(p)$ служит примером неразрешимой формулы. (Теорема Гёделя в первоначальной форме.)

(Простая) непротиворечивость у Клини понимается как невыводимость одновременно двух высказываний $A$ и $\neg A$ (§ 28). $\omega$-непротиворечивость означает, что если выводимо каждое из высказываний $A(0),A(1),A(2),\ldots$, то невыводимо $\neg\forall xA(x)$ (§ 42).

С другой формулой доказывается следующая теорема.

Цитата:

Теорема 29. Если арифметическая формальная система гл. IV (просто) непротиворечива, то не $\vdash A_q(q)$ и не $\vdash\neg A_q(q)$; иначе говоря, если эта система непротиворечива, то она (просто) неполна, и $A_q(q)$ является неразрешимой формулой. (Теорема Гёделя в форме Россера.)

[маткиб]

epros в сообщении #168799 писал(а):

но хотелось бы получить какие-нибудь подтверждения того, и в такой формулировке терема была доказана

Подтверждение:
http://en.wikipedia.org/wiki/Rosser's_trick

(хотя я бы основную идею доказательства попроще изложил)