Peano Arithmetic, games and descent recursion
Fuente:
arXiv
Gespeichert in:
| 1. Verfasser: | |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909409216561152 |
|---|---|
| author | Frittaion, Emanuele |
| author_facet | Frittaion, Emanuele |
| contents | We analyze Coquand's game-theoretic interpretation of Peano Arithmetic through the lens of elementary descent recursion. In Coquand's game semantics, winning strategies correspond to infinitary cut-free proofs and cut elimination corresponds to debates between these winning strategies. The proof of cut elimination, i.e., the proof that such debates eventually terminate, is by transfinite induction on certain interaction sequences of ordinals. In this paper, we provide a direct implementation of Coquand's proof, one that allows us to describe winning strategies by descent recursive functions. As a byproduct, we obtain yet another proof of well-known results about provably recursive functions and functionals. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_19884 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Peano Arithmetic, games and descent recursion Frittaion, Emanuele Logic We analyze Coquand's game-theoretic interpretation of Peano Arithmetic through the lens of elementary descent recursion. In Coquand's game semantics, winning strategies correspond to infinitary cut-free proofs and cut elimination corresponds to debates between these winning strategies. The proof of cut elimination, i.e., the proof that such debates eventually terminate, is by transfinite induction on certain interaction sequences of ordinals. In this paper, we provide a direct implementation of Coquand's proof, one that allows us to describe winning strategies by descent recursive functions. As a byproduct, we obtain yet another proof of well-known results about provably recursive functions and functionals. |
| title | Peano Arithmetic, games and descent recursion |
| topic | Logic |
| url | https://arxiv.org/abs/2411.19884 |