Projective unification in transitive modal logics
Sławomir Kost · Logic Journal of IGPL · 2018
We show that a transitive normal modal logic L enjoys projective unification (i.e. each unifiable formula is projective) if and only if L contains K4D1 (|${\textsf{D1}}\colon \Box (\Box x \to y)\lor \Box (\Box y \to x)$|). It means, in particular, that K4D1 (and any of its extensions) is almost structurally complete, i.e. the logic is complete with respect to all non-passive admissible rules. We also characterize non-unifiable formulas and provide an explicit form of the basis for all passive rules over |${\textsf{K4G}} + \Box (\Box x\to x).$|