# Assuming that an arbitrary Infinite Time Turing Machine halts, is it possible to have a finite proof of the fact that it halts?

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?

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.)