Gödel–Gentzen negative translation

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

Results

The double-negation translation is used to obtain the following relationship between classical and intuitionistic logic (Avigad and Feferman 1998, p. 342; Buss 1998 p. 66):

• If a set S of axioms proves a formula φ using classical logic, then S^N proves φ^N in intuitionistic logic. Here S^N consists of the double-negation translations of the formulas in S.

Thus result reduces the consistency of classical logic to that of intuitonistic logic. This is because a contradictory formula is interpreted as , which is still contradictory. Morevover, the proof of the relationship is entirely constructive, giving a way to transform a classical proof of into an intuitionistic proof of . This relative consistency proof was first obtained by Kolmogorov in 1925 (Troelstra 1977, p. 986) using a similar translation; the modern form of the double-negation translation is due to Gentzen (1936).

The double-negation translation was used by Gödel (1933) to study the relationship between classical and intutionistic 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 intuitionistic Heyting arithmetic.

This result shows that if Heyting arithmetic is consistent then so is Peano arithmetic. As before, the proof gives a constructive method for obtaining an intuitionistic proof of a contradiction in Heyting arithmetic from a classical proof of a contradiction in Peano arithmetic.

See also

• Dialectica interpretation

References

• J. Avigad and S. Feferman (1998), "Gödel's Functional ("Dialectica") Interpretation", Handbook of Proof Theory, S. Buss, ed., Elsevier. ISBN 0-444-89840-9
• S. Buss (1998), "Introduction to Proof Theory", Handbook of Proof Theory, S. Buss, ed., Elsevier. ISBN 0-444-89840-9
• G. Gentzen (1936), "Die Widerspruchfreiheit der reinen Zahlentheorie", Mathematische Annalen, v. 112, pp. 493–565 (German). Reprinted in English translation as "The consistency of arithmetic" in The collected works of Gerhard Gentzen, M. E. Szabo, ed.
• K. Gödel (1933), "Zur intuitionistischen Arithmetik und Zahlentheorie", Ergebnisse eines mathematische Kolloquiums, v. 4, pp. 34–38 (German). Reprinted in English translation as "On intuitionistic arithmetic and number theory" in The Undecidable, M. Davis, ed., pp. 75–81.
• A. N. Kolmogorov (1925), "O principe teritium non datur" (Russian). Reprinted in English translation as "On the principle of the excluded middle" in From Frege to Gödel, van Heijenoort, ed., pp. 414–447.
• A. S. Troelsta (1977), "Aspects of Constructive Mathematics", ''Handbook of Mathematical Logic", J. Barwise, ed., North-Holland. ISBN 0-7204-2285-X

External links

• " Intuitionistic logic", Stanford Encyclopedia of Philosophy.