Decidable properties of logical calculi and of varieties of algebras

Summary

Abstract. We give an overview of decidable and strongly decidable properties over the propositional modal logics K, GL, S4, S5 and Grz, and also over the intuitionistic logic Int and the positive logic Int⁺.

We consider a number of important properties of logical calculi: consistency, tabularity, pretabularity, local tabularity, various forms of interpolation and of the Beth property. For instance, consistency is decidable over K and strongly decidable over S4 and Int; tabularity and pretabularity are decidable over S4, Int and Pos; interpolation is decidable over S4 and Int⁺ and strongly decidable over S5, Grz and Int; the projective Beth property is decidable over Int, Int⁺ and Grz, etc. Some complexity bounds are found.

In addition, we state that tabularity and many variants of amalgamation and of surjectivity of epimorphisms are base-decidable in varieties of closure algebras, of Heyting algebras and of relatively pseudocomplemented lattices.

Introduction. Propositional calculi are usually defined by systems of axioms schemes and rules of inference. Natural problems arising in general study of logical calculi, for example, the problemof equivalence or the problem of determining for arbitrary calculus whether it is consistent or not, are, in general, undecidable. The first undecidability results for propositional calculi were found by S. Linial and E. Post in 1949 [16]. In particular, it was proved that the property “to be an axiomatization of the classical propositional logic” is undecidable. In 1963 A. V. Kuznetsov [13] found an essential extension of this result. He proved that for every superintuitionistic logic L the property “to be an axiomatization of L” is undecidable. In particular, consistency andmany other properties of calculi are, in general, undecidable. In [3] A. V. Chagrov has given a survey of results on undecidable properties of propositional calculi. Here we concentrate on decidable properties.

When we restrict ourself by considering particular families of calculi, for instance, propositional calculi extending intuitionistic or some modal logic, many important properties of calculi appear to be decidable (see a survey in [4]). When the rules of inference are fixed, for any given finite system of additional axioms, one can effectively decide consistency problem for normal modal logics, tabularity and interpolation problems for extensions of the intuitionistic logic or of the modal system S4 and some other problems.