Glivenko's theorem
From Wikipedia, the free encyclopedia
In logic, Glivenko's theorem states that whenever P → Q is a theorem of classical logic, ¬¬P → ¬¬Q is a theorem of intuitionistic logic. Similarly, ¬¬x is a theorem of intuitionistic logic whenever x is a theorem of classical logic.[1]
[edit] References
- Trolestra, A. S.. Constructivism in mathematics, 106.
- Sørensen, Morten Heine B; Pawel Urzyczyn (2006). Lectures on the Curry-Howard Isomorphism, Studies in Logic and the Foundations of Mathematics. Elsevier. ISBN 0444520775.
- ^ Sørensen, p. 42
 |
This logic-related article is a stub. You can help by expanding it. |
