Decision procedures for Intuitionistic logic and for modal logic S4 by 3-valued non-deterministic matrices

Abstract: In 1932 Gödel proved that it is impossible to characterize intuitionistic propositional logic (IPL) by a single finite logical matrix, that is, by finite-valued truth-tables. By adapting Gödel's proof, J. Dugundji proved in 1940 that no modal system between Lewis' S1 and S5 can be characterized by a single finite logical matrix. That is, the usual modal logics are also not characterizable by finite-valued truth-tables. As a way to overcome Dugundji’s result, J. Kearns introduced in 1981 a 4-valued non-deterministic matrix (Nmatrix, for short) for modal logics KT, S4, and S5 in which just a subset of the valuations are allowed (that valuations are called "level valuations"). He proved that this restricted Nmatrix (RNmatrix, for short) constitutes a sound and complete semantics for these modal logics. However, Kearns’s level valuations fail to provide an effective decision procedure for these modal logics. Recently, L. Grätz refined Kearn’s original RNmatrix to obtain a decidable 3-valued RNmatrix for modal logics KT and S4, by using an appropriate notion of partial valuation for level semantics. Thanks to the conservative translation from IPL into S4 introduced by Gödel in 1933 (which is also computable), by composing both algorithms a decision procedure for IPL is obtained.

In this talk the Grätz algorithm will be described, as well as a new algorithm for deciding validity in IPL obtained by considering another translation derived from Gödel's one. It allows defining the composed algorithm for IPL above mentioned, but in a direct way, hence the soundness and completeness of the method is proved independently of Gödel and Grätz results. In this way, an original 3-valued RNmatrix for IPL is defined, with a very natural interpretation, as well as an easy algorithm which allows to remove, from the truth tables generated by the 3-valued Nmatrix, those rows which are not sound. This decision procedure, as well as Grätz's one, were implemented in Coq. This is a joint work with Renato Leme and Bruno Lopes.

logic

Audience: researchers in the topic

Online logic seminar

Series comments: Description: Seminar on all areas of logic