Gödel–Gentzen negative translation

From Wikipedia, the free encyclopedia

In proof theory, the Gödel-Gentzen negative translation is a method for embedding classical first-order logic into intuitionistic first-order logic.

[edit] Definition

The translation associates with each formula φ in a first-order theory another formula φ^N, which is defined inductively:

If φ is atomic, then φ^N is ¬ ¬ (φ)
(φ ∧ θ)^N is φ^N ∧ θ^N
(φ ∨ θ)^N is ¬(¬ φ^N ∧ ¬ θ^N)
(φ → θ)^N is φ^N → θ^N
(¬ φ)^N is ¬ φ^N
(∀ x φ)^N is ∀ x φ^N
(∃ x φ)^N is ¬ ∀ x ¬ φ^N

[edit] Results

The negative translation of a formula is classically equivalent to the formula, but weaker than the original formula in intuitionistic logic. However, a formula φ is provable in classical logic if and only if φ^N is provable intuitionistically. Gödel used this to show that intuitionistic logic and classical logic are either both consistent or both inconsistent.