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 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 ¬¬φ. 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 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
:
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 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 , 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 Π⁰₂-conservative over Heyting arithmetic.

See also

* Dialectica interpretation
* Modal companion

Notes

References

*
*
*
*
*
*
*
*
#
#

External links

*
Intuitionistic logic
, Stanford Encyclopedia of Philosophy.
*

{{DEFAULTSORT:Godel-Gentzen negative translation
Proof theory
Intuitionism