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 by translating formulas to formulas which are classically equivalent but intuitionistically inequivalent. Particular instances of double-negation translation 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: Glivenko's theorem implies the more general statement: 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 translationassociates 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 is φN → θN
N is ¬φN
N is ∀x φN
N is ¬∀x ¬φN
This translation has the property that φN is classically equivalent to φ. The fundamental soundness theorem states: Here TN consists of the double-negation translations of the formulas in T. A sentence φ may not imply its negative translation φN in intuitionistic first-order logic. Troelstra and Van Dalen give a description of formulas that 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 is ¬¬∃x φN
Then the translation can be succinctly described as: prefix ¬¬ to every atomic formula, disjunction, and existential quantifier. Another possibility 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-namecontinuation-passing style 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 to study the relationship between classical and intuitionistic theories of the natural numbers. He obtains the following result: 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. 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.
