Tarskian Theories of Krivine's Classical Realisability
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866910904428265472 |
|---|---|
| author | Hayashi, Daichi Leigh, Graham E. |
| author_facet | Hayashi, Daichi Leigh, Graham E. |
| contents | This paper presents a formal theory of Krivine's classical realisability interpretation for first-order Peano arithmetic ($\mathsf{PA}$). To formulate the theory as an extension of $\mathsf{PA}$, we first modify Krivine's original definition to the form of number realisability, similar to Kleene's intuitionistic realisability for Heyting arithmetic. By axiomatising our realisability with additional predicate symbols, we obtain a first-order theory $\mathsf{CR}$ which can formally realise every theorem of $\mathsf{PA}$. Although $\mathsf{CR}$ itself is conservative over $\mathsf{PA}$, adding a type of reflection principle that roughly states that ``realisability implies truth'' results in $\mathsf{CR}$ being essentially equivalent to the Tarskian theory $\mathsf{CT}$ of typed compositional truth, which is known to be proof-theoretically stronger than $\mathsf{PA}$. Thus, $\mathsf{CT}$ can be considered a formal theory of classical realisability. We also prove that a weaker reflection principle which preserves the distinction between realisability and truth is sufficient for $\mathsf{CR}$ to achieve the same strength as $\mathsf{CT}$. Furthermore, we formulate transfinite iterations of $\mathsf{CR}$ and its variants, and then we determine their proof-theoretic strength. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_04094 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Tarskian Theories of Krivine's Classical Realisability Hayashi, Daichi Leigh, Graham E. Logic This paper presents a formal theory of Krivine's classical realisability interpretation for first-order Peano arithmetic ($\mathsf{PA}$). To formulate the theory as an extension of $\mathsf{PA}$, we first modify Krivine's original definition to the form of number realisability, similar to Kleene's intuitionistic realisability for Heyting arithmetic. By axiomatising our realisability with additional predicate symbols, we obtain a first-order theory $\mathsf{CR}$ which can formally realise every theorem of $\mathsf{PA}$. Although $\mathsf{CR}$ itself is conservative over $\mathsf{PA}$, adding a type of reflection principle that roughly states that ``realisability implies truth'' results in $\mathsf{CR}$ being essentially equivalent to the Tarskian theory $\mathsf{CT}$ of typed compositional truth, which is known to be proof-theoretically stronger than $\mathsf{PA}$. Thus, $\mathsf{CT}$ can be considered a formal theory of classical realisability. We also prove that a weaker reflection principle which preserves the distinction between realisability and truth is sufficient for $\mathsf{CR}$ to achieve the same strength as $\mathsf{CT}$. Furthermore, we formulate transfinite iterations of $\mathsf{CR}$ and its variants, and then we determine their proof-theoretic strength. |
| title | Tarskian Theories of Krivine's Classical Realisability |
| topic | Logic |
| url | https://arxiv.org/abs/2504.04094 |