Whenever you approach one of these problems, the first thing to do is what Rogers calls a Tarski-Kuratowski computation: find the level of the arithmetical hierarchy where the set in question lives. In this case, we have that $e \in \text{Tot}$ if for every $n$ there exists an $s$ with $\phi_{e,s}(n)\downarrow$ (that is, $\phi_e(n)$ halts in $s$ steps). Therefore Tot is $\Pi^0_2$ and its complement is $\Sigma^0_2$.
So how can we diagonalize against Tot to show it is not computably enumerable? Well, we can use the leading $\forall$ quantifier in its definition, and the fact that the halting set $K$ is already $\Sigma^0_1$, to show that if Tot was $\Sigma^0_1$ then the halting set would be computable. Recall that, in general, a set is computable if both it and its complement are $\Sigma^0_1$, which is equivalent to the set and its complement both being $\Pi^0_1$.
Let $e$ be given. We want to tell whether $e \in K$, that is, whether $\phi_e(0)$ halts. Let $g$ be such that $g(s) = 0$ if $\phi_{e,s}(0)\uparrow$ and $g(s)$ diverges if $\phi_{e,s}(0)\downarrow$. Notice that $g$ is a partial computable function, and $g$ is total if and only if $\phi_e(0)\uparrow$, and we can compute an index $\gamma_e$ for $g$ uniformly from an index $e$. Therefore, we have
$$
e \in K \leftrightarrow (\exists s)[\phi_{e,s}(0) \downarrow]\\
e \not \in K \leftrightarrow \gamma_e \in \text{Tot}
$$
So, if Tot was computably enumerable, the two facts there the would show that $K$ is computable, which is impossible. The method here was to leverage the $\forall$ quantifier in Tot; if we had a way to decide membership in Tot, that gives us a "free pass" to decide that universal quantifier. The definition of $\gamma_e$ leverages the universal quantifier to tell whether $\phi_e(0)$ does not halt.
How can we show that Tot is not $\Pi^0_1$? Well, we can use the inner $\exists$ quantifier in the definition of Tot, and the fact that the complement $\bar K$ of the halting problem is not computable. In the first part we used Tot to tell whether $\phi_e(0)\uparrow$. Now we will use Tot to tell whether $\phi_e(0)\downarrow$. Given $e$, let $h(x) = \mu s [\phi_{e,s}(0) \downarrow]$. Then $h$ is total if and only if $\phi_e(0)\downarrow$, which is equivalent to $e \not \in \bar K$. Also, we can compute an index $\eta(e)$ for $h$ uniformly from $e$. Thus:
$$
e \in \bar K \leftrightarrow (\forall s)[\phi_{e,s}(0)\uparrow]\\
e \not \in \bar K \leftrightarrow \eta(e) \in \text{Tot}
$$
Therefore, if $\text{Tot}$ was $\Pi^0_1$ then $\bar K$ would be computable, which is impossible.
You have proposed two good alternatives for resolving the question. Now you should ask:
- Is there any difference between these two?
- If there is a difference, do both solutions still validate the main theorems about infinite-time Turing machines (u-t-m and s-m-n theorems in particular)?
It's worthwhile thinking about these by yourself, as that will deepen the undersanding of Turing machines.
Regarding equivalence of the two solutions, as fas as I can see, we can transform a fall-of-the-tape machine to just-do-not-move-left-of-first-cell machine by placing a special marker at the begining of the tape (and moving the rest of the input slightly to the right, which may take $\omega$ steps for an infinite-time Turing machine). For the other direction, once again we can place a marker at the extreme left and go on a special state if we ever attempt to move left of that marker.
So all in all, there isn't a lot of difference and it doesn't matter what you do.
Best Answer
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.)