Induction on Dilators and Bachmann-Howard Fixed Points
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929635405594624 |
|---|---|
| author | Aguilera, Juan P. Freund, Anton Weiermann, Andreas |
| author_facet | Aguilera, Juan P. Freund, Anton Weiermann, Andreas |
| contents | One of the most important principles of J.-Y. Girard's $Π^1_2$-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 $Π^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 $Π^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 $Π^1_1$-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 $Λ$. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2412_13051 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Induction on Dilators and Bachmann-Howard Fixed Points Aguilera, Juan P. Freund, Anton Weiermann, Andreas Logic 03B30, 03D60, 03F15, 03F35 One of the most important principles of J.-Y. Girard's $Π^1_2$-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 $Π^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 $Π^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 $Π^1_1$-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 $Λ$. |
| title | Induction on Dilators and Bachmann-Howard Fixed Points |
| topic | Logic 03B30, 03D60, 03F15, 03F35 |
| url | https://arxiv.org/abs/2412.13051 |