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 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 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
TN consist of the double-negation translations of the formulas in
T. The fundamental soundness theorem states: :If
T is a set of axioms and φ is a formula, then
T proves φ using classical logic if and only if
TN 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 , 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
Π02-
conservative over Heyting arithmetic. == See also ==