Axiom Beta Implies Elementary Transfinite Recursion

TL;DR

This paper demonstrates that a weak set theory with Axiom Beta can prove elementary transfinite recursion and generate relativized constructible hierarchies, linking it to known systems and functions in set theory.

Contribution

It establishes that the theory C with Axiom Beta proves elementary transfinite recursion and corresponds to Simpson's ATR_0^set without countability, also analyzing its computational strength.

Findings

C proves the totality of the Veblen function.

C can generate relativized constructible hierarchies.

C is equivalent to PRSω plus Axiom Beta.

Abstract

We show that $\mathbf{C}$, a weak theory of sets with Axiom Beta, proves the scheme of Elementary, or $\Delta_0$ Transfinite Recursion and can generate, for every set, the corresponding relativized constructible hierarchy. We show that the theory $\mathbf{C}$ corresponds to Simpson's system $\mathbf{ATR}_0^\text{set}$ without the Axiom of Countability. In fact, $\mathbf{C}$ proves the totality of the Veblen function and of all primitive recursive set functions. In particular, this means our system $\mathbf{C}$ is equivalent to $\mathbf{PRS}\omega+\text{Axiom Beta}$. We also establish an upper bound, though not a sharp one, for the $\Sigma_1$-definable functions of $\mathbf{C}$. Finally, we show that the variant of $\mathbf{C}$ in which the Finite Powerset Axiom is replaced by the closure under the rudimentary functions is a strictly weaker theory and no longer ensures the existence of the relativized constructible hierarchy.