The topological product of S4 and S5
The most obvious bimodal logic generated from unimodal logics L1 and L2 is their fusion, L1 ⊗ L2, axiomatized by the theorems of L1 for
⬛1 and of L1 for ⬛2, and by the rules of modus ponens, substitution and necessitation for ⬛1 and for ⬛2. Shehtman introduced the frame product L1 × L2, as the logic of the products of certain Kripke frames.
Typically, L1 ⊗ L2 ⊊ L1 × L2, e.g. S4 ⊗ S4 ⊊ S4 × S4. Van Benthem, Bezhanishvili, ten Cate and Sarenac generalized Shehtman's idea and introduced the topological product L1 ×t L2, as the logic of the products
of certain topological spaces: they showed, in particular, that
S4 ×t S4 = S4 ⊗ S4. In this paper, we axiomatize S4 ×t S5, which is
strictly between S4 ⊗ S5 and S4 × S5. We also apply our techniques
to proving a conjecture of van Benthem et al concerning the logic of products of Alexandrov spaces with arbitrary topological spaces.