Abstract
Leon Henkin was not a modal logician, but there is a branch of modal logic that has been deeply influenced by his work. That branch is hybrid logic, a family of logics that extend orthodox modal logic with special propositional symbols (called nominals) that name worlds. This paper explains why Henkin’s techniques are so important in hybrid logic. We do so by proving a completeness result for a hybrid type theory called HTT, probably the strongest hybrid logic that has yet been explored. Our completeness result builds on earlier work with a system called BHTT, or basic hybrid type theory, and draws heavily on Henkin’s work. We prove our Lindenbaum Lemma using a Henkin-inspired strategy, witnessing ◊-prefixed expressions with nominals. Our use of general interpretations and the construction of the type hierarchy is (almost) pure Henkin. Finally, the generality of our completeness result is due to the first-order perspective, which lies at the heart of both Henkin’s best known work and hybrid logic.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Some authors bind nominals directly, forming expressions like ↓i(¬◊i). There is nothing wrong with this, but it seems neater to draw a syntactic distinction between state variables (which are open to binding) and nominals (which are not).
- 2.
In modal logic, the basic proof system is usually called K in honor of Saul Kripke. The three axiomatizations considered here are alternative ways of providing a basic proof system for HTT.
- 3.
These three approaches have a common evolutionary history. The earliest was the Paste plus Name combination found in K2. This was introduced in [7] in the setting of propositional tense logic with ↓ and used to prove analogs of Theorems 5 and 7 of this paper. The Bounded Generalization plus Name combination used in K1 was designed to provide a natural deduction style counterpart to the tableau style Paste rule. Balder ten Cate then showed how this combination could be refined (when ↓ is in the language) with the rules and axioms used in K3. For detailed explorations of the Bounded Generalization plus Name option and their simplifications with ↓, see [6] and [9]. Another nonorthodox hybrid proof rule (one which is useful even if we do not have @ in our language) is the COV rule of [11].
References
Areces, C., Blackburn, P., Huertas, A., Manzano, M.: Completeness in hybrid type theory. J. Philos. Log. 43, 209–238 (2014)
Areces, C., Blackburn, P., Marx, M.: Hybrid logics: characterization, interpolation and complexity. J. Symb. Log. 66(3), 977–1010 (2001)
Areces, C., ten Cate, B.: Hybrid logic. In: Handbook of Modal Logic, pp. 821–868. Elsevier, Amsterdam (2007)
Blackburn, P., De Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2002)
Blackburn, P., Seligman, J.: Hybrid languages. J. Log. Lang. Inf. 4(3), 251–272 (1995)
Blackburn, P., ten Cate, B.: Pure extensions, proof rules, and hybrid axiomatics. Stud. Log. 84, 277–322 (2006)
Blackburn, P., Tzakova, M.: Hybrid languages and temporal logic. Log. J. IGPL 7(1), 27–54 (1999)
Braüner, T.: Hybrid Logic and Its Proof-Theory. Applied Logic Series, vol. 37. Springer, Berlin (2010)
ten Cate, B.: Model theory for extended modal languages. Ph.D. thesis, University of Amsterdam. ILLC Dissertation Series DS-2005-01 (2005)
Feferman, S.: Persistent and invariant formulas for outer extensions. Compos. Math. 20, 29–52 (1968)
Gargov, G., Goranko, V.: Modal logic with names. J. Philos. Log. 22, 607–636 (1993)
Henkin, L.: The completeness of the first-order functional calculus. J. Symb. Log. 14(3), 159–166 (1949)
Henkin, L.: Completeness in the theory of types. J. Symb. Log. 15(2), 81–91 (1950)
Henkin, L.: The discovery of my completeness proofs. Bull. Symb. Log. 2(2), 127–158 (1996)
Manzano, M.: Extensions of First Order Logic. Cambridge University Press, Cambridge (1996)
Van Benthem, J., Doets, K.: Higher-order logic. In: Handbook of Philosophical Logic, pp. 275–329. Springer, Berlin (1983)
Acknowledgements
The authors are grateful to the Spanish Ministerio de Economía y Competitividad for funding the project Logica Intensional Hibrida (Hybrid Intensional Logic), FFI2013-47126-P, hosted by the Universidad de Salamanca.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Blackburn, P., Huertas, A., Manzano, M., Jørgensen, K.F. (2014). Henkin and Hybrid Logic. In: Manzano, M., Sain, I., Alonso, E. (eds) The Life and Work of Leon Henkin. Studies in Universal Logic. Birkhäuser, Cham. https://doi.org/10.1007/978-3-319-09719-0_19
Download citation
DOI: https://doi.org/10.1007/978-3-319-09719-0_19
Publisher Name: Birkhäuser, Cham
Print ISBN: 978-3-319-09718-3
Online ISBN: 978-3-319-09719-0
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)