помогите понять т Геделя о неполноте

[kefi]

Как я понял отсюда есть две теоремы :
1. Для любой непротиворечивой системы аксиом существует недоказуемое и неопровержимое с ее помощью высказывание .
2. Для любой непротиворечивой системы аксиом нельзя с ее помощью доказать ее непротиворечивость.

Вопросы такие :

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

- вообще - теоремы Г о неполноте справедливы для любой формальной системы ? Если да, то - почему, вроде как, он для арифметики только выводил их ?

[ИСН]

Для любой непротиворечивой системы аксиом, достаточно жирной, чтобы в ней можно было переформулировать арифметику...

[Sonic86]

Мендельсон Матлогика. Читайте, просвещайтесь.
Есть и научпоп версии, формулировки без формул почти.

kefi в сообщении #558275 писал(а):

- вообще - теоремы Г о неполноте справедливы для любой формальной системы ? Если да, то - почему, вроде как, он для арифметики только выводил их ?

Он их сначала в арифметике выводил, а потом вывод уже перенесли на достаточно широкий класс теорий.

[kefi]

2 Sonic86 > Да прежде, чем засесть на годы обучения логике и всем с ней связанным, хотелось бы понять кое-что навскидку .
Что такое более широкий класс теорий - Там кроме арифметики еще что-то допускается - или это вообще любые формальные аксиоматические теории подразумеваются ?

Вообще основной - первый вопрос из стартового поста хотелось бы понять ?

[Maslov]

kefi в сообщении #558275 писал(а):

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

Теорема Геделя о неполноте арифметики сводится к существованию в формальной теории, аксиоматизирующей арифметику, такой формулы, что ни она сама, ни ее отрицание не являются теоремами (не могут быть выведены в) данной теории; причем эта формула является истинной. Противоречивость истинной формулы доказать в рамках непротиворечивой теории нельзя. По-моему, так :)

kefi в сообщении #558289 писал(а):

Что такое более широкий класс теорий - Там кроме арифметики еще что-то допускается - или это вообще любые формальные аксиоматические теории подразумеваются ?

Подразумеваются любые формальные теории, допускающие аксиоматизацию арифметики. Существуют более простые теории, в которых теорема о неполноте не выполняется. Например, в классическом исчислении высказываний любая тавтология (истинная формула) является выводимой. По-моему, так :)

[kefi]

Maslov в сообщении #558321 писал(а):

причем эта формула является истинной. Противоречивость истинной формулы доказать в рамках непротиворечивой теории нельзя. По-моему, так :)

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

[Maslov]

kefi в сообщении #558328 писал(а):

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

Истинная формула формальной теории -- это формула, истинная в любой интерпретации этой теории.

kefi в сообщении #558328 писал(а):

И еще - из истинности высказывания следует его непротиворечивость ?

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

[Sonic86]

kefi в сообщении #558289 писал(а):

Что такое более широкий класс теорий - Там кроме арифметики еще что-то допускается - или это вообще любые формальные аксиоматические теории подразумеваются ?

Ну Вам же ИСН написал:

ИСН в сообщении #558277 писал(а):

Для любой непротиворечивой системы аксиом, достаточно жирной, чтобы в ней можно было переформулировать арифметику...

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

kefi в сообщении #558275 писал(а):

1. Для любой непротиворечивой системы аксиом существует недоказуемое и неопровержимое с ее помощью высказывание .

неверно (например, исчисление высказываний)
Боюсь только, что я неточно выразился.

[kefi]

Maslov писал(а):

Не могу понять в рамках теоремы - откуда известно, что формула является истинной ?Истинная формула формальной теории -- это формула, истинная в любой интерпретации этой теории.

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

[apriv]

kefi в сообщении #558275 писал(а):

Для любой непротиворечивой системы аксиом нельзя с ее помощью доказать ее непротиворечивость.

Не вполне так. Во-первых, нужна оговорка про то, что система должна в каком-то смысле «содержать арифметику». Во-вторых, точная формулировка такая: «существует предложение, которое выражает непротиворечивость системы и которое недоказуемо в рамках этой системы». Это не то же самое.

[Maslov]

kefi в сообщении #558512 писал(а):

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

Речь идет не о любой формуле, а о вполне конкретной, которую Гедель использовал для доказательства неполноты арифметики, а именно, формулы, содержащей утверждение о своей собственной невыводимости. Эта формула с неизбежностью истинна, т. к. если она ложна (и следовательно, выводима), то получим противоречивую арифметику (ибо в ней оказывается выводимой ложная формула), что уже совсем никуда не годится :)

Дальше читайте сами.

Мендельсона Вам уже советовали.
"Игошин В. Математическая логика и теория алгоритмов" -- тоже неплохой учебник, и задачник к нему есть.

А вот тут (http://www.mathnet.ru/php/presentation. ... sentid=105) лекция о теореме Геделя, прочитанная в летней школе «Современная математика» (г. Дубна)

И вот еще оттуда же: http://www.mathnet.ru/php/presentation. ... n_lang=rus

[Solaris L86]

Или скачайте брошурку В. А. Успенского: ЗДЕСЬ

Solaris L86, устное замечание за использование красного цветовыделения. Убрал. /Toucan

[Профессор Снэйп]

kefi в сообщении #558275 писал(а):

Для любой непротиворечивой системы аксиом существует недоказуемое и неопровержимое с ее помощью высказывание .

Это неверно!

Такое высказывание (точнее, формула первого порядка без свободных переменных) существует для любой непротиворечивой алгоритмически перечислимой и совместной с аксиомами арифметики Пеано системы аксиом.

То, что Вы пропустили, я выделил жирным шрифтом. Это очень важные уточнения.

Насчёт совместности с арифметикой Пеано - оно естественно. Теорема Гёделя - она ведь о неполноте чего? О неполноте арифметики А Вы в своей "формулировке" арифметику вообще никак не упоминаете!

Насчёт алгоритмической перечислимости... Ну вот возьмите множество всех предложений, истинных на натуральном ряде, и объявите его множеством аксиом. Будет полученная система аксиом полной?

[kefi]

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

[Sonic86]

kefi в сообщении #558666 писал(а):

требуют условие того, что формула должна содержать утверждение о своей собственной невыводимости

Это не условие. Это конкретная формула в теореме Геделя так строится. Т.е. если формула истинна, то в общем случае не факт, что она должна каким-то неведомым образом содержать утверждение о своей невыводимости, а в теореме Геделя именно так.

Блин, я Вам все-таки выпишу кусок из Мендельсона, в упрощенном виде... Только подождите...
Берется конкретная система аксиом для арифметики, напоминающая аксиомы Пеано. Далее, производится арифметизация теории: несложными приемами нумеруются все переменные, термы, выражения, формулы, выводы (т.е. у каждого объекта - свой номер - гёделев номер ГН, но не всякое число - ГН объекта). Для простых предикатов "$x$ - ГН константы теории", "$x$ - ГН функциональной буквы теории", "$x$ - ГН предикатной буквы теории" строятся явно их арифметические формулы (например, "$x$ - ГН переменной" выражается формулой $\exists z _{z<x} (1 \leqslant z \& x=2^{5+8z})$), причем они примитивно-рекурсивны. И поехало: мы, комбинируя простые отношения и выражающие их формулы, явно конструируем арифметические формулы для отношений "$x$ - ГН терма", "$x$ - ГН формулы теории", "$x$ - ГН частного случая схемы аксиом такой-то", "$x$ - ГН такого-то вывода (доказательства) в данной теории" и отношение $W_1(u,y)$ - "$u$ - ГН формулы $\mathcal{A}(x_1)$ со свободной переменной $x_1$, а $y$ - ГН вывода $\mathcal{A}(u)$".
Берем отношение $W_1(u,y)$ - оно выразимо некоторой формулой $\mathcal{W}_1(x_1,x_2)$ теории от $x_1,x_2$. Т.е. если $W_1(k_1,k_2)$ истинно, то $\vdash \mathcal{W}_1(k_1,k_2)$. Теперь берем формулу $\forall x_2 \neg\mathcal{W}_1(x_1,x_2)$, пусть $m$ - ее ГН, и берем утверждение (без свободных переменных) $\forall x_2 \neg\mathcal{W}_1(m,x_2)(**)$. Теорема Гёделя утверждает, что если теория (арифметика) непротиворечива, то сама формула $(**)$ невыводима и ее отрицание $\neg (**)$ невыводимо.
Действительно, предположим, что теория непротиворечива, и формула $(**)$ $\forall x_2 \neg\mathcal{W}_1(m,x_2)$ выводима. $k$ - ГН этого вывода, то по смыслу $W_1$ будет верно $W_1(m,k)$, но так как $\mathcal{W}_1$ выражает $W_1$, то $\vdash \mathcal{W}_1(m,k)$. С другой стороны, если верна $\forall x_2 \neg\mathcal{W}_1(m,x_2)$, то она верна и для $x_2=k$ $\neg\mathcal{W}_1(m,k)$ - получается, что мы вывели $(**)$ и $\neg (**)$, что противоречит предположению, о непротиворечивости теории.
С другой стороны, если выводима \neg $(**)$ и теория непротиворечива, то $(**)$ невыводима, поэтому $W_1(m,n)$ ложно для любого натурального $n$. А это значит, что $\vdash \neg\mathcal{W}_1(m,n)$. Возьмем в качестве $\mathcal (x_2)$ формулу $\neg\mathcal{W}_1(m,x_2)$ - получим, что не $\vdash \exists x_2 \neg\neg\mathcal{W}_1(m,x_2)$ - а это противоречит \neg $(**)$.

Мендельсон писал(а):

Весьма любопытна стандартная интерпретация неразрешимого пред-
предложения $(**)$: $\forall x_2 \neg\mathcal{W}_1(m,x_2)$. Так как $\mathcal{W}_1$ выражает в $S$ отношение $W_1$, то, в соответствии со стандартной интерпретацией, $(**)$ утверждает, что $W_1(m, x_2)$ ложно для каждого натурального числа $х_2$. Согласно (I) (т.е. определению $W_1$), это означает, что не существует вывода формулы $(**)$ в $S$. Другими словами, формула $(**)$ утверждает свою собственную невыводимость в $S$. По теореме же Гёделя, если только теория $S$ непротиворечива, эта формула и в самом деле невыводима в $S$ и потому истинна при
стандартной интерпретации. Итак, для натуральных чисел, соответствующих обычной интерпретации, формула $(**)$ верна, но в $S$ невыводима.

З.Ы. Вот я скачал из интернетов книгу Нагель Ньюман Теорема Геделя. Это научпоп, формул нет почти, но я сам не читал (и читал у какого-то E.G.A. в интернете и у Сингха ВТФ). Попробуйте ее прочесть.