Computable Aspects of the Bachmann-Howard Principle

TL;DR

This paper explores the computability and foundational aspects of the Bachmann-Howard principle, showing its equivalence to $oldsymbol{ ext{Pi}}^1_1$-comprehension within a weaker base theory and providing a computable notation system for fixed points.

Contribution

It demonstrates that the Bachmann-Howard fixed point principle can be expressed in a computable form and relates it to $oldsymbol{ ext{Pi}}^1_1$-comprehension over a minimal base theory.

Findings

The base theory can be lowered to $ ext{RCA}_0$.

A computable notation system $ heta(T)$ for fixed points is constructed.

The well-foundedness of $ heta(T)$ characterizes $oldsymbol{ ext{Pi}}^1_1$-comprehension.

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{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 $\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.