Glivenko'S Theorem, Finite Height, And Local Tabularity

Glivenko's theorem states that a formula is derivable in classical propositional logic CL iff under the double negation it is derivable in intuitionistic propositional logic IL: CL proves phi iff IL proves sic sic phi. Its analog for the modal logics S5 and S4 states that S5 proves phi iff S4 proves sic square sic square phi. In Kripke semantics, IL is the logic of partial orders, and CL is the logic of partial orders of height 1. Likewise, S4 is the logic of preorders, and 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.