Тем не менее я ему благодарен, т.к. до конца понял существование константы Хайтина.
Будет ещё лучше, если кто-нибудь приведёт связь с теоремой Гёделя, если не сложно.
Ну, я сейчас наверно скажу то, что Вы уже знаете, а если не знаете, то догадываетесь :)
Есть такая область, как теория вычислимости, или теория рекурсии. Изучает она вычислимые и невычислимые функции, там есть иерархии и полурешетки, но мы не об этом.
Дело в том, что объекты этой теории можно представлять в различном виде. Самый явный - это, собственно, алгоритмы и вычисляемые ими функции, распознаваемые или перечисляемые множества. Диагональный метод дает здесь halting problem, перечислимое, но не рекурсивное множество всех самоприменимых программ и неперечислимое множество всех несамоприменимых программ.
А теперь можно вспомнить, что у нас всего функций континуум, как и действительных чисел. Каждое действительное число можно воспринимать как функцию
. Или как дедекиндово сечение (рассматриваются только общерекурсивные функции и разрешимые множества рациональных чисел). Соответственно, можно считать, что теория рекурсии имеет дело не с функциями, а с действительными числами - вычислимыми и невычислимыми. Тот же диагональный метод даст нам как раз константу Чейтина как невычислимое число. Она же является аналогом нерекурсивного перечислимого множества: нижняя часть ее сечения Дедекинда перечислима.
Теперь к теореме Геделя и логическим теориям. Рассмотрим ту же halting problem. Утверждение о том, что некоторая машина останавливается или не останавливается, можно рассматривать как утверждение некоторой формальной теории. Тогда теорема о halting problem становится аналогом теоремы Геделя: не существует эффективно аксиоматизируемой теории, в которой доказуемы все верные утверждения вида "машина
(не) останавливается на строке
". Теория - это, по сути, перечислимое множество, а теорема говорит о том, что множество
(стрелочки - это сходится-расходится, останавливается-зацикливается). Теорема Геделя утверждает то же самое относительно множества всех истинных утверждений арифметики, и один из возможных способов доказательства - как раз кодирование алгоритмов.
Другое дело, что множество истин арифметики неразрешимо "значительно сильнее", чем halting problem: если мы добавим оракул для решения HP, мы все равно не сможем получить всю арифметику. Для этого необходимо сделать счетную цепочку оракулов, отвечающих на вопросы об останове машин с оракулами ниже рангом.
У меня тоже есть один вопрос в тему, вдруг кто-нибудь знает. Что происходит с конструктивным анализом, если разрешить использовать оракул, говорящий, равны два числа или нет, или добавить аксиому
(и одно ли это и то же)? Понятно, что появляются разрывные функции и вроде бы теорема о промежуточном значении. Насколько все хорошо становится?