Completeness in hybrid type theory
Fil: Areces, Carlos Eduardo. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina.
| Main Authors: | , , , |
|---|---|
| Format: | submittedVersion |
| Language: | eng |
| Published: |
2021
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/11086/20021 https://doi.org/10.1007/s10992-012-9260-4 |
| _version_ | 1801215566258634752 |
|---|---|
| author | Areces, Carlos Eduardo Blackburn, Patrick Huertas, Antonia Manzano, María |
| author_facet | Areces, Carlos Eduardo Blackburn, Patrick Huertas, Antonia Manzano, María |
| author_sort | Areces, Carlos Eduardo |
| collection | Repositorio Digital Universitario |
| description | Fil: Areces, Carlos Eduardo. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. |
| format | submittedVersion |
| id | rdu-unc.20021 |
| institution | Universidad Nacional de Cordoba |
| language | eng |
| publishDate | 2021 |
| record_format | dspace |
| spelling | rdu-unc.200212022-10-13T11:07:10Z Completeness in hybrid type theory Areces, Carlos Eduardo Blackburn, Patrick Huertas, Antonia Manzano, María Hybrid logic Type theory Higher-order modal logic Nominals @ operators submittedVersion Fil: Areces, Carlos Eduardo. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. Fil: Blackburn, Patrick. University of Roskilde. Centre for Culture and Identity. Department of Philosophy and Science Studies; Dinamarca. Fil: Huertas, Antonia. Universitat Oberta de Catalunya; España. Fil: Manzano, María. Universidad de Salamanca; España. We show that basic hybridization (adding nominals and @ operators) makes it possible to give straightforward Henkin-style completeness proofs even when the modal logic being hybridized is higher-order. The key ideas are to add nominals as expressions of type t, and to extend to arbitrary types the way we interpret @i in propositional and first-order hybrid logic. This means: interpret @iαa, where αa is an expression of any type a, as an expression of type a that rigidly returns the value that αa receives at the i-world. The axiomatization and completeness proofs are generalizations of those found in propositional and first-order hybrid logic, and (as is usual in hybrid logic) we automatically obtain a wide range of completeness results for stronger logics and languages. Our approach is deliberately low-tech. We don’t, for example, make use of Montague’s intensional type s, or Fitting-style intensional models; we build, as simply as we can, hybrid logic over Henkin’s logic. submittedVersion Fil: Areces, Carlos Eduardo. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. Fil: Blackburn, Patrick. University of Roskilde. Centre for Culture and Identity. Department of Philosophy and Science Studies; Dinamarca. Fil: Huertas, Antonia. Universitat Oberta de Catalunya; España. Fil: Manzano, María. Universidad de Salamanca; España. Ciencias de la Computación 2021-08-31T14:22:20Z 2021-08-31T14:22:20Z 2014 article Areces, C. E., Blackburn, P., Huertas, A. y Manzano, M. (2014). Completeness in hybrid type theory. Journal of Philosophical Logic, 43 (2-3), 209-238. https://doi.org/10.1007/s10992-012-9260-4 http://hdl.handle.net/11086/20021 https://doi.org/10.1007/s10992-012-9260-4 eng Attribution-NonCommercial-NoDerivatives 4.0 International http://creativecommons.org/licenses/by-nc-nd/4.0/ Impreso; Electrónico y/o Digital EISSN 1573-0433 |
| spellingShingle | Hybrid logic Type theory Higher-order modal logic Nominals @ operators Areces, Carlos Eduardo Blackburn, Patrick Huertas, Antonia Manzano, María Completeness in hybrid type theory |
| title | Completeness in hybrid type theory |
| title_full | Completeness in hybrid type theory |
| title_fullStr | Completeness in hybrid type theory |
| title_full_unstemmed | Completeness in hybrid type theory |
| title_short | Completeness in hybrid type theory |
| title_sort | completeness in hybrid type theory |
| topic | Hybrid logic Type theory Higher-order modal logic Nominals @ operators |
| url | http://hdl.handle.net/11086/20021 https://doi.org/10.1007/s10992-012-9260-4 |
| work_keys_str_mv | AT arecescarloseduardo completenessinhybridtypetheory AT blackburnpatrick completenessinhybridtypetheory AT huertasantonia completenessinhybridtypetheory AT manzanomaria completenessinhybridtypetheory |