Glivenko's theorem is a basic result showing a close connection between classical

Classical logic

Classical logic identifies a class of formal logics that have been most intensively studied and most widely used. The class is sometimes called standard logic as well...

 and intuitionistic

Intuitionistic logic

Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...

 propositional logic. It was proven by Valery Glivenko

Valery Ivanovich Glivenko

Valery Ivanovich Glivenko / January 2, 1897 in Kiev, died February 15, 1940 in Moscow) was a Soviet mathematician. He worked in foundations of mathematics and probability theory. He taught at Liebknecht University until his death at age 43....

 in 1929, with the aim of showing that intuitionistic logic is consistent and coherent. 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. Glivenko's theorem does not hold in general for quantified formulas; its generalization is the Kuroda negative translation

Gödel–Gentzen negative translation

In proof theory, the Gödel–Gentzen negative translation is a method for embedding classical first-order logic into intuitionistic first-order logic. It is one of a number of double-negation translations that are of importance to the metatheory of intuitionistic logic...

.