Completeness in Hybrid Type Theory

Carlos Areces, Patrick Rowan Blackburn, Antonia Huertas, Maria Manzano

Research output: Contribution to journalJournal articleResearchpeer-review


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 inhybrid 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 logicover Henkin’s logic
Original languageEnglish
JournalJournal of Philosophical Logic
Issue number2-3
Pages (from-to)209-238
Number of pages30
Publication statusPublished - 2014


  • Type theory
  • @-operator
  • Nominals
  • Hybrid logic
  • Higher-order modal logic

Cite this