Ищут ли сейчас контрпример для проблемы останова?

[fractalon]

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

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

Кажется, это проблема, которая сейчас находится в том же состоянии, в котором 2000 лет назад находилась проблема как можно более точного вычисления числа $\pi$.

[Sender]

Предлагаю упрощение. Поскольку любые начальные данные можно сгенерировать из пустой ленты некоторой машиной Тьюринга, можно ограничиться рассмотрением зацикливания МТ на пустой ленте. А в этом направлении исследования уже проводятся, см, например, Busy beaver.

[mihaild]

Два года назад построили конкретную машину Тьюринга с 7918 состояниями, которая не останавливается, но доказать это в ZFC нельзя.
Задача тесно связана с вычислением функции усердных бобров (время работы самой долгоиграющей машины Тьюринга с $n$ состояниями): если можно доказать верхнюю оценку на $BB(n)$, то для любой конкретной не останавливающейся МТ с $n$ состояниями можно доказать, что она не останавливается (т.к. если бы она останавливалсь, то она останавливалась бы не более чем за $BB(n)$ шагов, а что это не так можно доказать в любой интересной теории). Сейчас известно, что $BB(4) = 107$ (и соответственно проблема останова для МТ с не более чем $4$ состояниями решена), и что $BB(5) \geqslant 47176870$.

[fractalon]

mihaild, спасибо за подробное объяснение! Но я не понял одну деталь: если нельзя доказать в ZFC, откуда тогда мы знаем, что она не останавливается? В какой теории это доказано? Когда я писал своё сообщение, то подразумевал поиск машины, останавливающейся на невычислимом множестве начальных состояний - это было бы подвластно моему рассудку. Но если недоказуемо в ZFC, тогда о её зацикливаемости знают из верхной оценки на $BB(7918)$, что ли? (сомневаюсь, что оно оценено, но других версий у меня нет). Если не через $BB(7918)$, то как всё-таки с этим связано $BB$? Вы же привели оценки на $BB(5)$, а там 7918.

[mihaild]

Если бы вы прочитали пост по ссылке (сделайте это, Ааронсон пишет гораздо лучше, чем я), вы бы увидели:

Ааронсон писал(а):

1. Z runs forever, assuming the consistency of a large-cardinal theory called SRP (Stationary Ramsey Property), but
2. Z can’t be proved to run forever in ZFC (Zermelo-Fraenkel set theory with the Axiom of Choice, the usual foundation for mathematics), assuming that ZFC is consistent.

Из этого следует, что в ZFC недоказуемы никакие верхние оценки на $BB(7918)$ - если бы можно было доказать, что $BB(7918) < N$ для какого-то конкретного $N$, то можно было бы доказать, что МТ, ищущая противоречия в ZFC не останавливается, это означало бы, что ZFC непротиворечива - а непротиворечивость ZFC в самой ZFC не доказывается.

(аналогичной техникой наверняка можно построить МТ, ищущую противоречия в PA - тогда в PA нельзя будет доказать, что она не останавливается, а в ZF можно)

[fractalon]

Спасибо, я, кажется, разобрался! Дело в том, что машина пытается доказать противоречивость ZFC средствами ZFC, а это невозможно, потому что это не так. А доказать зацикленность машины невозможно, потому что это доказывало бы доказательство непротиворечивости ZFC средствами ZFC, а это невозможно вследствии соответствующей теоремы Гёделя.

Остаётся маленький уточняющий вопрос: как я понимаю, теорема Гёделя не привязана конкретно к ZFC. Верно ли поэтому, что тот же приём можно провернуть с любой формальной арифметикой, и опять получить недоказуемо зацикленную машину Тьюринга?

[mihaild]

С любой теорией, удовлетворяющей условиям теоремы Гёделя, да.

[george66]

Например, строится машина, которая перебирает все выводы в ZFC, пока не найдёт вывод противоречия. Если ZFC непротиворечива, то она никогда не найдёт и не остановится. А если вдруг противоречива, тогда найдёт и остановится! Какое из двух верно, мы не знаем.

[fractalon]

george66 в сообщении #1293773 писал(а):

А если вдруг противоречива, тогда найдёт и остановится! Какое из двух верно, мы не знаем.

Я сам не очень хорошо разбираюсь в формальных системах, но, как я понял, разбираясь с этим вопрос, непротиворечивость ZFC доказана, но в более сложной системе. Она не доказывается только средствами ZFC.

[epros]

fractalon в сообщении #1293915 писал(а):

но в более сложной системе

Которая в свою очередь может оказаться противоречивой.

[fractalon]

Хм... Действительно. А есть ли выход из этого замкнутого круга?

[mihaild]

По теоереме Гёделя - нет.

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

[Someone]

Собственно, утверждение о непротиворечивости формальной теории в ней самой нельзя не только доказать, но и сформулировать. Это утверждение относится к метатеории данной теории: оно там формулируется и доказывается, если метатеория достаточно сильная. То, что сделал Гёдель, это некоторый фокус: средствами мета-метатеории метатеория арифметики Пеано кодируется в этой арифметике, в результате чего утверждение о непротиворечивости арифметики превращается в некоторое утверждение о натуральных числах. И вот это утверждение о натуральных числах оказывается недоказуемым в арифметике.

[warlock66613]

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

Это утверждение относится к метатеории данной теории

А есть какое-то требование, чтобы метатеория была "сильнее"/"больше" теории? Иначе геворя - не может ли в принципе метатеория быть в точности той же теорией?

[Someone]

warlock66613 в сообщении #1294211 писал(а):

А есть какое-то требование, чтобы метатеория была "сильнее"/"больше" теории?

Нет. Метатеория должна быть в состоянии определить язык предметной теории, то есть, описать алфавит, синтаксис, аксиомы (включая логические), правила вывода. Арифметика Пеано для этого обычно достаточна, хотя и неудобна, поскольку всё нужно кодировать натуральными числами. Впрочем, у неё есть переформулировка, эквивалентная теории наследственно конечных множеств (фактически ZFC, в которой аксиома бесконечности заменена её отрицанием, и добавлены аксиомы индукции, которые без аксиомы бесконечности, кажется, не выводятся). Теория множеств типа ZFC или NBG гораздо удобнее и обладает чрезвычайно широкими возможностями для построения моделей. Чаще всего в роли метатеории выступает естественный язык, но в каких-то случаях может потребоваться формализованная метатеория.

warlock66613 в сообщении #1294211 писал(а):

Иначе говоря - не может ли в принципе метатеория быть в точности той же теорией?

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