FLAP Journal 2021 Journal Article
Glivenko's Theorem, Finite Height, and Local Tabularity.
- Ilya B. Shapirovsky
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.