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.

[edit] References

"Intuitionistic logic", Stanford Encyclopedia of Philosophy.