Можно ли обобщить теорему Гёделя ?

[quex]

Вот появился у меня по вопрос связанный с теоремой Гёделя : если формальная система непротиворечива то можно ли доказать что нельзя доказать утверждение о ее непротиворечивости средствами (аксиомами) этой формальной системы ? То есть можно ли доказать теорему Гёделя аксиомами арифметики ?

[Xaositect]

Если эффективно аксиоматизируемая формальная система, в которой интерпретируется минимальная арифметика(арифметика Робинсона http://en.wikipedia.org/wiki/Robinson_arithmetic подойдет, возможно, что-то еще меньше), не полна и утверждение о ее непротиворечивости является примером недоказуемого и неопровержимого утверждения

[vek88]

Конечно, можно. Для этого достаточно посмотреть на смысл теоремы Геделя (для определенности, о неполноте арифметики) с общих позиций.

Итак, "забудем" о том, что мы рассматриваем формализацию именно арифметики средствами именно финитных формальных систем. В терминах множеств это значит, что мы "забываем" о представлении множества всех арифметических множеств посредством множества всех рекурсивно перечислимых (далее - РП) множеств.

Итак, мы все это "забыли" - оставили только тот факт, что всякое РП множество является арифметическим. Но существует арифметическое множество, которое не является РП множеством. Т.е. попросту говоря, множество всех арифметических множеств является нетривиальным расширением множества всех РП множеств (см. определение арифметичеких и РП множеств).

И тогда "Теорема Геделя о неполноте" очевидна: Если мы представляем (=формализуем) некоторое множество множеств $A$ в более узком множестве множеств $A_0$, то обязательно найдется множество $a \in A$, такое, что $a \notin A_0$.

А почему же так все сложно при обычном изложении теоремы Геделя о неполноте? ИМХО так сложилось исторически.

[Dialectic]

quex в сообщении #400824 писал(а):

Вот появился у меня по вопрос связанный с теоремой Гёделя : если формальная система непротиворечива то можно ли доказать что нельзя доказать утверждение о ее непротиворечивости средствами (аксиомами) этой формальной системы ?

Хм... иметь бы ещё её точную формулировку...
Вторую теорему Геделя можно интерпретировать, как я понимаю так: "если непротиворечивая формальная система, настолько богата, что в неё можно предъявить знакосочетание, которое может быть интерпритированно нами как утверждение о непротиворечивости этой самой системы - то такое знакосочетание – не может быть выведено в этой системе".
Однако, наш Советский математик – А.С. Есенин –Вольпин
обнаружил следующую вещь: он обнаружил такое знакосочетание, которое ТАКЖЕ можно интерпретировать, как утверждение выражающее непротиворечивость системы, но последнее – уже выводимо. Таким образом: свойство того, знакосочетания, которое выражает непротиворечивость системы – не является ещё достаточным условием, для того, чтобы утверждать, что данное знакосочетание не выводится в системе. Требуется указать КОНКРЕТНОЕ знакосочетание. И тогда теорема Геделя правильней бы звучала так: «если в непротиворечивой формальной системе имеются средства, достаточно мощные, чтобы в ней можно было предьявлять различные знакосочетания, которые содержательно выражают мысль о её непротиворечивости – то некоторые из них – не выводимы».
Xaositect, скажите пожалуйста как специалист- я правильно понимаю дело? Ничего не напутал?

[quex]

Интересно , получается доказать непротиворечивость какой-то системы аксиом ее же средствами невозможно , но можно доказать что это действительно так ( то есть доказать теорему Геделя средствами этой системы аксиом уже можно ). Все правильно ?