@article {215,
	title = {Completeness in Hybrid Type Theory},
	journal = {Journal of Philosophical Logic},
	volume = {43},
	year = {2014},
	month = {June},
	pages = {209{\textendash}238},
	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{\textquoteright}t, for example, make use of Montague{\textquoteright}s intensional type s, or Fitting-style intensional models; we build, as simply as we can, hybrid logic over Henkin{\textquoteright}s logic.},
	author = {Carlos Areces and Blackburn, P. and Huertas, A., and Manzano, M.}
}