Completeness in hybrid type theory
View/ Open
Date
2014Author
Areces, Carlos Eduardo
Blackburn, Patrick
Huertas, Antonia
Manzano, María
Metadata
Show full item recordAbstract
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.
xmlui.dri2xhtml.METS-1.0.item-citation
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