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

[epros]

nasldfhgon, ну и запоздалая же у Вас реакция на комментарий.

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

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

Нет, совершенно не улавливаю. Во-первых, не содержать недоказуемое утверждение может только противоречивая теория. Возможно, Вы были неточны в формулировках и на самом деле хотели сказать «неразрешимое утверждение» (т. е. неопровержимое и недоказуемое). Но в этом смысле проблема тоже непонятна, ибо разрешимые теории от неразрешимых обычно чётко отличимы. Например, арифметика Пресбургера — разрешима, а примитивно-рекурсивная арифметика или и арифметика Робинсона — уже нет.

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

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

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

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

[nasldfhgon]

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

nasldfhgon, ну и запоздалая же у Вас реакция на комментарий.

Я уже не помню почему так вышло. Видимо на что-то отвлекся и забыл про эту тему и вообще этот форум. Недавно опять наткнулся и вспомнил.

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

Нет, совершенно не улавливаю.

Пусть T - теория. Предположим, что она непротиворечива. Теория полна если она не содержит недоказуемое утверждение такое, что его отрицание тоже недоказуемо. Мы хотим доказать полна T или нет с учетом предположения, что она непротиворечива. Долго мучаемся и ничего не выходит. Потом объявляется какой-нибудь смышленый парень и говорит: <<слушай, я только что доказал, что утверждение "теория T полна" недоказуемое равно как и утверждение "теория T не полна">>. Мы смотрим его доказательство и убеждаемся, что оно верно. Вот о такой ситуации я говорил.

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

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

Извиняюсь. Я хотел сказать недоказуемое утверждение вместе с его отрицанием. Т.е. и утверждение недоказуемо и его отрицание тоже недоказуемо.

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

Возможно, Вы были неточны в формулировках и на самом деле хотели сказать «неразрешимое утверждение» (т. е. неопровержимое и недоказуемое).

Да, если мы одинаково понимаем, что это значит. Я понимаю под этим недоказуемое вместе со своим отрицанием утверждение. А неразрешимая теория - это теория, которая содержит неразрешимое утверждение.

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

Но в этом смысле проблема тоже непонятна, ибо разрешимые теории от неразрешимых обычно чётко отличимы.

Чтобы выяснить разрешима теория или нет мы должны доказать одно из утверждений: "данная теория разрешима" либо "данная теория не разрешима". Разве не может, в принципе, возникнуть ситуации, что для какой-то теории мы докажем, что оба эти утверждения недоказуемы?

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

Например, арифметика Пресбургера — разрешима, а примитивно-рекурсивная арифметика или и арифметика Робинсона — уже нет.

Это понятно, да, для этих теорий мы это знаем. Но разве отсюда сразу следует, что мы можем для любой теории узнать разрешима она или нет? Может существует теория для которой это нельзя узнать в принципе?

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

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

Хорошо, допустим нам надоело вручную это делать и мы написали программу, которая способна "четко следовать правилам синтаксиса" и т.п. Но вдруг в ней ошибка? Для этого мы её хотим верифицировать. Что в этом психически ненормального?

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

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

Вот, это почти то, что я хотел сказал. Но допустим, что мы все же хотим чтобы эти некоторые математики признали эти доказательства. Для этого мы пишем программу-верификатор, которая доказывает правильность того самого данного компьютером доказательства, которое они не признают. Некоторые из этих математиков опять могут остаться недовольными: ведь теперь нужно проверить правильность программы-верификатора, что они считают не могут сделать не являясь программистами. Т.е. теперь нужно написать программу, которая проверят данную программу-верификатор. И т.д. до бесконечности.

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

[Someone]

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

Мы хотим доказать полна T или нет с учетом предположения, что она непротиворечива. Долго мучаемся и ничего не выходит. Потом объявляется какой-нибудь смышленый парень и говорит: <<слушай, я только что доказал, что утверждение "теория T полна" недоказуемое равно как и утверждение "теория T не полна">>. Мы смотрим его доказательство и убеждаемся, что оно верно.

Это его доказательство в какой теории?

[nasldfhgon]

Someone в сообщении #890312 писал(а):

Это его доказательство в какой теории?

В теории доказательств (proof theory).

[Someone]

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

В теории доказательств (proof theory).

А причём тут теория доказательств? Утверждение о доказуемости или недоказуемости некоторого утверждения теории $T$, равно как и утверждение о полноте или неполноте теории $T$, являются утверждениями метатеории теории $T$, и доказательство, стало быть, строится в метатеории. Поэтому утверждение о доказуемости или недоказуемости утверждения о полноте или неполноте теории $T$ принадлежит уже мета-метатеории теории $T$. Там же находится и утверждение о доказуемости или недоказуемости утверждения о доказуемости или недоказуемости некоторого утверждения теории $T$.

Но ситуация гораздо интереснее. Если выбранная нами метатеория теории $T$ настолько слаба, что не в состоянии доказать полноту или неполноту теории $T$ (либо доказуемость или недоказуемость некоторого утверждения теории $T$), то, вероятно, нужно взять более сильную метатеорию. Выбор более сильной метатеории, естественно, неоднозначен. Например, мы можем присоединить к метатеории в качестве аксиомы, что теория $T$ полна. Или, наоборот, присоединить в качестве аксиомы утверждение, что теория $T$ неполна. Так же мы можем поступить и в случае, когда речь идёт о доказуемости или недоказуемости некоторого утверждения теории $T$.

[nasldfhgon]

Someone в сообщении #890325 писал(а):

А причём тут теория доказательств?

Теория доказательств занимается формальными доказательствами. Утверждение теории называется недоказуемым если не существует формального доказательства этого утверждения в данной теории.

Someone в сообщении #890325 писал(а):

Если выбранная нами метатеория теории $T$ настолько слаба, что не в состоянии доказать полноту или неполноту теории $T$ (либо доказуемость или недоказуемость некоторого утверждения теории $T$), то, вероятно, нужно взять более сильную метатеорию.

Что нужно делать в такой ситуации - это уже отдельный вопрос. Я лишь пытался объяснить epros, что я имел в виду, когда говорил о иерархии недоказуемостей. Эта ситуация - это второй уровень этой иерархии: утверждение "теория Т неразрешима" неразрешимо. (Определение неразрешимости я давал выше). Третьий уровень - утверждение <<утверждение "теория Т неразрешима" неразрешимо>> неразрешимо. И т.д.

Упоминание этой иерархии в ОП было недоразумением. Я тогда просто еще не осознавал, что

migmit в сообщении #697486 писал(а):

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

Сейчас же я просто пытался объяснить epros что я имел в виду, потому что он процитировал тот кусок с упоминанием этой иерархии.

[Someone]

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

Теория доказательств занимается формальными доказательствами.

Формальными доказательствами вообще, но не доказательствами неполноты конкретных теорий.

[epros]

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

Теория полна если она не содержит недоказуемое утверждение такое, что его отрицание тоже недоказуемо. Мы хотим доказать полна T или нет с учетом предположения, что она непротиворечива.

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

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

Чтобы выяснить разрешима теория или нет мы должны доказать одно из утверждений: "данная теория разрешима" либо "данная теория не разрешима". Разве не может, в принципе, возникнуть ситуации, что для какой-то теории мы докажем, что оба эти утверждения недоказуемы?

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

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

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

Это бессмысленно, ибо чистые математики в программах всё равно копаться вряд ли станут: не та специальность. Тут два варианта: либо довериться программистам, либо остановиться на том, что к доказательству полного доверия нет.

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

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

Быть полностью уверенным можно только в том, на полную уверенность в чём ты запрограммирован.

[nasldfhgon]

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

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

Я всегда имел в виду только одно: в теории существует высказывание $B$ такое, что $B$ и $\lnot B$ недоказуемы.

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

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

Я не спорю. Просто я хотел объяснить, что я имел в виду, когда говорил о иерархии недоказуемостей в ОП, потому что Вы процитировали этот кусок в сообщении #698081 и не так его поняли. Вообще же, упоминание этой иерархии в ОП было недоразумением.

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

Это бессмысленно, ибо чистые математики в программах всё равно копаться вряд ли станут: не та специальность.

Если вспомнить о соответствии Карри-Ховарда (эквивалентности между математическими доказательствами и программами), то выходит, что математики и программисты занимаются по сути одним и тем же: формулируют и доказывают теоремы. Большинство так называемых программистов об этом даже не подозревают, но это уже другой вопрос.

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

Тут два варианта: либо довериться программистам, либо остановиться на том, что к доказательству полного доверия нет.

Ну вот мы пришли в итоге к тому, что все сводится к вере. Нельзя в принципе быть ни в чем полностью уверенным. Даже если есть доказательство.

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

Быть полностью уверенным можно только в том, на полную уверенность в чём ты запрограммирован.

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

[epros]

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

Я всегда имел в виду только одно: в теории существует высказывание $B$ такое, что $B$ и $\lnot B$ недоказуемы.

Тонкости различий заключаются в том, как трактовать «существование». Если утверждение о существовании или несуществовании такого $B$ доказано в некой метатеории, то оно — про полноту. Но может, например, случиться так, что утверждение о доказуемости некоего $B$ окажется неконструктивным: т. е. метатеория утверждает, что $B$ доказуемо в теории, но самого доказательства $B$ у нас не будет.

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

Если вспомнить о соответствии Карри-Ховарда (эквивалентности между математическими доказательствами и программами), то выходит, что математики и программисты занимаются по сути одним и тем же: формулируют и доказывают теоремы. Большинство так называемых программистов об этом даже не подозревают, но это уже другой вопрос.

Да, теоретически это так. Но на практике не только некоторые так называемые программисты не знают, что занимаются математикой, но и некоторые так называемые математики не знают, что занимаются программированием.

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

Ну вот мы пришли в итоге к тому, что все сводится к вере. Нельзя в принципе быть ни в чем полностью уверенным. Даже если есть доказательство.

Кто ж нам запретит? Если есть полное доверие к аксиоматике и к безошибочности процедуры доказательства, то можно быть полностью уверенным и в выводе.

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

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

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

В полной (или почти полной) уверенности самой по себе нет ничего плохого. Часто она позволяет не тратить время на изучение заведомо бесперспективных альтернатив.

[Skipper]

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

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

Возьмём какую нибудь гипотезу, которая описывается и легко понимается с помощью арифметики первого порядка.
Например, сильную гипотезу Гольдбаха, или -
гипотезу о том, что существует бесконечно много простых пар чисел-близнецов, с разностью в парах равной $2$,
(такие как, $11$ и $13$ ; $101$ и $103$, и т.д.).

Допустим, будет доказано, что эта гипотеза недоказуема - ни в арифметике первого порядка, ни в ZFC, ни в теорией с большими кардиналами, и т.д. Значит, как выше указано, нам останется только принять некую новую теорию, что будет эквивалентно принятию самой гипотезы - как $аксиому$: например - "существует бесконечное количество таких пар чисел-близнецов. ".

А другие математики примут, обратную аксиому, что лишь конечное количество таких пар чисел-близнецов существует.

Поскольку я не могу перебрать всё их бесконечное количество, то экспериментально не могу убедиться кто из них прав.
Кому тогда верить?

[Anton_Peplov]

Skipper в сообщении #1567330 писал(а):

Значит, как выше указано, нам останется только принять некую новую теорию, что будет эквивалентно принятию самой гипотезы - как $аксиому$: например - "существует бесконечное количество таких пар чисел-близнецов. ".

А другие математики примут, обратную аксиому, что лишь конечное количество таких пар чисел-близнецов существует.

Поскольку я не могу перебрать всё их бесконечное количество, то экспериментально не могу убедиться кто из них прав.
Кому тогда верить?

"В геометрии Евклида расстояние между параллельными прямыми одинаково в любой точке, а в геометрии Лобачевского оно может отличаться от точки к точке. Поскольку прямые не ограниченны, я не могу проследить всю протяженность параллельных прямых и экспериментально проверить, кто из них прав.
Кому тогда верить?".

[Skipper]

Anton_Peplov в сообщении #1567331 писал(а):

"В геометрии Евклида расстояние между параллельными прямыми одинаково в любой точке, а в геометрии Лобачевского оно может отличаться от точки к точке. Поскольку прямые не ограниченны, я не могу проследить всю протяженность параллельных прямых и экспериментально проверить, кто из них прав.
Кому тогда верить?".

Тут можно верить и Евклиду - если строим и представляем классическую геометрию, а можно и Лобачевскому - если строим неевклидову геометрию. Они обе имеют своё применение,

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

[Anton_Peplov]

Skipper в сообщении #1567332 писал(а):

А утверждение о том, бесконечное ли или конечное количество простых чисел-близнецов, кажется, должно иметь одну, абсолютную истину.

"Кажется" - ключевое слово.

[EminentVictorians]

Anton_Peplov,а не поделитесь Вашей точкой зрения? Я тоже, как и Skipper, считаю, что уж как минимум по отношению к утверждениям о натуральных числах абсолютная истина есть.