Induction on Dilators and Bachmann-Howard Fixed Points

TL;DR

This paper establishes a deep connection between induction on dilators, the Bachmann-Howard principle, and $oldsymbol{ ext{Pi}}^1_1$-comprehension, clarifying longstanding technical and conceptual links in proof theory.

Contribution

It proves the equivalence between $oldsymbol{ ext{Pi}}^1_1$-comprehension and the totality of a functor related to Girard's $oldsymbol{ extLambda}$, unifying previous approaches.

Findings

Shows $oldsymbol{ extPi}^1_1$-comprehension is equivalent to the totality of P"appinghaus's functor

Relates induction on dilators to the Bachmann-Howard principle

Closes the gap in Girard's original proof from 1980

Abstract

One of the most important principles of J.-Y. Girard's $\Pi^1_2$-logic is induction on dilators. In particular, Girard used this principle to construct his famous functor $\Lambda$. He claimed that the totality of $\Lambda$ is equivalent to the set existence axiom of $\Pi^1_1$-comprehension from reverse mathematics. While Girard provided a plausible description of a proof around 1980, it seems that the very technical details have not been worked out to this day. A few years ago, a loosely related approach led to an equivalence between $\Pi^1_1$-comprehension and a certain Bachmann-Howard principle. The present paper closes the circle. We relate the Bachmann-Howard principle to induction on dilators. This allows us to show that $\Pi^1_1$-comprehension is equivalent to the totality of a functor $\mathbb J$ due to P. P\"appinghaus, which can be seen as a streamlined version of $\Lambda$.