Intuitionistic Excluded Middle, Glivenko’s theorem and the Gödel-Gentzen translation

In intuitionistic logic, the law of the excluded middle doesn’t hold even though it is valid in classical logic. That being said, its double negation does hold and we can prove that the negation of the excluded middle isn’t true. In other words, we have a term \[\mathtt{not}\text{-}\mathtt{not}\text{-}\mathtt{lem} : \lnot \lnot \prod_{A : \mathcal{U}} A + \lnot A\]

With a bit of thought, we can actually construct such a term in Haskell

import Data.Void

type Not a = a -> Void
notNotLem :: Not (Not (Either a (Not a))
notNotLem = \f -> f (Right $ \x -> f $ Left x)

And if you think about it for a bit, you get the following equivalent definition.

notNotLem :: Not (Not (Either a (Not a))
notNotLem = (. Right) <*> (. Left)

Where <*> is the S combinator from the SKI combinator calculus and the relevant term in type theory is \(\lambda f. f (\mathtt{inr\ } \lambda x. f (\mathtt{inl\ } x))\).

There are more of these results: for example double negation elimination also holds in classical logic but fails to hold in intuitionistic logic yet the double negation of double negation elimination is a valid sentence in intuitionistic logic. You can also define these results in Haskell.

negationIntroduction :: a -> Not (Not a)
negationIntroduction = \x -> \f -> f x
negationIntroduction = flip ($)

negationElimination :: Not (Not (Not (Not a) -> a))
negationElimination = \f -> f negationIntroduction
negationElimination = ($ negationIntroduction)
negationElimination = ($ flip ($))

In classical logic we have double negation elimination as a theorem, so if the double negation of a statement holds in intuitionistic logic then we can prove the statement in classical logic by applying double negation elimination.

But does the converse hold? That is, if we can prove a theorem in classical logic, can we prove its double negation in intuitionistic logic? Or, if \(A\) holds in classical logic, can we prove \(\lnot \lnot A\) in intuitionistic logic?

The answer to this question is yes and it is precisely the content of Glivenko’s theorem. We can construct such proofs via the Gödel–Gentzen translation.

While we can prove this theorem and construct the translation by induction on the terms of both logics, there is a more elegant way to reason about this.

Intuitionistic logic is the internal logic of Heyting categories and classical logic is the internal logic of Boolean categories.

Using this, we can construct functors between boolean algebras and heyting algebras which correspond to syntactic translations between the two logics. The double negation translation becomes a functor that preserves meets and exponentials and the proof of Glivenko’s theorem is the existence of this functor.