2
$\begingroup$

If we consider ordinary Turing machines, we can assume that if an $i$-th machine halts, there exists a finite proof of this: just write the corresponding computation history.

But if we consider Infinite Time Turing Machines and pick an arbitrary natural number $i$, then, if an $i$-th machine halts and clocks any ordinal which is not less than $\omega$, there is no direct way to have a finite string that encodes the corresponding computation history step by step (because the computation is infinite). Does this imply that it is not possible to have a finite proof of halting for the $i$-th ITTM?

If the answer to the previous question is “No, it is possible”, then how can this be done? And what can be an example of a formal language that allows to write such proofs?

$\endgroup$
2
$\begingroup$

No, in general it is impossible to "prove in a finite way" that a halting ITTM computation actually is a halting ITTM computation.

One way to make this precise is to talk about the complexity of the corresponding index set - namely, the set of $e$ such that the $e$th ITTM halts on input $e$ (say). "Finite verifiability" corresponds to a computably enumerable (in the usual sense) index set (just search through all possible "verifications"); but it's easy to show that this set is not c.e.

And this indicates what's going wrong: a type mismatch. "Finite verifiability" is really connected with classical computability and the classical notion of c.e. For ITTMs, we want to generalize this appropriately. And this winds up pointing in the very fruitful direction of the use of (fragments of) logics beyond first-order logic - especially the infinitary logic $\mathcal{L}_{\omega_1,\omega}$ and its fragments - in higher recursion theory.

(Another way to say that we can't "finitely verify" ITTM computations is to observe that there are two $\omega$-models of ZFC which disagree over the haltingness of a given ITTM computation.)

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.