Interpolation in weakly transitive modal logics (Q694243)

The paper establishes decidability of weakened versions of Craig interpolation for two classes of modal propositional logics, namely, the classes of normal modal logics extending the systems wK4 and DL, respectively. Of these two, wK4 is just the basic system K plus the following weak version of transitivity: \[ (A \wedge \square A) \to \square\square A, \] whereas DL is wK4 plus the Brouwer (symmetry) axiom \(A \to \square\lozenge A\). The author uses algebraic semantics for modal logic so she mostly speaks about, say, DL-algebras rather than DL-frames. The paper relies heavily on the earlier results obtained by the author herself and by L. Maksimova; more than 50\% of the text is devoted to an exposition of preliminaries and of a dozen theorems from earlier papers. The author basically builds upon an earlier result that there are exactly 16 extensions of DL that enjoy the so-called deductive interpolation property. She then defines formulas that can play the role of characteristic formulas for an important class of finite DL-algebras so that an algebra from this class will be a model of a given extension of DL iff its characteristic formula is NOT a theorem of DL. These characteristic formulas are then used to give finite axiomatizations of the 16 extensions mentioned above in a pretty straightforward way. The author then uses the fact that checking whether a given extension of DL by a given list of new axioms coincides with one of these 16 extensions can be done by checking that the additional axioms are FALSE in the algebras corresponding to the characteristic formulas used as the axioms in this latter extension. This provides a decision procedure for the deductive interpolation property in the extensions of DL. As a corollary, the author obtains decidability of the weak interpolation property for logics extending wK4 using an earlier result that an extension of DL with new axioms \(A\) has deductive interpolation iff the extension of wK4 with these same axioms has the weak interpolation property.