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

Results

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.

First-order logic

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 φ. 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 in intuitionistic first-order logic also. There, this is not the case for all formulas. (This is related to the fact that propositions with additional double-negations can be stronger than their simpler variant. E.g., ¬¬φ → θ always implies φ → θ, but the schema in the other direction would imply double-negation elimination.)

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 ∨ θ^N)
• (∃x φ)^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 provenly 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

∀x ¬¬φ(x) → ¬¬∀x φ(x)

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 (Avigad and Feferman 1998, p. 342; Buss 1998 p. 66) states:

If T is a set of axioms and φ is a formula, then T proves φ using classical logic if and only if T^N proves φ^N using intuitionistic logic.

Arithmetic

The double-negation translation was used by Gödel (1933) to study the relationship between classical and intuitionistic theories of the natural numbers ("arithmetic"). He obtains the following result:

If a formula φ is provable from the axioms of Peano arithmetic then φ^N is provable from the axioms of Heyting arithmetic.

This result shows that if Heyting arithmetic is consistent then so is Peano arithmetic. This is because a contradictory formula θ ∧ ¬θ is interpreted as θ^N ∧ ¬θ^N, 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 θ^N ∧ ¬θ^N 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.