In proof theory

Proof theory

Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...

, the Gödel–Gentzen negative translation is a method for embedding classical first-order logic

First-order logic

First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...

 into intuitionistic

Intuitionistic logic

Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...

 first-order logic. It is one of a number of double-negation translations that are of importance to the metatheory of intuitionistic logic. It is named after logicians Kurt Gödel

Kurt Gödel

Kurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...

 and Gerhard Gentzen

Gerhard Gentzen

Gerhard Karl Erich Gentzen was a German mathematician and logician. He had his major contributions in the foundations of mathematics, proof theory, especially on natural deduction and sequent calculus...

.

Propositional logic

The easiest double-negation translation to describe comes from Glivenko's theorem

Glivenko's theorem

Glivenko's theorem is a basic result showing a close connection between classical and intuitionistic propositional logic. It was proven by Valery Glivenko in 1929, with the aim of showing that intuitionistic logic is consistent and coherent...

. It maps each classical formula φ to its double negation ¬¬φ.

Glivenko's theorem states:

If T is a set of propositional formulas and φ a propositional formula, then T proves φ using classical logic if and only if T proves ¬¬φ using intuitionistic logic.

In particular, a set of propositional formulas is intuitionistically consistent if and only if it is classically satisfiable.

First-order logic

The translation associates with each formula φ in a first-order language 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

Notice that φ^N is classically equivalent to φ.

The fundamental soundness theorem states:

If T is a set of axioms and φ a formula, then T proves φ using classical logic if and only if T^N proves φ^N using intuitionistic logic.

Here T^N consists of the double-negation translations of the formulas in T.

Note that φ need not imply its negative translation φ^N in intuitionistic first-order logic. Troelsta and Van Dalen give a description (due to Leivant) of formulas which do imply their Gödel–Gentzen translation.

Variants

There are several alternative definitions of the negative translation. They are all provably equivalent in intuitionistic logic, but may be easier to apply in particular contexts.

One possibility is to change the clauses for disjunction and existential quantifier to

• (φ ∨ θ)^N is ¬¬(φ^N ∨ θ^N)
• (∃x φ)^N is ¬¬∃x φ^N

Then the translation can be succinctly described as: prefix ¬¬ to every atomic formula, disjunction, and existential quantifier.

Another possibility (described by Kuroda) is to construct φ^N from φ by putting ¬¬ before the whole formula and after every universal quantifier. Notice that this reduces to the simple ¬¬φ translation if φ is propositional.

It is also possible to define φ^N by prefixing ¬¬ before every subformula of φ, as done by Kolmogorov. Such a translation is the logical counterpart to the call-by-name continuation-passing style

Continuation-passing style

In functional programming, continuation-passing style is a style of programming in which control is passed explicitly in the form of a continuation. Gerald Jay Sussman and Guy L. Steele, Jr...

 translation of functional programming languages along the lines of the Curry–Howard correspondence between proofs and programs.

Results

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

Heyting arithmetic

In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it....

.

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

Friedman translation

In mathematical logic, the Friedman translation is a certain transformation of intuitionistic formulas. Among other things it can be used to show that the Π02-theorems of various first-order theories of classical mathematics are also theorems of intuitionistic mathematics...

, it is in fact possible to prove that Peano arithmetic is Π⁰₂

Arithmetical hierarchy

In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene-Mostowski hierarchy classifies certain sets based on the complexity of formulas that define them...

-conservative

Conservative extension

In mathematical logic, a logical theory T_2 is a conservative extension of a theory T_1 if the language of T_2 extends the language of T_1; every theorem of T_1 is a theorem of T_2; and any theorem of T_2 which is in the language of T_1 is already a theorem of T_1.More generally, if Γ is a set of...

over Heyting arithmetic.)

The propositional mapping of φ to ¬¬φ does not extend to a sound translation of first-order logic, because is not a theorem of intuitionistic predicate logic. This explains why φ^N has to be defined in a more complicated way in the first-order case.

External links

• "Intuitionistic logic", Stanford Encyclopedia of Philosophy.