One can refute in intutionistic logic that they cannot refute the law of excluded middle. The proof is a bit strange:

em-irrefutable : ∀ {A : Set} → ¬ ¬ (A ⊎ ¬ A)
em-irrefutable k = k (inj₂ λ{ x → k (inj₁ x) })

In the discussion of this proof here, the author tells the following story:

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 realised 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.

In an attempt to interpret the proof in a nice way, I tried to write the proof as follows:

em-irrefutable : ∀ {A : Set} → ¬ ¬ (A ⊎ ¬ A)
em-irrefutable devil = devil (inj₂ λ{ billion → devil (inj₁ billion) })

But I do not quiet see how the story and the proof sync up, since what we should ideally be able to show in the proof is that it is possible to extract a billion dollars by tricking the devil. How do I better understand this proof by drawing a correspondence with the allegory?

I apologise if my question is too vague, but I find the proof to be a rather strange one, and would like to see an earthly explanation of it.

  • $\begingroup$ I don't know about a precise answer but here's the way I see the allegory : proving $\neg ( A\lor \neg A)$ is impossible because if you try to prove it to me, then I'll ask you to prove that neither $A$ nor $\neg A$ holds, so you'll come to me all happy with a proof that $A$ does not hold (that's the billion dollars) and I'll say: well here you go, a proof of $\neg A$. Anyway that's how the proof I know of this irrefutability goes, but I don't know if that's what the allegory is about $\endgroup$ – Max Jul 18 '18 at 20:01
  • $\begingroup$ This seems to me to be a typical example of an "intuitive" or "motivational" explanation of a mathematical phenomenon that is much harder to internalise than the essence of the formal proof: the double negation mapping from a Heyting algebra to itself is a homomorphism. $\endgroup$ – Rob Arthan Jul 22 '18 at 22:38

It is useful to rewrite the proof using game semantics: $$\begin{array}{l l c l l} \text{Proponent} & & & \text{Opponent} & \\ \hline 1.\; \text{asserts} & \neg\neg(A \lor \neg A) & & 2.\; \text{attacks 1:} & \neg (A \lor \neg A) \\ 3.\; \text{attacks 2:} & A \lor \neg A & & 4.\; \text{attacks 3:} & ? \\ 5.\; \text{defends 3 from 4:} & \neg A & & 6.\; \text{attacks 5:} & A \\ 7.\; \text{attacks 2:} & A \lor \neg A & & 8.\; \text{attacks 7:} & ? \\ 9.\; \text{defends 7 from 8:} & A & & - & \\ \hline \end{array}$$

Different moments in the story correspond to different moves in the game, with the devil as the proponent and the man as the opponent.

Here $A$ can be interpreted as the proposition "The man has one billion dollars". If the devil grants offer (a), it means that $A$ is true, because the man will have one billion dollars. If the devil grants offer (b), it means that $\neg A$ is true, because the offer has the form $A \to B$ where $B$ is any wish, which is equivalent to $A \to \bot$ by the principle of explosion, which is exactly $\neg A$ by definition.

When the devil makes his offer he's asserting the first proposition, $\neg \neg (A \lor \neg A)$, in move $1$. It sounds as though he's saying $A \lor \neg A$, but he must actually use the double negation in order to win (and it shouldn't be surprising that he's using deception, being the devil as he is).

The next part isn't reflected very well in the game, so we skip directly to move $4$, when the man (i.e., the opponent) asks if he gets offer (a) or (b). The devil responds with (b), which is move $5$ in the game.

Then the man gets his one billion dollars, which he presents to the devil with move $6$. But now the rules of the game allow the proponent to attack move $2$ again, which forces the opponent to counterattack, which in turn allows the proponent to win the game. This corresponds to the devil going back on his word (notice how move $9$ is the opposite of move $5$), choosing offer (a) and winning.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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