Event Detail

Saul Kripke published in 1959 a proof of completeness for first-order S5 modal logic [7] and in 1963 he extended the method to cover the propositional modal systems T, S4, S5, and B [8]. His method employed a generalization of Beth’s tableaux and completeness was established by showing how to derive a proof from a failed attempt to find a counter model.

In 1966, Kaplan criticized Kripke’s proof in his review of Kripke’s article [6] and suggested a different and, arguably, more elegant approach based on an adaptation of Henkin’s model theoretic completeness proof for first-order logic [5]. (Actually, completeness proof for S5 following Henkin’s ideas had already been published in 1959 in an article by Bayart [2], and other proofs were been published at about the time of Kaplan’s by Makinson in 1966 [9] and Cresswell in 1967 [4].)

Henkin’s proof of completeness for first-order logic used to important ideas: 1) that a consistent set of formulas can be extended to a maximally consistent set of formulas, and 2) that existential quantifiers can be witnessed using constants, which can then be used to form the domain of the model. The first of these two ideas is fundamental in modern completeness proofs for classical propositional modal logics which build a canonical model (satisfying all consistent formulas) that has as domain the (uncountable) set of all maximally consistent sets of formulas. The second idea (the use of witnesses) seemed less useful in the propositional setting — till the arrival of hybrid modal logics [1].

One of the main characteristic of hybrid modal logics is the inclusion of nominals which are special propositional symbols that name particular states in the model. This “naming” is achieved by restricting the interpretation of nominals to be singleton sub- sets of the domain. Nominals can be used as witnesses for the modal existential oper- ators and, in this way, the completeness construction needs to build just a single max- imal, witnessed consistent set of formulas from which a countable model is built (see, e.g., [3, Chap 7.3] and [10]). As a side-effect a particularly strong completeness result can be proved, that establishes that it is possible to give a complete axiomatic system for the basic hybrid logic, which remains complete under the extension with a particular family of axioms w.r.t. the corresponding class of models.

[1] C. Areces and B. ten Cate., Hybrid logics, Handbook of Modal Logics, (P. Blackburn, F. Wolter, and J. van Benthem), Elsevier, 2006, pp. 821–868.

[2] A. Bayart, Quasi-adequation de la logique modale de 2eme ordre, Logique et analyse, vol. 2 (1959), no. 6/7 pp. 99–121.

[3] P. Blackburn, M. De Rijke, and Y. Venema, Modal Logic, Cambridge University Press, Cambridge, 2002.

[4] M. Cresswell, A Henkin completeness for T , Notre Dame Journal of For- mal Logic, vol. 8 (1967), no. 3 pp. 186–190.

[5] L. Henkin, The completeness of the first-order functional calculus, The Journal of Symbolic Logic, vol. 14 (1949), no. 3, pp. 159–166.

[6] D. Kaplan, Review: Saul A. Kripke, semantical analysis of modal logic i. normal modal propositional calculi, The Journal of Symbolic Logic, vol. 31 (1966), no. 1, pp. 120–122.

[7] S. Kripke, A completeness theorem in modal logic, The Journal of Symbolic Logic, vol. 24 (1959), no. 1, pp. 1–14.

[8] S. Kripke, Semantical analysis of modal logic i. normal modal propositional calculi, Zeitschrift fur mathematische Logik und Grundlagen der Mathematik, vol. 9 (1963), no. 5-6, pp. 67–96.

[9] D. Makinson, On some completeness theorems in modal logic, Zeitschrift fur mathematische Logik und Grundlagen der Mathematik, vol. 12 (1966), no. 1, pp. 379–384.

[10] B. ten Cate, Model theory for extended modal languages. PhD thesis, Univer- sity of Amsterdam, 2005.