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

Propositional 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:
Glivenko's theorem implies the more general statement:
In particular, a set of propositional formulas is intuitionistically consistent if and only if it is classically satisfiable.

First-order logic

The Gödel–Gentzen translation 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 is ¬

and otherwise

^N is φ^N ∧ θ^N
^N is φ^N → θ^N
^N is ¬φ^N
^N is ∀x φ^N

This translation has the property that φ^N is classically equivalent to φ. Troelstra and Van Dalen give a description, due to Leivant, of formulas that do imply their Gödel–Gentzen translation in intuitionistic first-order logic also. There, this is not the case for all formulas.

Equivalent variants

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. One possibility can thus succinctly be described as follows: Prefix "¬¬" before every atomic formula, but also to every disjunction and existential quantifier,

^N is ¬¬
^N is ¬¬∃x φ^N

Another procedure, known as Kuroda's translation, is to construct a translated φ by putting "¬¬" before the whole formula and after every universal quantifier. This procedure exactly reduces to the propositional translation whenever φ is propositional.
Thirdly, one may instead prefix "¬¬" before every subformula of φ, as done by Kolmogorov. Such a translation is the logical counterpart to the call-by-name continuation-passing style translation of functional programming languages along the lines of the Curry–Howard correspondence between proofs and programs.
The Gödel-Gentzen- and Kuroda-translated formulas of each φ are provably equivalent to one another, and this result holds already in minimal propositional logic. And further, in intuitionistic propositional logic, the Kuroda- and Kolmogorov-translated formulas are equivalent also.
The mere propositional mapping of φ to ¬¬φ does not extend to a sound translation of first-order logic, as the so called double negation shift
is not a theorem of intuitionistic predicate logic. So the negations in φ^N have to be placed in a more particular way.

Results

Let T^N consist of the double-negation translations of the formulas in T.
The fundamental soundness theorem states:

Arithmetic

The double-negation translation was used by Gödel to study the relationship between classical and intuitionistic theories of the natural numbers. He obtains the following result:
This result shows that if Heyting arithmetic is consistent then so is Peano arithmetic. This is because a contradictory formula is interpreted as, which is still contradictory. Moreover, the proof of the relationship is entirely constructive, giving a way to transform a proof of in Peano arithmetic into a proof of in Heyting arithmetic.
By combining the double-negation translation with the Friedman translation, it is in fact possible to prove that Peano arithmetic is Π⁰₂-conservative over Heyting arithmetic.