Gödel–Gentzen negative 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 by translating formulas to formulas which are classically equivalent but intuitionistically inequivalent. Particular instances of double-negation translation 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:

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.

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:

This translation has the property that φ^N is classically equivalent to φ. The fundamental soundness theorem states:

Here T^N consists of the double-negation translations of the formulas in T.

A sentence φ may not imply its negative translation φ^N in intuitionistic first-order logic. Troelsta and Van Dalen give a description (due to Leivant) of formulas that do imply their Gödel–Gentzen translation.

There are several alternative definitions of the negative translation. They are all provably equivalent in intuitionistic logic, but may be easier to apply in particular contexts.

One possibility is to change the clauses for disjunction and existential quantifier to

Then the translation can be succinctly described as: prefix ¬¬ to every atomic formula, disjunction, and existential quantifier.

Another possibility (known as Kuroda's translation) is to construct φ^N from φ by putting ¬¬ before the whole formula and after every universal quantifier. Notice that this reduces to the simple ¬¬φ translation if φ is propositional.

...
Wikipedia