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

### 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 Π$^0$$_2$-conservative over Heyting arithmetic.