Comment by red75prime

> The "non-standard number of steps" is as nonsense as it sounds.

That is we can add a nonsensical axiom and get a consistent nonsensical theory that has nothing to do with actually running Turing machines (no matter in which physical or abstract universe they run). Er, OK, fine I guess.

A universally inapplicable theory.

No. I can't wrap my head around it. Successors for the tape state are defined for the initial segment of a non-standard natural numbers. How the proof of termination would even look like? Something non-constructive that doesn't allow to choose the machine among a finite number of the machines?