Yet Another Proof of Glivenko's Theorem

TL;DR

This paper presents an alternative proof of Glivenko's Theorem using natural deduction, demonstrating that only one application of reductio ad absurdum is needed in proofs.

Contribution

It provides a new proof of Glivenko's Theorem within Gentzen's natural deduction framework, simplifying the proof process.

Findings

Proof shows only one application of reductio ad absurdum is necessary

Establishes equivalence between classical and intuitionistic provability for formulas

Uses natural deduction system for the proof

Abstract

In this short note we give an alternative proof of Glivenko's Theorem, stating that a formula $\phi$ is provable in classical propositional logic if and only if $\neg\neg\phi$ 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.