A Note on Power-OTMs
Merlin Carl
TL;DR
This work introduces power-OTMs, OTMs augmented with a power-set operator, and develops a realizability framework based on them. By defining F-OTM-programs with F-encodings and coding-stable semantics, the authors show that power-OTMs can enumerate entire $V$-levels, making power-computability equivalent to power-recognizability and linking these notions to a $\Sigma_{2}$-definability perspective when ordinal parameters are used. A key focus is the realizability of axioms, especially the axiom of choice, which becomes independent of ZFC in this setting, being true under $V=L$ but not in all models (e.g., when $V\neq \text{HOD}$). The paper also introduces the halting problem for power-OTMs and discusses how the computational landscape differs from Set Register Machines, while outlining potential directions for further study on reducibility, clockable ordinals, and degree structures in the power-OTM realm.
Abstract
We consider the computational strength of Power-OTMs, i.e., ordinal Turing machines equipped with a power set operator, and study a notion of realizability based on these machines. When parameters are allowed, these machines are, modulo access to a global well-ordering, equivalent to the Set Register Machines defined by Robert Passmann in \cite{Passmann}, and while most of the results on the realizability of Power-OTMs are analogous to results obtained by Passmann, the settings lead to different results concerning the axiom of choice. As we will see, the computational strength of power-OTMs can, depending on the set-theoretical background, also differ from that of Set Register Machines.