Glivenko's theorem

It has been suggested that this article or section be merged into Gödel–Gentzen negative translation. (Discuss)

Glivenko's theorem is a basic result showing a close connection between classical and intuitionistic propositional logic. It was proven by Valery Glivenko in 1929, with the aim of showing that intuitionistic logic is consistent and coherent.^[1] The theorem was proven relative to an axiomatisation of intuitionistic logic provided by Glivenko, one of the first attempts to axiomatise the logic.

Statement

Glivenko's theorem states that whenever P → Q is a theorem of classical propositional logic, then ¬¬P → ¬¬Q is a theorem of intuitionistic propositional logic. Similarly, ¬¬P is a theorem of intuitionistic propositional logic if and only if P is a theorem of classical propositional logic.^[2] Glivenko's theorem does not hold in general for quantified formulas; its generalization is the Kuroda negative translation.

Notes

References

• van Atten, M. (2008). 'The development of intuitionistic logic'. Stanford Encyclopedia of Philosophy. S
• Glivenko, V. (1929). Sur quelques points de la logique de M. Brouwer'. In Bulletins de la classe des sciences, ser. 5, vol. 15:183–188. Academie Royale de Belgique.
• Trolestra, A. S.; van Dalen, D. (1988). Constructivism in mathematics, 2 volumes. Amsterdam: North-Holland.
• J. Moschovakis (2008). 'Intuitionistic Logic'. The Stanford Encyclopedia of Philosophy.
• Sørensen, M. H. B.; Urzyczyn, P. (2006). Lectures on the Curry-Howard Isomorphism. Studies in Logic and the Foundations of Mathematics. Elsevier. ISBN 0444520775. 

This logic-related article is a stub. You can help Wikipedia by expanding it.