@ARTICLE{arec:comp13,
author = {Areces, C., and Blackburn, P. and Huertas, A., and Manzano, M.},
title = {Completeness in Hybrid Type Theory},
journal = {Journal of Philosophical Logic},
year = {2014},
volume = {43},
pages = {209--238},
number = {2--3},
month = {June},
abstract = {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 \alpha_a,
where \alpha_a is an expression of any type a, as an expression of
type a that rigidly returns the value that \alpha_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.},
owner = {areces},
timestamp = {2013.02.10}
}