Computable Aspects of the Bachmann-Howard Principle

Abstract

We have previously established that ${\Pi }_1^1$-comprehension is equivalent to the statement that every dilator has a well-founded Bachmann-Howard fixed point, over $\mathbf{AT}{\mathbf{R}}_0$. In the present paper we show that the base theory can be lowered to $\mathbf{RC}{\mathbf{A}}_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 ${\Pi }_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.

This is the submitted version (before peer review) of a paper published in the Journal of Mathematical Logic. Note, in particular, that the numbering of theorems differs from the published version

Cited by in corpus (6)

• Derivatives of normal functions in reverse mathematics
• A Categorical Construction of Bachmann-Howard Fixed Points
• A note on ordinal exponentiation and derivatives of normal functions
• How strong are single fixed points of normal functions?
• Ackermann and Goodstein go functorial
• Reverse mathematics of a uniform Kruskal-Friedman theorem