2015/10/20 by Pedro Sánchez Terraf, Terraf, Pedro Sánchez
Computer Science · Mathematics · #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 #acm:03B20 #acm:03F03. #acm:03F55 #math.LO #msc:03B20 #msc:03F03. #msc:03F55
paper · pdf · doi:10.48550/arxiv.1510.05873
This paper has been withdrawn by the author. I was informed that this proof has already appeared in the book "Elements of logical reasoning" (CUP 2013) by Jan von Plato and uses a normalization result published in "Normal derivability in classical natural deduction," Jan von Plato and Annika Siders, Review of Symbolic Logic, 2012
openalex publication_date 2015/10/20 · arxiv created 2015/10/25 · arxiv updated 2015/10/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.