The universal modality, the center of a Heyting algebra, and the Blok–Esakia theorem

We introduce the bimodal logic S4.Grz u , which is the extension of Bennett’s bimodal logic S4 u by Grzegorczyk’s axiom □ ( □ ( p → □ p ) → p ) → p and show that the lattice of normal extensions of the intuitionistic modal logic WS5 is isomorphic to the lattice of normal extensions of S4.Grz u , thus generalizing the Blok–Esakia theorem. We also introduce the intuitionistic modal logic WS5.C, which is the extension of WS5 by the axiom ∀ ( p ∨ ¬ p ) → ( p → ∀ p ) , and the bimodal logic S4.Grz u C , which is the extension of Shehtman’s bimodal logic S4 u C by Grzegorczyk’s axiom, and show that the lattice of normal extensions of WS5.C is isomorphic to the lattice of normal extensions of S4.Grz u C .