Seminário remoto "Lógicos em Quarentena" 06/08/2020 (quinta-feira) 16:00h

[Bruno Lopes]

Numa iniciativa conjunta da Sociedade Brasileira de Lógica e do Grupo de Interesse em Lógica da Sociedade Brasileira de Computação, gostaríamos de convidar a todos a participarem do Seminário "Lógicos em Quarentena". Trata-se de um seminário remoto com apresentações informais por membros da comunidade e espaço para perguntas no fim. As apresentações usualmente são gravadas e disponibilizadas na página do evento http://lq.sbl.org.br (com a agenda completa).

Data: 06 de agosto de 2020 (quinta-feira)
Horário: 16:00h
Apresentador: Carlos Areces (UNC & CONICET)
Título: Henkin Completeness in Modal Logic (with an application to semi-structured databases)
Resumo: 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 published at about the same 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 (witnesses) seemed less useful in the propositional setting — till the arrival of hybrid modal logics [1]. One of the main characteristics 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 maximal, 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. Together with Raul Fervari, we have recently extended these results to provide general strong completeness results for an axiomatization of XPath, a query language for semi-structured databases. [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.
A apresentação ocorrerá pelo Google Meet através do link público http://meet.google.com/eoq-uibs-atw .

--

Bruno Lopes

Professor Adjunto

Instituto de Computação

Universidade Federal Fluminense

http://www.ic.uff.br/~bruno