Недоказуемое

[nasldfhgon]

Вот Кантор, например, долго мучился пытаясь доказать континуум-гипотезу. В итоге только нервы себе потрепал, так ничего и не доказав. Как выяснилось позже, ее вообще нельзя ни доказать, ни опровергнуть в ZFC, т.е. она недоказуема. Теперь же, перед математиками стоит другой вопрос: противоречива или нет ZFC? Многие пытаются доказать ее непротиворечивость уже много лет и так ничего не выходит. Это меня натолкнуло на мысль, что, возможно, непротиворечивость ZFC недоказума. Почему бы и нет?
И вообще, может быть существуют целая иерархия недоказумостей: недоказумость, недоказумость недоказумости, недоказумость недоказумости недоказумости, ...
Приходил ли уже кто-нибудь к такой мысли?

-- 16.03.2013, 14:09 --

И еще. Зачем вообще нужны доказательства? Ну, например, чтобы убедить себя и других в чем-то. Хорошо, допустим вы что-то доказали, например, решили какую-нибудь проблему тысячелетия. И доказательство у вас получилось очень очень большим. Себя вы уже, допустим, убедили, что оно правильное. Чтобы убедить остальных, они должны проверить ваше доказательство. Т.е. естественным образом возникает необходимость доказать, что ваше доказательство правильное. Хорошо, допустим, что и это доказали. Но теперь возникает другая проблема: а вдруг доказательство того, что ваше доказательство правильное, само является неправильным? Т.е. теперь уже необходимо доказательство того, что доказательство того, что ваше ваше доказательство правильное, само является правильным. И т.д., в итоге приходим к выводу, что цель доказательств - абсолютно убедить - недостижима.

[nikvic]

nasldfhgon в сообщении #696523 писал(а):

цель доказательств - абсолютно убедить - недостижима

Пять слов, и каждое под кардинальным вопросом - что оно значит?
"Can machin think?" - и потом 3 вопроса. 1967(?) год.

[Xaositect]

nasldfhgon в сообщении #696523 писал(а):

Вот Кантор, например, долго мучился пытаясь доказать континуум-гипотезу. В итоге только нервы себе потрепал, так ничего и не доказав. Как выяснилось позже, ее вообще нельзя ни доказать, ни опровергнуть в ZFC, т.е. она недоказуема. Теперь же, перед математиками стоит другой вопрос: противоречива или нет ZFC? Многие пытаются доказать ее непротиворечивость уже много лет и так ничего не выходит. Это меня натолкнуло на мысль, что, возможно, непротиворечивость ZFC недоказума. Почему бы и нет?
И вообще, может быть существуют целая иерархия недоказумостей: недоказумость, недоказумость недоказумости, недоказумость недоказумости недоказумости, ...
Приходил ли уже кто-нибудь к такой мысли?

Да. Теорема Геделя о неполноте.

[nasldfhgon]

Xaositect
Эта мысль - следствие теоремы Геделя о неполноте?

[Xaositect]

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

[nasldfhgon]

Я так и не понял какое отношение имеет теорема Геделя о неполноте к тому о чем я говорил.

[Xaositect]

Из нее следует, что непротиворечивость ZFC недоказуема в ZFC.

[nasldfhgon]

А я не имел в виду в ZFC. Я имел в виду доказать (не)противоречивость ZFC подобно тому, как Генцен доказал непротиворечивость арифметики Пеано (он её доказал не в рамках арифметики Пеано).

[Xaositect]

nasldfhgon в сообщении #696741 писал(а):

А я не имел в виду в ZFC. Я имел в виду доказать (не)противоречивость ZFC подобно тому, как Генцен доказал непротиворечивость арифметики Пеано (он её доказал не в рамках арифметики Пеано).

Непротиворечивочть ZFC следует из существования больших кардиналов (напр. http://en.wikipedia.org/wiki/Inaccessible_cardinal ). Непротиворечивость ZFC можно доказать в теории классов Морзе-Келли ( http://en.wikipedia.org/wiki/Morse%E2%8 ... set_theory ) или теории множеств Тарского-Гротендика ( http://en.wikipedia.org/wiki/Tarski%E2% ... set_theory ).

[nasldfhgon]

Ясно.

[migmit]

Учитывая, что на любую теорию $T$ можно подобрать такую теорию $T'$, в которой докажется непротиворечивость $T$, это как-то не очень интересно. Собственно, можно подобрать одну такую $T'$ на все возможные $T$.

[epros]

nasldfhgon в сообщении #696523 писал(а):

Это меня натолкнуло на мысль, что, возможно, непротиворечивость ZFC недоказума. Почему бы и нет?
И вообще, может быть существуют целая иерархия недоказумостей: недоказумость, недоказумость недоказумости, недоказумость недоказумости недоказумости, ...

Существует целая иерархия доказуемостей непротиворечивости: Непротиворечивость арифметики первого порядка доказуема ZFC, непротиворечивость ZFC доказуема теорией с большими кардиналами, и т.д. Проблема только в том, что каждый следующий уровень иерархии достигается принятием новых аксиом. А аксиомы, как известно, это то, что принято без доказательств. Фактически, можно было бы получить новый уровень иерархии, просто приняв единственную аксиому: «предыдущая теория непротиворечива».

Кстати, «иерархия недоказуемостей» тоже с эти связана: Можно построить арифметическое утверждение, которое недоказуемо арифметикой первого порядка, но доказуемо ZFC, а потом можно построить арифметическое утверждение, которое недоказуемо даже ZFC, но доказуемо теорией с большими кардиналами и т.д.

nasldfhgon в сообщении #696523 писал(а):

Зачем вообще нужны доказательства?
…
И т.д., в итоге приходим к выводу, что цель доказательств - абсолютно убедить - недостижима.

Не совсем так. Цель доказательств — не «абсолютно убедить». Правильная цель доказательств: Дать возможность разным людям, но принимающим одинаковые предпосылки (аксиоматику), приходить к одинаковым выводам. Т.е. договариваться по множеству сложных вопросов, на основе принятия общей достаточно простой аксиоматики.

Если аксиоматики будут разными, то и выводы — тоже. Но, проанализировав свои выводы, мы сможем найти различия в аксиоматиках, т.е. обнаружим коренные причины разногласий. Это тоже неплохо.

[nasldfhgon]

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

Существует целая иерархия доказуемостей непротиворечивости: Непротиворечивость арифметики первого порядка доказуема ZFC, непротиворечивость ZFC доказуема теорией с большими кардиналами, и т.д.

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

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

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

А если агент (человек) во всем сомневается? Вот он доказал что-то, но думает "а вдруг ошибся, надо перепроверить". Перепроверил. Опять думает: "а вдруг я ошибся во время проверки, надо сделать проверку предыдущей проверки". И так до бесконечности.

[Someone]

nasldfhgon в сообщении #889406 писал(а):

А если агент (человек) во всем сомневается? Вот он доказал что-то, но думает "а вдруг ошибся, надо перепроверить". Перепроверил. Опять думает: "а вдруг я ошибся во время проверки, надо сделать проверку предыдущей проверки". И так до бесконечности.

К психиатру пускай обращается.

[arseniiv]

nasldfhgon в сообщении #889406 писал(а):

А если агент (человек) во всем сомневается? Вот он доказал что-то, но думает "а вдруг ошибся, надо перепроверить". Перепроверил. Опять думает: "а вдруг я ошибся во время проверки, надо сделать проверку предыдущей проверки". И так до бесконечности.

Формальный вывод — очень веская причина отбросить сомнения. Если они после построения и проверки правильности (лучше всего программой; имея доказательство корректности самой программы и парочку оценок надёжности компилятора, железа и проверяльщика программы, можно получить ооочень хорошую вероятность того, что всё будет хорошо) такого вывода останутся, то больше ничего не поможет. А вдруг я не сижу на стуле и не печатаю, а «на самом деле» мне это внушает невидимый розовый единорог?