Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

In Wikipedia's Double-negation translation article, I found that any formula in classical logic has its double negation as its intuitionist equivalent:

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-name continuation-passing style translation of functional programming languages along the lines of the Curry–Howard correspondence between proofs and programs.

Could anyone explain how prefixing ¬¬ before every sub formula of a proposition is the logical counter part to call-by-name continuation-passing style? If possible, could you use Python, since I'm not familiar with Scheme and Haskell.

I've done some research into CPS, but I'm not seeing the relationship, apart from the fact that a function $P \to \bot$ doesn't have a return value.

share|cite|improve this question
Some slides of mine tackle this question. They start with a general introduction to the difference between classical and constructive mathematics and end with specific Haskell code. – Ingo Blechschmidt Jan 12 at 20:33

Turns out that my question is answered in great detail here:

share|cite|improve this answer
Can you add some commentary? I don't see any mention in that article about the correspondence between double negation and call-by-name CPS. – Joshua Taylor Aug 25 '14 at 19:51

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.