Paper detail

Computable Aspects of the Bachmann-Howard Principle

We have previously established that $Π^1_1$-comprehension is equivalent to the statement that every dilator has a well-founded Bachmann-Howard fixed point, over $\mathbf{ATR_0}$. In the present paper we show that the base theory can be lowered to $\mathbf{RCA_0}$. We also show that the minimal Bachmann-Howard fixed point of a dilator $T$ can be represented by a notation system $\vartheta(T)$, which is computable relative to $T$. The statement that $\vartheta(T)$ is well-founded for any dilator $T$ will still be equivalent to $Π^1_1$-comprehension. Thus the latter is split into the computable transformation $T\mapsto\vartheta(T)$ and a statement about the preservation of well-foundedness, over a system of computable mathematics.