The Devil of the Excluded Middle


L E J Brouwer (1881-1966) who propounded the doctrine mathematical intuitionism.



In the spirit of the great sufiana parables, here is one my favorite stories from the heart of computer science and logic. This is the story of the “devil of the excluded middle” as told by Phil Wadler [1]. Underlying this story is the deep reason for one of the great disagreements about the nature of mathematical proof leading to classical and intuitionistic mathematics.

Once upon a time, the devil approached a man and made an offer: “Either (a) I will give you one billion dollars, or (b) I will grant you any wish if you pay me one billion dollars. Of course, I get to choose whether I offer (a) or (b).”

The man was wary. Did he need to sign over his soul? No, said the devil, all the man need do is accept the offer.

The man pondered. If he was offered (b) it was unlikely that he would ever be able to buy the wish, but what was the harm in having the opportunity available?

“I accept,” said the man at last. “Do I get (a) or (b)?”

The devil paused. “I choose (b).”

The man was disappointed but not surprised. That was that, he thought. But the offer gnawed at him. Imagine what he could do with his wish! Many years passed, and the man began to accumulate money. To get the money he sometimes did bad things, and dimly he realized that this must be what the devil had in mind. Eventually he had his billion dollars, and the devil appeared again.

“Here is a billion dollars,” said the man, handing over a valise containing the money. “Grant me my wish!”

The devil took possession of the valise. Then he said,“Oh, did I say (b) before? I’m so sorry. I meant (a). It is my great pleasure to give you one billion dollars.”

And the devil handed back to the man the same valise that the man had just handed to him.

Wadler also mentions a version of this story told by Peter Selinger, which I have not been able to track down.

[1] [doi] P. Wadler, “Call-by-value is dual to call-by-name,” SIGPLAN Not., vol. 38, iss. 9, pp. 189-201, 2003.
 author = {Wadler, Philip},
 title = {Call-by-value is dual to call-by-name},
 journal = {SIGPLAN Not.},
 issue_date = {September 2003},
 volume = {38},
 number = {9},
 month = aug,
 year = {2003},
 issn = {0362-1340},
 pages = {189--201},
 numpages = {13},
 url = {},
 doi = {10.1145/944746.944723},
 acmid = {944723},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Curry-Howard correspondence, De Morgan dual, lambda calculus, lambda mu calculus, logic, natural deduction, sequent calculus},

Comments are closed.