The McKinsey Axiom on Weakly Transitive Frames

The McKinsey axiom (M) □♦p → ♦□p has a local first-order correspondent on the class of all weakly transitive frames WT . It globally corresponds to Lemmon’s condition (m^∞) on WT . The formula (M) is canonical over the weakly transitive modal logic wK4 = K ⊕ p ∧ □p → □□p. The modal logic wK4.1 = wK4 ⊕ M has the finite model property. The modal logics wK4.1Tⁿ₀ (n > 0) form an infinite descending chain in the interval [wK4.1, K4.1] and each of them has the finite model property. Thus all the modal logics wK4.1 and wK4.1Tⁿ₀  (n > 0) are decidable.