Double-negation translation

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.

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

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.

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.