BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Marcelo E. Coniglio (University of Campinas (UNICAMP)) DTSTART:20240502T180000Z DTEND:20240502T190000Z DTSTAMP:20260423T035931Z UID:OLS/154 DESCRIPTION:Title: De cision procedures for Intuitionistic logic and for modal logic S4 by 3-val ued non-deterministic matrices\nby Marcelo E. Coniglio (University of Campinas (UNICAMP)) as part of Online logic seminar\n\n\nAbstract\nIn 1932 Gödel proved that it is impossible to characterize\nintuitionistic propo sitional logic (IPL) by a single finite logical\nmatrix\, that is\, by fin ite-valued truth-tables. By adapting Gödel's\nproof\, J. Dugundji proved in 1940 that no modal system between Lewis'\nS1 and S5 can be characterize d by a single finite logical matrix. That\nis\, the usual modal logics are also not characterizable by finite-valued\ntruth-tables. As a way to over come Dugundji’s result\, J. Kearns\nintroduced in 1981 a 4-valued non-de terministic matrix (Nmatrix\, for\nshort) for modal logics KT\, S4\, and S 5 in which just a subset of the\nvaluations are allowed (that valuations a re called "level\nvaluations"). He proved that this restricted Nmatrix (RN matrix\, for\nshort) constitutes a sound and complete semantics for these modal\nlogics. However\, Kearns’s level valuations fail to provide an\ne ffective decision procedure for these modal logics. Recently\, L.\nGrätz refined Kearn’s original RNmatrix to obtain a decidable 3-valued\nRNmatr ix for modal logics KT and S4\, by using an appropriate\nnotion of partial valuation for level semantics.\nThanks to the conservative translation fr om IPL into S4 introduced by\nGödel in 1933\n(which is also computable)\, by composing both algorithms a decision\nprocedure for IPL is obtained.\n \nIn this talk the Grätz algorithm will be described\, as well as a new a lgorithm\nfor deciding validity in IPL obtained by considering another tra nslation\nderived from Gödel's one. It allows defining the composed algor ithm\nfor IPL above mentioned\, but in a direct way\, hence the soundness and\ncompleteness of the method is proved independently of Gödel and Grä tz results.\nIn this way\, an original 3-valued RNmatrix for IPL is define d\, with a\nvery natural\ninterpretation\, as well as an easy algorithm wh ich allows to remove\,\nfrom the truth\ntables generated by the 3-valued N matrix\, those rows which are not\nsound. This decision\nprocedure\, as we ll as Grätz's one\, were implemented in Coq. This is a\njoint work with R enato\nLeme and Bruno Lopes.\n LOCATION:https://researchseminars.org/talk/OLS/154/ END:VEVENT END:VCALENDAR