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

[nikov]

Часто говорится, что противоречивые теории неинтересны, так как в них любое высказывание является теоремой. Фактически, наличие одного противоречия "отравляет" всю теорию. Известно также, что теория (в которой можно осуществить гёделевскую нумерацию), в которой доказуема ее собственная непротиворечивость, является противоречивой.
А может ли существовать непротиворечивая теория, в которой доказуема ее собственная противоречивость?
Например, если высказывание $Prf(0=1)$ является теоремой, то из него нельзя вывести $0=1$. То есть, доказать свою противоречивость она может, а доказать какое-то утверждение вместе с его отрицанием, вроде бы, не получается.

[маткиб]

nikov в сообщении #167873 писал(а):

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

Может.

[nikov]

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

nikov в сообщении #167873 писал(а):

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

Может.

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

[маткиб]

nikov в сообщении #167891 писал(а):

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

Этот вопрос изучали многие, и обсосали уже с самых различных сторон. Есть, например, российский математик Лев Дмитриевич Беклемишев, он занимается формальной арифметикой, читает спецкурсы на эту тему в Москве, и у него по материалам его спецкурсов есть электронные конспекты, там всё довольно понятно разжёвано. Правда, пишет он почему-то исключительно на английском. Вот здесь можно их скачать (поискать в списке по слову "Beklemishev"). Например, "Reflection principles and provability algebras in formal arithmetic". В статьях есть его e-mail, в крайнем случае можно ему написать, он посоветует, что почитать. Сам я не занимаюсь логикой, поэтому информацию черпаю, в основном, с подобных спецкурсов, гугла (а также яндекса) и собственных измышлений (ну и конечно же университетских курсов).

По поводу вашего конкретного вопроса, можно взять например теорию (ZFC+"ZFC противоречива"). Она будет непротиворечива (потому что в ZFC нельзя доказать непротиворечивость ZFC), но в ней можно доказать её противоречивость (потому что можно доказать противоречивость даже более слабой теории ZFC).

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

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

...можно взять например теорию (ZFC+"ZFC противоречива"). Она будет непротиворечива (потому что в ZFC нельзя доказать непротиворечивость ZFC), но в ней можно доказать её противоречивость (потому что можно доказать противоречивость даже более слабой теории ZFC).

Теория ZFC + "ZFC противоречива" будет непротиворечивой лишь в том случае, если непротиворечива сама ZFC Так это или нет --- неизвестно!

[epros]

Господа! А уточните пожалуйста, что Вы имеете в виду, говоря "теория противоречива" или "теория непротиворечива". Я знаю два способа определения непротиворечивости теории, но не знаю ничего про то, чтобы одно определение сводилось к другому:

1. Теория $T$ непротиворечива, если никакое опровержимое в ней высказывание нельзя в ней доказать (опровержимое недоказуемо):
$(T \vdash \neg S) \to \neg (T \vdash S)$

2. Теория $T$ непротиворечива, если в ней нельзя доказать никакое ложное высказывание (доказуемое истинно):
$(T \vdash S) \to S$

При доказательстве теорем Гёделя о неполноте (и первой, и второй) используется второе определение, но я не слышал, чтобы к тем же самым выводам можно было прийти, использовав первое определение. Т.е., как я понимаю, не факт, что непротиворечивое в первом смысле расширение арифметики обязано быть неполным (кстати, определение полноты теории тоже может иметь варианты).

[Someone]

Второе свойство называется иначе: корректность. Истинность высказывания не является, вообще говоря, внутренним свойством формальной теории, она (истинность) может зависеть от интерпретации. И корректность тоже, соответственно, не является внутренним свойством, а зависит от интерпретации. При доказательстве теоремы Гёделя используется непротиворечивость (и $\omega$-непротиворечивость).

[маткиб]

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

При доказательстве теорем Гёделя о неполноте (и первой, и второй) используется второе определение, но я не слышал, чтобы к тем же самым выводам можно было прийти, использовав первое определение.

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

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

Т.е., как я понимаю, не факт, что непротиворечивое в первом смысле расширение арифметики обязано быть неполным (кстати, определение полноты теории тоже может иметь варианты)

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

Добавлено спустя 6 минут 35 секунд:

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

[nikov]

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

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

Не совсем понимаю, как в определении может фигурировать понятие истинности, если оно является невыразимым по теореме Тарского.

[маткиб]

nikov в сообщении #168580 писал(а):

Не совсем понимаю, как в определении может фигурировать понятие истинности, если оно является невыразимым по теореме Тарского.

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

[epros]

Someone писал(а):

Второе свойство называется иначе: корректность. Истинность высказывания не является, вообще говоря, внутренним свойством формальной теории, она (истинность) может зависеть от интерпретации. И корректность тоже, соответственно, не является внутренним свойством, а зависит от интерпретации. При доказательстве теоремы Гёделя используется непротиворечивость (и $\omega$-непротиворечивость).

Касательно терминологии я с Вами согласен - мне тоже кажется неестественным называть второе свойство "непротиворечивостью", и именно по этой причине: потому что истинность не является внутренним свойством теории.

Однако выше я написал не то, что мне кажется, а то, что я почерпнул из литературы. Доказательство первой теоремы Гёделя о непротиворечивости строится таким образом, что при получении вывода об истинности $G$ используется именно второе свойство теории. Порядок рассуждений таков: Поскольку $G$ эквивалентно своей недоказуемости, то оно не может быть ложным, ибо это означало бы его доказуемость, т.е. доказуемость в теории ложного высказывания, что невозможно для непротиворечивой теории. Следовательно $G$ истинно.

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

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

А продемонстрируйте пожалуйста вывод $G$ из первого свойства теории $T$ + из равносильности $G$ его недоказуемости в теории $T$:
$G \leftrightarrow \neg (T \vdash G)$

[маткиб]

epros писал(а):

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

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

А продемонстрируйте пожалуйста вывод $G$ из первого свойства теории $T$ + из равносильности $G$ его недоказуемости в теории $T$:
$G \leftrightarrow \neg (T \vdash G)$

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

[nikov]

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

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

Опять прошу ссылки на какие-нибудь обзорные работы.
На русском или английском языке.

[epros]

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

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

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

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

[маткиб]

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

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

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

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

Добавлено спустя 14 минут 45 секунд:

nikov в сообщении #168747 писал(а):

Опять прошу ссылки на какие-нибудь обзорные работы.

На русском или английском языке.

Обзорные не знаю.
В книге Верещагина и Шеня "Вычислимые функции", например, приводится чисто теоретико-алгоритмическое доказательство теоремы Гёделя.