Yet Another Proof of Glivenko's Theorem

2015/10/20 by Pedro Sánchez Terraf, Terraf, Pedro Sánchez
Computer Science · #03B20 #Advanced Algebra and Logic #F.4.1 #FOS: Mathematics #I.2.3 #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Primary 03F03. Secondary 03F55

paper · pdf · doi:10.48550/arxiv.1510.05873

openalex publication_date 2015/10/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

In this short note we give an alternative proof of Glivenko's Theorem, stating that a formula ϕ is provable in classical propositional logic if and only if ¬¬ϕ is provable in intuitionistic propositional logic. We work in the natural deduction system by Gentzen, and the key lemma shows that in any proof one needs only one application of reductio ad absurdum.

Citations

• Untersuchungen �ber das logische Schlie�en. I

Related

• Classical logic and intuitionistic logic: equivalent formulations in natural deduction, Gödel-Kolmogorov-Glivenko translation
• Glivenko's theorem, finite height, and local tabularity
• Postponement of raa and Glivenko's theorem, revisited (extended version)
• An abstract approach to Glivenko's theorem
• Proofs of some Propositions of the semi-Intuitionistic Logic with Strong Negation