Double-negation translation

In proof theory, a discipline within mathematical logic, double-negation translation, sometimes called negative translation, is a general approach for embedding classical logic into intuitionistic logic. Typically it is done by translating formulas to formulas which are classically equivalent but intuitionistically inequivalent. Particular instances of double-negation translations include Glivenko's translation for propositional logic, and the Gödel–Gentzen translation and Kuroda's translation for first-order logic. The easiest double-negation translation to describe comes from Glivenko's theorem, proved by Valery Glivenko in 1929. It maps each classical formula φ to its double negation ¬¬φ. Glivenko's theorem states: If φ is a propositional formula, then φ is a classical tautology if and only if ¬¬φ is an intuitionistic tautology. Glivenko's theorem implies the more general statement: If T is a set of propositional formulas and φ a propositional formula, then T ⊢ φ in classical logic if and only if T ⊢ ¬¬φ in intuitionistic logic. In particular, a set of propositional formulas is intuitionistically consistent if and only if it is classically satisfiable. The Gödel–Gentzen translation (named after Kurt Gödel and Gerhard Gentzen) associates with each formula φ in a first-order language another formula φN, which is defined inductively: If φ is atomic, then φN is ¬¬φ as above, but furthermore (φ ∨ θ)N is ¬(¬φN ∧ ¬θN) (∃x φ)N is ¬(∀x ¬φN) and otherwise (φ ∧ θ)N is φN ∧ θN (φ → θ)N is φN → θN (¬φ)N is ¬φN (∀x φ)N is ∀x φN This translation has the property that φN is classically equivalent to φ. But in intuitionistic first-order logic, neither direction is necessarily provable. Troelstra and van Dalen (1988, Ch. 2, Sec. 3) give a description, due to Leivant, of formulas that do imply their Gödel–Gentzen translation. Due to constructive equivalences, there are several alternative definitions of the translation. For example, a valid De Morgan's law allows one to rewrite a negated disjunction.