Ordinal complexity of recursive definitions (Q1193596)

We classify and compare recursive and iterative definitions of total computable functions according to the complexity of the ordinal structures needed to verify termination. The main results are as follows: Let \(A\) be a set of structured tree-ordinals. \(\text{T-WHILE}(A)\) is a set of functions (denoted by programs) built from sequencing, conditionals and terminating while-loops which use tree parameters \(\alpha\in A\). \(\text{HARDY}(A)\) is, by Theorem I, an equivalent formulation, based on a Kleene-style presentation which includes primitive recursion and adds in the set \(H(A)\) of Hardy functionals \(\{H_ \alpha: \alpha\in A\}\). \(\text{REC}(A)\) is a set of functions defined by composition, conditionals and nested recursions which use parameters from \(A\). Theorem II establishes that, provided \(A\) satisfies suitable conditions such as Turing-machine representability and closure under addition and multiplication, \[ \text{T- WHILE}(A)\equiv\text{ELEM}(H(A))\equiv\text{SPACE}(H(A)). \] Theorem III tells us that under somewhat weaker conditions on \(A\), \(\text{REC}(\omega\cdot A)\equiv\text{T-WHILE}(\omega^ A)\), and is a generalization of a theorem of Tait showing nested recursions over a given well-ordering can be compiled to unnested ones but at the cost of an exponential increase in the size of the well-ordering. Some applications of these theorems are given at the end of the paper, for example: \[ \begin{aligned}\text{REC}(\omega\cdot N) & \equiv \text{WHILE}(\omega^ N)\\& \equiv\text{PRIMITIVE RECURSIVE}\\ \text{REC}(E) & \equiv \text{WHILE}(E)\equiv\text{SPACE}(E)\\ &\equiv \text{PROVABLY RECURSIVE in PA},\end{aligned} \] where \(N\) is the set of finite tree-ordinals and \(E\) is the closure of \(N\) under exponentiation. The first author has subsequently shown that under the weaker conditions, \(\text{PROV}(\lvdash^{\omega\cdot A}_{\Sigma^ 0_ 1 C})\equiv\text{REC}(\omega\cdot A)\), where \(\text{PROV}(\lvdash^ A_{\Sigma^ 0_ 1 C})\) is the set of functions which have a totality proof in \(\omega\)-logic with \(\Sigma^ 0_ 1\) cut-rank and ordinal bound in \(A\).