2018/06/18 by Ilya Shapirovsky, Shapirovsky, Ilya B. · 1 citation
Computer Science · #03B45 #03B55 #20F10 #Advanced Algebra and Logic #F.4.1 #FOS: Mathematics #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1806.06899
openalex publication_date 2018/06/18 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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\vdashφ iff IL\vdash¬¬φ. Its analog for the modal logics S5 and S4 states that S5\vdash φ iff S4 \vdash ¬ \Box ¬ \Box φ. 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.