Finite non-deterministic semantics for some modal systems

摘要

Trying to overcome Dugundji's (1940) result on uncharacterisability of modal logics by finite logical matrices, Kearns (1981) and Ivlev (1988) proposed, independently, a characterisation of some modal systems by means of four-valued multivalued truth-functions (by restricting the valuations using level valuations, in Kearns's approach), as an alternative to Kripke semantics. This constitutes an antecedent of the non-deterministic matrices introduced by Avron and Lev (2001). In this paper we propose a reconstruction of Kearns's and Ivlev's results (which did not have the dissemination or impact they deserved) in a uniform way, obtaining an extension to another modal systems. The first part of the paper is devoted to four-valued Nmatrices, including Kearns's and Ivlev's. Besides proving with full details Kearns's results for T, S4 and S5, we also obtain a characterisation of the system B by four-valued Nmatrices with level valuations. Concerning Ivlev's results, two new modal systems are introduced and characterised by Nmatrices. In the second part of this paper, six-valued Nmatrices are introduced which characterise a variant of the eight systems studied in the first part, by replacing axiom (T) with axiom (D). As a by-product, novel decision procedures for T, S4, S5, D, KDB, KD4 and KD45 are obtained, which open up interesting possibilities in the study of the complexity of modal logics and, in particular, of intuitionistic propositional logic (IPC), taking into account the Godel-McKinsey-Tarski translation between IPC and S4.