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 ` ϕ iff IL ` ¬¬ϕ. Its analog for the modal logics S5 and S4 states that S5 ` ϕ iff S4 ` ¬2¬2ϕ. 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.

Authors

• Ilya B. Shapirovsky

Keywords

• Glivenko’s translation
• modal logic
• intermediate logic
• finite height