Машины Тьюринга, окончание которых недоказуемо?

У меня наивный вопрос: существует ли машина Тьюринга, завершение которой истинно, но недоказуемо какой-либо естественной, последовательной и конечно аксиоматизируемой теорией? Я прошу простое доказательство существования, а не конкретный пример.

Это может быть связано с порядковым анализом . Действительно, для машины Тьюринга $M$ мы можем определить $O(M)$ как наименьший порядковый номер последовательной теории, доказывающей ее окончание (или инфимум этих порядковых чисел). Так что я думаю, что было бы эквивалентно спросить, существует ли $M$ такой, что $O(M) \geq \omega_1^{CK}$ ?

turing-machines proof-theory halting-problem Super8
источник

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

Йонатан N

Ваше предложение интересно, спасибо. Я знал о вашей озабоченности при формулировании вопроса, поэтому я добавил «естественный» в требования. Конечно, проблема в том, можем ли мы дать формальное определение «естественности», которое исключило бы эту искусственную конструкцию.

Super8

думаю, что ответ отрицательный, потому что если он останавливается, то просто запускается машина, и она останавливается за конечное число шагов, и это доказательство, и этот факт можно преобразовать в любую достаточно мощную систему доказательств. с другой стороны, думаю, что можно закодировать / преобразовать / перевести недоказуемое tho Годеля в машину без остановки, для которой невозможно остановить без остановки. этот вопрос похож, есть ли ТМ, который останавливается на всех входах, но свойство не доказуемо cs.se

vzn

Вы можете построить машину Тьюринга

M

$M$ который вычисляет последовательность Гудштейна

G (n)

$G(n)$ ввода

n

$n$ и останавливается, когда достигает

0

$0$ Остановка

M

$M$ не может быть доказано в арифметике Пеано; то есть теорема Гудштейна не доказуема с помощью аксиом арифметики Пеано. См. Лори Кирби, Джефф Пэрис, Доступные результаты независимости для арифметики Пеано (1982)

Марцио Де Биаси

Спасибо, я не знал этих записей. Что я спрашиваю, тем сильнее, я бы хотел недоказуемость в отношении любой разумной теории (а не конкретной теории, такой как PA). Я не уверен, что вопрос имеет определенный ответ, хотя.

Super8

Ответы:

Завершение машины Тьюринга (на фиксированном входе) является $\Sigma^0_1$ предложение и все обычные арифметические теории первого порядка для $\Sigma^0_1$ предложения, т.е. все верно $\Sigma^0_1$ утверждения доказуемы в этих теориях.

Если вы посмотрите на тотальности вместо приостановки , т.е. ТМ останавливается на все входы, то это $\Pi^0_2$ -полное предложение и для любой вычислимо аксиоматизируемой непротиворечивой теории, которая достаточно сильна (например, расширяет, скажем, Робинсона $Q$ теория) есть ТМ, чья совокупность не может быть доказана в этой теории.

Кава
источник

Да, я искал совокупность, поскольку, конечно, проблема для фиксированного ввода тривиальна. Я подумаю о вашем утверждении и о том, как это доказать, но на данный момент я не понимаю, как рассмотрение «вычислимо аксиоматизируемых» теорий исключает вышеупомянутую проблему? Кроме того, в вашем утверждении ТМ зависит от рассматриваемой теории, можем ли мы получить мое более сильное утверждение с помощью некоторой диагонализации?

Super8

Вот простой способ: набор доказуемо полных вычислимых функций такой теории равен ce, набор полных вычислимых функций не равен ce, или же вы можете по диагонали сравнивать с доказуемо полными функциями теории.

Каве

После второй мысли я предлагаю рассмотреть ограничение проблемы следующим образом. Дана порядковая система обозначений

σ

$\sigma$ представляет порядковый номер

α

$\alpha$ мы можем определить соответствующую «элементарную теорию»

T (α, σ)

$\mathcal{T}(\alpha,\sigma)$ что позволяет трансфинитную индукцию до

α

$\alpha$ , Учитывая ТМ

M

$M$ мы бы тогда определили

O (M)

$O(M)$ как наименьший порядковый номер

α

$\alpha$ такое, что прекращение

M

$M$ может быть доказано теорией

T (α, σ)

$\mathcal{T}(\alpha,\sigma)$ (то есть система обозначений может быть свободно выбрана). Имеет ли это определение смысл?

Super8

@ Super8, я не уверен. Как правило, ассоциация ординалов с теориями не является канонической, для этого существуют различные способы ассоциирования. Вы можете начать со слабой теории, такой как PRA, и добавить индукцию к вычислимым ординалам с хорошими фундаментальными последовательностями и т. Д., Но я не уверен, почему вы хотели бы сделать это.

Каве

Хорошо, я не понял проблему, я постараюсь найти лучшее определение самостоятельно тогда.

Super8

Я не эксперт по логике, но я верю, что ответ - нет . Если машина Тьюринга останавливается и система достаточно сильна, вы должны иметь возможность выписать полную историю вычислений машины Тьюринга на ее входе. Когда кто-то проверяет, что результатом вычисления является завершающая последовательность переходов, можно увидеть, что машина останавливается. Независимо от того, как вы формализуете машины Тьюринга в своей теории, в любой разумной теории вы должны показать, что машина, которая останавливается, действительно останавливается. В качестве аналогии подумайте о попытке доказать, что конечная сумма равна тому, чему она равна; например, докажите, что 5 + 2 + 3 + 19 + 7 + 6 = 42 или 5 + 5 + 5 = 15. Так же, как это всегда возможно до тех пор, пока число шагов является конечным, также доказывается результат конечного вычисления.

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

Филип Уайт
источник

Я согласен с вашим первым пунктом, см. Мой ответ ниже. Что касается вашего второго пункта, противоречивая теория также докажет прекращение (фактически не определяющего) ТМ, откуда ограничение на согласованные теории.

Super8

Я думаю, что мы говорим то же самое; Я только заметил, что вы сказали «последовательный» в вопросе, извините за то, что пропустили это. Я думаю, что ответ Каве охватывает все те же вещи и в любом случае написан более элегантно.

Филип Уайт