When writing with a friend of mine today we came up with idea of extending ITTM concept of Hamkins and Kidder. First of all, I am familiar with one of Hamkins and Lewis results saying that every machine either halts or repeats before $\omega_1$, so allowing standard ITTMs to run beyond $\omega_1$ will give us nothing (because machine either already halted or won't halt ever).
The idea we had is the following: standard ITTM introduces specialized limit state the machine enters at every limit stage, that is, at every stage which is a multiple of $\omega$. To extend this, we add a second limit stage, such that machine enters it at stages which are multiples of $\omega_1$.
How strong is this extended system? The answer is: very strong. To show that I'll show how to decide $0^\blacktriangledown$, the set of all pairs $\langle e,r\rangle\in\mathbb{N}\times\mathbb{R}$ such that $e$th ITTM halts on input $r$: we just simulate this machine on that input! If the machine halts on this input, we will eventually notice this, and we can accept. Moreover, if the machine halts, it halts before $\omega_1$. So if we reach stage $\omega_1$ we know machine won't halt. But with our new limit stage we know when we reach $\omega_1$. Thus $0^\blacktriangledown$ is decidable.
From this fact, by a result of P.D.Welch, $\Sigma$ and ordinals well beyond it are writable. We can also iterate the above argument, so we prove decidability of $0^{\blacktriangledown^n}$.
Even better, we can iterate $\blacktriangledown$ operator transfinitely, up to ordinals of size of $\Sigma$. The argument to show this is actually quite similar to Hamkins-Lewis argument to show that tranfinitely iterated Turing jump is ITTM-computable.
When figuring this all out, I kept thinking about one thing - the relation between this model and ITTMs is very similar to relation between ITTMs and standard Turing machines. I also was thinking "there is no way this hasn't been considered before!".
The actual question of mine: has this system been considered by anyone before? The extension seems so simple I'd be surprised if no one did. It also is a very strong system, so my second question is: if this has already been considered, how strong is this system, actually? I suspect its complexity to be properly contained in $\Delta^1_2$, like with normal ITTMs.
(a little off-topic question, but I don't want to make separate MO question: I read somewhere that Koepke's ordinal machines with no ordinal parameters compute exactly $\Delta^1_2$ sets. Does anyone know good reference for this?)
