**carlos.arecesgmail.com**

Henkin Completeness in Modal Logic

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] as lacking in rigor and as making excessive use of “intuitive” arguments on the geometry of tableau proofs. More importantly, Kaplan 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 a little known 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 (at least) 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.

Carlos Areces is currently a Full Professor at the Computer Science Section of the Facultad de Matemática, Astronomía, Física y Computación, Universidad Nacional de Córdoba, where he is the director of the Logics, Interaction and Intelligent Systems (LIIS) Group. Since 2010, he is also a Researcher of the Consejo Nacional de Investigaciones Científicas y Técnicas (CONICET).

He received his doctoral degree in Computer Science from the Universiteit van Amsterdam, The Netherlands in 2000, where he was a researcher at the Institute for Logic, Language and Computation. After his doctoral studies he was an INRIA Researcher at the Lorraine Research Laboratory in Computer Science and its Applications, Nancy, France, a research unit common to CNRS, the University of Lorraine and INRIA.

His main area of interest is Computational Logic, with special emphasis in Modal Logic. He has carried out research in model theory, computational complexity, artificial intelligence, automated reasoning and computational linguistics, among others.