[Haskell-cafe] Relationship between ((a -> Void) -> Void) and (forall r. (a -> r) -> r)

[Ingo Blechschmidt]

On Fri 15 May 2020 05:19:01 AM GMT, Ruben Astudillo wrote:
> On 13-05-20 09:15, Olaf Klinke wrote:
> > Excersise: Prove that intuitionistically, it is absurd to deny the law
> > of excluded middle:
> >
> > Not (Not (Either a (Not a)))

This fact is indeed truly wondrous. I encourage everyone to ponder it
thoroughly. It has been worked into a classical logic fairy tale:

    http://blog.ezyang.com/2013/04/a-classical-logic-fairy-tale/
    (sorry for http)

And more in this little Oleg jewel:

    https://web.archive.org/web/20180901035449/http://okmij.org/ftp/Computation/lem.html

> given you seem knowledgeable I want to corroborate with you. I've seen
> claimed on the web that the CPS transform *is* the double negation [1]
> [2]. I don't think that true, it is almost true in my view. I'll
[...]

Yes, you are right, and your analysis of the situation is correct.

Using (_ → R) → R for some fixed statement R instead of ¬¬_ = ((_ → ⊥) → ⊥)
is what's called "the R-Friedman translation applied to the double
negation translation". It is what powers "Friedman's trick", a marvelous
technique for extracting constructive content from classical proofs [1].

People say that you cannot escape the continuation monad. But sometimes,
you can.

Dickson's lemma nicely illustrates this insight. It states that for any
infinite list xs ∷ [Nat], there is an index i such that xs !! i ≤ xs !! (i + 1).
This lemma has a trivial classical proof (just pick the minimum of the
list xs), but this classical proof is not effective: There is no
algorithm for computing the minimum of an infinite list. Using the
continuation monad, we can extract the constructive content of this
classical proof. See here:

    https://github.com/iblech/talk-constructive-mathematics/blob/master/law-of-exluded-middle.hs

Cheers,
Ingo

[1] Say you want to constructively prove A → B. You already have a classical
proof of A → B, and you managed [2] to turn this proof into a
constructive proof of

    ((A → R) → R) → ((B → R) → R),

for any as of yet undecided statement R. Now specialize to R ≔ B. Hence
we have a constructive proof of

    ((A → B) → B) → ((B → B) → B).

Combining this with the constructive tautologies A → ((A → B) → B) and
((B → B) → B) ↔ B, we obtain a constructive proof of A → B.

[2] A metatheorem states that if some statement A is classically
provable then its double negation translation and furthermore the
R-Friedman translation of the double negation translation are
constructively provable. (Incidentally, this metatheorem has a
constructive proof.)

But "translation" here means more than just replacing A by ¬¬A
(respectively ((A → R) → R)). It means introducing a double negation in
front of every equality, disjunction and existential quantification. For
instance, the ¬¬-translation of

    ∀x. ∃y. f(x,y) = g(x,y)

is

    ∀x. ¬¬∃y. ¬¬(f(x,y) = g(x,y)).

In some circumstances, the double negation translation of a complex
statement A is constructively equivalent to ¬¬A, that is, in some
circumstances the many nested double negations can be pulled to the
front. This is for instance the case for so-called "geometric formulas",
statements in which the logical symbols "→" and "∀" don't occur.