First-order homotopical logic
Fuente:
arXiv
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Preprint |
| Publié: |
2019
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866912483123396608 |
|---|---|
| author | Helfer, Joseph |
| author_facet | Helfer, Joseph |
| contents | We introduce a homotopy-theoretic interpretation of intuitionistic first-order logic based on ideas from Homotopy Type Theory. We provide a categorical formulation of this interpretation using the framework of Grothendieck fibrations. We then use this formulation to prove the central property of this interpretation, namely homotopy invariance. To do this, we use the result from arXiv:1905.10690 that any Grothendieck fibration of the kind being considered can automatically be upgraded to a 2-dimensional fibration, after which the invariance property is reduced to an abstract theorem concerning pseudonatural transformations of morphisms into 2-dimensional fibrations. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_1908_08944 |
| institution | arXiv |
| publishDate | 2019 |
| record_format | arxiv |
| spellingShingle | First-order homotopical logic Helfer, Joseph Logic Algebraic Topology Category Theory 18C50 (Primary) 18D30, 55U35 (Secondary) We introduce a homotopy-theoretic interpretation of intuitionistic first-order logic based on ideas from Homotopy Type Theory. We provide a categorical formulation of this interpretation using the framework of Grothendieck fibrations. We then use this formulation to prove the central property of this interpretation, namely homotopy invariance. To do this, we use the result from arXiv:1905.10690 that any Grothendieck fibration of the kind being considered can automatically be upgraded to a 2-dimensional fibration, after which the invariance property is reduced to an abstract theorem concerning pseudonatural transformations of morphisms into 2-dimensional fibrations. |
| title | First-order homotopical logic |
| topic | Logic Algebraic Topology Category Theory 18C50 (Primary) 18D30, 55U35 (Secondary) |
| url | https://arxiv.org/abs/1908.08944 |