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.
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.