2024/12/17 by Juan P. Aguilera, Aguilera, Juan P., Anton Freund +3
Social Sciences · Engineering · Mathematics · #Historical Geography and Cartography #Advanced Numerical Analysis Techniques #Mathematics and Applications
paper · pdf · doi:10.48550/arxiv.2412.13051
One of the most important principles of J.-Y. Girard's Π12-logic is induction on dilators. In particular, Girard used this principle to construct his famous functor Λ. He claimed that the totality of Λ is equivalent to the set existence axiom of Π11-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 Π11-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 Π11-comprehension is equivalent to the totality of a functor \mathbb J due to P. Päppinghaus, which can be seen as a streamlined version of Λ.