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

TL;DR

This paper establishes the finite axiomatization of the combined modal logics $ extbf{GL} imes extbf{S5}$ and $ extbf{Grz} imes extbf{S5}$, resolving a long-standing open problem in modal logic.

Contribution

It proves that $ extbf{GL} imes extbf{S5}$ is product matching and provides a finite axiomatization for $ extbf{Grz} imes extbf{S5}$ by extending existing systems.

Findings

$ extbf{GL} imes extbf{S5}$ is product matching.

$ extbf{Grz} imes extbf{S5}$ is finitely axiomatizable.

Resolved the open problem posed by Gabbay and Shehtman (1998).

Abstract

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