Доказать разрешимость множества неконструктивно

[epros]

Сейчас случайно обратил внимание на утверждение у Верещагина и Шеня в Лекциях по математической логике и теории алгоритмов.Часть 3. Вычислимые функции. Раздел 1.2. Разрешимые множества:

Цитата:

Отметим тонкий момент: можно доказать разрешимость множества неконструктивно, не предъявляя алгоритма.

При этом определение разрешимости множества такое:

Цитата:

Множество натуральных чисел $X$ называется разрешимым, если существует алгоритм, который по любому натуральному $n$ определяет, принадлежит ли оно множеству $X$.

Что ж, понятно, можно доказать существование алгоритма неконструктивно, то бишь не предъявляя его.

Но вот пример меня озадачил:

Цитата:

Вот традиционный пример: множество тех $n$, для которых в числе $\pi$ есть не менее $n$ девяток подряд, разрешимо. В самом деле, это множество содержит либо все натуральные числа, либо все натуральные числа вплоть до некоторого. В обоих случаях оно разрешимо. Тем не менее мы так и не предъявили алгоритма, который по $n$ узнавал бы, есть ли в $\pi$ не менее $n$ девяток подряд.

Где же здесь доказательство существования алгоритма, определяющего принадлежность любого $n$ этому множеству? Я вижу только способ подтвердить, что $n$ принадлежит этому множеству, но способа подтвердить, что $n$ не принадлежит этому множеству, я не вижу. Вероятно, я туплю.

[kotenok gav]

Если для натуральных: если число натуральное, вывести ДА. Иначе вывести НЕТ.
Если для натуральных меньше k: если число натуральное и меньше k, вывести ДА. Иначе вывести НЕТ.

[epros]

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

[george66]

Воспринимайте так: если Перельман докажет, что в числе пи бывает 98 девяток подряд, но не больше, мы узнаем алгоритм. То есть, он есть, его не может не быть, но мы его пока не знаем.

[arseniiv]

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

Но как-то душа оного не приемлет. Чувствую, что конструктивист с классиком никогда друг друга до конца не поймут ввиду неких глубинных мировоззренческих расхождений...

Классик как минимум может смоделировать у себя конструктивную вселенную, так что что ему не понимать?

Вашу проблему я понимаю в таком ключе: хочется считать, что промежуток натурального ряда, содержащий его начало (разрешимость которого очевидна) и то множество, связанное с $\pi$ — несовпадающие. Кажется, этому можно придать какой-то смысл: может быть, в некоторой подходящей теории как раз нельзя доказать их равенство. В классике они совпадают — ну так «в теории нет разницы между теорией и практикой, а на практике есть».

[g______d]

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

Где же здесь доказательство существования алгоритма, определяющего принадлежность любого $n$ этому множеству? Я вижу только способ подтвердить, что $n$ принадлежит этому множеству, но способа подтвердить, что $n$ не принадлежит этому множеству, я не вижу. Вероятно, я туплю.

Применяем алгоритм, выдающий последовательность знаков числа $\pi$, и останавливаемся, если он выдал $n$ девяток подряд. Тот факт, что ответа "нет" он выдать не может и вместо этого будет продолжаться вечно, -- не проблема, это соответствует определению вычислимой функции из предыдущего раздела.

-- Пн, 27 авг 2018 14:38:46 --

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

При этом определение разрешимости множества такое:

Там есть ещё следующий абзац.

[epros]

g______d в сообщении #1334958 писал(а):

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

Определению разрешимого множества он, однако, не соответствует. Такой алгоритм соответствует определению перечислимого множества (даётся в следующем разделе).

g______d в сообщении #1334958 писал(а):

Там есть ещё следующий абзац.

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

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

Другой пример, о котором я сейчас вспомнил, это определение невычислимой функции $\Sigma:\mathbb{N} \to \mathbb{N}$ "busy beaver". Там классический анализ тоже заявляет, что хотя общего алгоритма для вычисления $\Sigma(n)$ не существует, однако "существует алгоритм вычисления для каждого отдельного $n$". Поскольку никто ещё не знает, чему равно $\Sigma(9)$, закономерно возникает вопрос: Каков же этот алгоритм для вычисления $\Sigma(9)$? Вы будете смеяться, но ответ классической логики таков: Это алгоритм $\text{PRINT}~\Sigma(9)$ - подставьте вместо $\Sigma(9)$ соответствующее число, каким бы оно ни оказалось. Мой разум не в состоянии этого постичь, ибо раз мы не в состоянии вычислить $\Sigma(9)$, то по моим понятиям никакого $\Sigma(9)$ не существует.

[g______d]

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

Хотя прямо здесь этого не сказано, но очевидно, что характеристическая функция подразумевается всюду определённой.

Да, похоже, что Вы правы, в следующем параграфе это уточняется. Спасибо.

[g______d]

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

Мой разум не в состоянии этого постичь, ибо раз мы не в состоянии вычислить $\Sigma(9)$, то по моим понятиям никакого $\Sigma(9)$ не существует.

Кстати, а тогда такой вопрос: если кто-нибудь докажет конструктивную верхнюю оценку для $\Sigma(9)$, будет проще? В смысле если есть конечное число алгоритмов, среди которых один правильный, но неизвестно, какой именно.

[mihaild]

g______d в сообщении #1335461 писал(а):

Кстати, а тогда такой вопрос: если кто-нибудь докажет конструктивную верхнюю оценку для $\Sigma(9)$, будет проще?

Для достаточно больших значений $9$ не докажут никогда - например, в ZF нельзя доказать никакую оценку сверху на $\Sigma(9000)$.