Машина тьюринга останавливается в некоторых интерпретациях?

[lyakusha_qwerty]

Кажется я где-то запутался.

1. Для машины Тьюринга M можно логикой первого порядка и ZF записать предложение, что M при подаче n на вход не останавливается, например что-то вроде <тут аксиомы ZF>→<тут сформулированное в ZF предложение, что M при подаче n не останавливается>
2. Если это предложение верно во всех интерпретациях ZF, то существует его доказательство (по теореме Гёделя о полноте).
3. Если для каждой неостанавливающейся пары (M, n) существует доказатальство предложения вида как в шаге 1, то функция останова вычислима - параллельно делаем: 1 шаг машины тьюринга, один шаг дедуктивного вывода поиском вширь, когда-нибудь или остановится, или мы дойдем доказательство предложения.
4. Значит существует M и n такие, что M не останавливается при n на входе, но в некоторой интерпретации ZF оно останавливается.

Как так?

[george66]

Теория множеств учит, что существуют нестандартные интерпретации, в которых натуральный ряд содержит нестандартные бесконечно большие числа. Где-то там и остановится машина. Ещё вариант: добавим к арифметике аксиому "есть вывод противоречия в арифметике". Эта теория непротиворечива (по второй теореме Гёделя). По теореме о полноте у неё есть модель. Это нестандартный натуральный ряд, в котором есть бесконечно длинный (недостижимый для нас) вывод противоречия.

[lyakusha_qwerty]

Тогда почему бы не дополнить ZF(C) дополнительными аксиомами, чтобы не было интерпретаций, в которых правдива всякая чушь?

Upd: ах, кажется теорема Геделя о неполноте говорит, что так не получится

[Утундрий]

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

Где-то там и остановится машина

Правда ждать этого, сами понимаете, бесконечно долго.