@Article{Areces2014,
  author =       "C. Areces and P. Blackburn and A. Huertas and M.
                 Manzano",
  journal =      "Journal of Philosophical Logic",
  title =        "Completeness in Hybrid Type Theory",
  year =         "2014",
  number =       "2--3",
  pages =        "209--238",
  volume =       "43",
  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",
}