Glivenko's theorem, finite height, and local tabularity

Abstract

Glivenko's theorem states that a formula is derivable in classical propositional logic $\mathrm{CL}$ iff under the double negation it is derivable in intuitionistic propositional logic $\mathrm{IL}$: $\mathrm{CL}\vdash\varphi$ iff $\mathrm{IL}\vdash\neg\neg\varphi$. Its analog for the modal logics $\mathrm{S5}$ and $\mathrm{S4}$ states that $\mathrm{S5}\vdash \varphi$ iff $\mathrm{S4} \vdash \neg \Box \neg \Box \varphi$. In Kripke semantics, $\mathrm{IL}$ is the logic of partial orders, and $\mathrm{CL}$ is the logic of partial orders of height 1. Likewise, $\mathrm{S4}$ is the logic of preorders, and $\mathrm{S5}$ is the logic of equivalence relations, which are preorders of height 1. In this paper we generalize Glivenko's translation for logics of arbitrary finite height.