Kuroda's Translation for Higher-Order Logic
Fuente:
arXiv
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866912971359256576 |
|---|---|
| author | Traversié, Thomas |
| author_facet | Traversié, Thomas |
| contents | Kuroda's translation embeds first-order classical logic into intuitionistic logic, such that a formula and its translation are equivalent in classical logic. Recently, Brown and Rizkallah extended this translation to higher-order logic. However, they showed that the translation fails in the presence of functional extensionality, and they did not prove the classical equivalence between a formula and its translation. In this paper, we emphasize different conditions under which Kuroda's translation works in the presence of functional extensionality, including the double-negation shift. We show that the classical equivalence between a formula and its translation does not necessarily hold in higher-order logic. However, it is sufficient to assume both functional extensionality and propositional extensionality. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_19503 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Kuroda's Translation for Higher-Order Logic Traversié, Thomas Logic in Computer Science Kuroda's translation embeds first-order classical logic into intuitionistic logic, such that a formula and its translation are equivalent in classical logic. Recently, Brown and Rizkallah extended this translation to higher-order logic. However, they showed that the translation fails in the presence of functional extensionality, and they did not prove the classical equivalence between a formula and its translation. In this paper, we emphasize different conditions under which Kuroda's translation works in the presence of functional extensionality, including the double-negation shift. We show that the classical equivalence between a formula and its translation does not necessarily hold in higher-order logic. However, it is sufficient to assume both functional extensionality and propositional extensionality. |
| title | Kuroda's Translation for Higher-Order Logic |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2404.19503 |