Glivenko's theorem, finite height, and local finiteness

The well-known Glivenko's theorem (1929) states that a formula is derivable in the classical propositional logic CL iff under the double negation it is derivable in the intuitionistic propositional logic IL. Modal analog of this theorem translates $\mathsf{S5}$ to $\mathsf{S4}$ (Matsumoto, 1955; Rybakov, 1992).
In Kripke semantics, the intuitionistic propositional logic is the logic of partial orders; the classical propositional logic is the logic of partial orders of height 1. Likewise for logics $\mathsf{S4}$ and $\mathsf{S5}$: $\mathsf{S4}$ is the logic of preorders, and $\mathsf{S5}$ is the logic of equivalence relations, which are preorders of height 1.
In this talk I will generalize Glivenko's theorem for the case of arbitrary finite height. Namely, for a logic $\mathsf{L}$ and a finite $h$, let $\mathsf{L}[h]$ be the extension of $\mathsf{L}$ with the formula of height $h$: e.g., $\mathsf{CL}=\mathsf{Int}[1]$, $\mathsf{S5}=\mathsf{S4}[1]$. I will describe translations from $\mathsf{L}[h+1]$ to $\mathsf{L}$ for the cases $\mathsf{L}=\mathsf{Int}$, $\mathsf{L}=\mathsf{S4}$, and more generally, for arbitrary modal logic $\mathsf{L}$ such that $\mathsf{L}[h]$ is locally finite.
arxiv.org/pdf/1806.06899.pdf