Yet Another Proof of Glivenko's Theorem
Logic
2015-10-27 v2
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.
Cite
@article{arxiv.1510.05873,
title = {Yet Another Proof of Glivenko's Theorem},
author = {Pedro Sánchez Terraf},
journal= {arXiv preprint arXiv:1510.05873},
year = {2015}
}
Comments
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