Completeness in Hybrid Type Theory

C. Areces, P. Blackburn, A. Huertas, and M. Manzano. Completeness in Hybrid Type Theory. Journal of Philosophical Logic, 43(2--3):209–238, 2014.

Download

[pdf] 

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.

BibTeX

@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",
}