The double negation translation is a method for converting propositions valid in classical logic into propositions valid in intuitionistic logic. It was discovered independently by a number of mathematicians including Kurt Gödel, Gerhard Gentzen, and Andrey Kolmogorov, and is also called the Gödel–Gentzen negative translation.
The traditional descriptions are highly syntactic, but can be motivated by recalling some conceptual relationships between Boolean algebras (which are algebras for classical propositional logic) and Heyting algebras (which are algebras for intuitionistic propositional logic).
is given objectwise by taking a Heyting algebra to the poset of regular elements , i.e., those satisfying . It was shown that is a Boolean algebra, and is a Heyting algebra homomorphism which is universal among Heyting algebra maps into Boolean algebras.
In particular, if is the free Heyting algebra on a set of variables , it follows by composing left adjoints
that is the free Boolean algebra on .
Furthermore, it was shown in Heyting algebra that for Heyting algebras ,
Consequently, the inclusion of regular elements also preserves meets and implications, strictly. This gives the following result.
If is a tautology in classical propositional logic, then is a tautology in intuitionistic propositional logic, and conversely.
Here and are term expressions in variables over the signature . To say is a classical tautology means that holds when interpreted in . But since , this is equivalent to saying that
when interpreted in , which is to say that is an intuitionistic tautology.
Continuing this thought: the join in is computed as
since preserves joins (it is a left adjoint). Putting all this together, because preserves Heyting algebra structure, we arrive the following syntactic translation.
The double-negation translation on term expressions in the theory of Heyting algebras is defined by induction as follows.
for variables .
(since preserves )
(since preserves )
(since preserves the meet operation)
(since preserves the implication operation)
Thus, by Glivenko’s theorem, is a classical tautology if and only if is an intuitionistic tautology. This result may be extended to theories as well: suppose is an intuitionistic theory or Heyting algebra, given by a presentation as a coequalizer in :
Then, since the functor is a left adjoint, it takes this coequalizer to a coequalizer
so that an term expression is a theorem in the classical theory if and only if is a theorem in the intuitionistic theory .