Upcoming Events

Logic Colloquium

April 13, 2018, 4:00 PM (60 Evans)

Carlos Eduardo Areces
Professor of Computer Science, Universidad Nacional de Córdoba, Argentina

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] 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, University of Amsterdam, 2005.

Logic Colloquium

April 27, 2018, 4:10 PM (60 Evans Hall)

Vaughan Pratt
Professor Emeritus of Computer Science, Stanford University

The Class CAT of Locally Small Categories as a Functor-Free Framework for Foundations and Philosophy

Exploiting an evident circularity, we give three elementary properties of the category Set that uniquely determine it up to equivalence within the class CAT of locally small categories. The analogous three properties extend this result to many other categories of interest in algebra, topology, type theory, and philosophy via a framework which structures categories with nothing more than distinguished objects each serving as either a primitive representative of a given sort such as cat or box, or a palette of sorted values for a given property such as color or mass. The notion of property thereby defined is as extensional as the notion of sort. In those categories catering for both sorts and and properties, qualia of sort s for property p arise ambiguously as sort-s members of the palette p and as p-states of the primitive s, for example calico as a possible color for a cat. This framework provides a paradox-free interpretation of C.I. Lewis’s notion of qualia as well as serving the function of the pituitary gland in Descartes’ mind-body dualism. While functors and natural transformations underpin the whole framework we exploit the Yoneda embedding to hide them beneath the framework’s more elementary conceptual language