Herbrandized modified realizability
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866911784106983424 |
|---|---|
| author | Ferreira, Gilda Firmino, Paulo |
| author_facet | Ferreira, Gilda Firmino, Paulo |
| contents | Realizability notions in mathematical logic have a long history, which can be traced back to the work of Stephen Kleene in the 1940s, aimed at exploring the foundations of intuitionistic logic. Kleene's initial realizability laid the ground for more sophisticated notions such as Kreisel's modified realizability and various modern approaches. In this context, our work aligns with the lineage of realizability strategies that emphasize the accumulation, rather than the propagation of precise witnesses. In this paper, we introduce a new notion of realizability, namely herbrandized modified realizability. This novel form of (cumulative) realizability, presented within the framework of semi-intuitionistic logic is based on a recently developed star combinatory calculus, which enables the gathering of witnesses into nonempty finite sets. We also show that the previous analysis can be extended from logic to (Heyting) arithmetic. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_16437 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Herbrandized modified realizability Ferreira, Gilda Firmino, Paulo Logic 03F10, 03B20, 03B40, 03F30, 03F25 Realizability notions in mathematical logic have a long history, which can be traced back to the work of Stephen Kleene in the 1940s, aimed at exploring the foundations of intuitionistic logic. Kleene's initial realizability laid the ground for more sophisticated notions such as Kreisel's modified realizability and various modern approaches. In this context, our work aligns with the lineage of realizability strategies that emphasize the accumulation, rather than the propagation of precise witnesses. In this paper, we introduce a new notion of realizability, namely herbrandized modified realizability. This novel form of (cumulative) realizability, presented within the framework of semi-intuitionistic logic is based on a recently developed star combinatory calculus, which enables the gathering of witnesses into nonempty finite sets. We also show that the previous analysis can be extended from logic to (Heyting) arithmetic. |
| title | Herbrandized modified realizability |
| topic | Logic 03F10, 03B20, 03B40, 03F30, 03F25 |
| url | https://arxiv.org/abs/2402.16437 |