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.
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:
- If φ is a propositional formula, then φ is a classical tautology if and only if ¬¬φ is an intuitionistic tautology.
Glivenko's theorem implies the more general statement:
- If T is a set of propositional formulas, T* a set consisting of the doubly negated formulas of T, and φ a propositional formula, then T ⊢ φ in classical logic if and only if T* ⊢ ¬¬φ in intuitionistic logic.
In particular, a set of propositional formulas is intuitionistically consistent if and only if it is classically satisfiable.
- If φ is atomic, then φ is ¬¬φ
- (φ ∧ θ) is φ ∧ θ
- (φ ∨ θ) is ¬(¬φ ∧ ¬θ)
- (φ → θ) is φ → θ
- (¬φ) is ¬φ
- (∀x φ) is ∀x φ
- (∃x φ) is ¬∀x ¬φ
This translation has the property that φ is classically equivalent to φ.
The fundamental soundness theorem (Avigad and Feferman 1998, p. 342; Buss 1998 p. 66) states:
- If T is a set of axioms and φ is a formula, then T proves φ using classical logic if and only if T proves φ using intuitionistic logic.
Here T consists of the double-negation translations of the formulas in T.
A sentence φ may not imply its negative translation φ in intuitionistic first-order logic.
Troelstra and Van Dalen (1988, Ch.
3) give a description (due to Leivant) of formulas that do imply their Gödel–Gentzen translation.
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.
- (φ ∨ θ) is ¬¬(φ ∨ θ)
- (∃x φ) is ¬¬∃x φ
Then the translation can be succinctly described as: prefix ¬¬ to every atomic formula, disjunction, and existential quantifier.
Notice that this reduces to the simple ¬¬φ translation if φ is propositional.
It is also possible to define φ 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 translation of functional programming languages along the lines of the Curry–Howard correspondence between proofs and programs.
The double-negation translation was used by Gödel (1933) to study the relationship between classical and intuitionistic theories of the natural numbers ("arithmetic").
He obtains the following result:
- If a formula φ is provable from the axioms of Peano arithmetic then φ is provable from the axioms of intuitionistic Heyting arithmetic.
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 ∀x ¬¬φ(x) → ¬¬∀x φ(x) is not a theorem of intuitionistic predicate logic.
This explains why φ has to be defined in a more complicated way in the first-order case.
Credits to the contents of this page go to the authors of the corresponding Wikipedia page: en.wikipedia.org/wiki/Double-negation translation.