Finite axiomatization of $\text{GL}\times \text{S5}$ and $\text{Grz}\times \text{S5}$

Abstract

We prove that $\mathbf{GL}\times S5$ is product matching, and that $\mathbf{Grz}\times S5$ is axiomatizable by adding to $[\mathbf{Grz},S5]$ the Gödel translation of the monadic Casari formula. This settles the question of the finite axiomatizability of these logics posed by Gabbay and Shehtman (1998).