Sorry for the delay… I’ve realized that I’ll need to completely rework my next post on forcing, and I don’t have the time right now. Hopefully soon(tm) I’ll be able to finish up and do something a little more fun. In the mean time, some thoughts on the famous diagonal argument.

When explaining the diagonal argument, and when trying to understand why so many students have such a hard time accepting it, intuitionism seems to come up a lot; the statement is usually something like “Many students implicitly use intuitionistic logic, which is why they have such a hard time accepting the proof” or “the diagonal argument uses proof by contradiction so requires classical logic.”

This claim always baffles me because *the diagonal argument is inutionistically valid!*

The misconception seems to arise from the misleading statement “Intuitionistic logic does not allow proofs by contradiction.” This statement is true, but many math students (and many mathematicians, it seems) have a vague notion of what proof by contradiction is.

Consider the following three “arguments” by contradiction:

**1** Claim: foo.

Proof: Assume not foo. [Argument] Contradiction. Therefore foo.

**2** Claim: not foo.

Proof: Assume the claim is false. That is, assume foo. [Argument] Contradiction. Therefore not foo.

**3** Claim: not foo.

Proof: Assume foo. [Argument] Contradiction. Therefore not foo.

**3** is intuitionistically valid, **2** is an incorrect argument (intuitionistically), but leads to a correct result, while **1** is not intuitionistically valid. Where is the difference?

In **1**, we assume *not foo*, and then derive a contradiction. We haven’t yet shown that *foo is true*, instead, what we’ve shown is that *not foo is false*. We then jump to *foo is true* using your favorite classical principle (e.g., law of the excluded middle, or double-negation elimination)

In **2 **we make this jump directly. And then we derive a contradiction from the “assumption” not (not foo); however, we’ve actually derived it from foo directly: instead of assuming not (not foo), *we should just assume foo directly*, and show that this leads to a contradiction (and so must be false). This would give us **3**, where we never jump from *not foo is false* to *foo is true*.

*false*. These are (to the intuitionist) different propositions.

**1**is an actual proof by contradiction,

**2**

*looks like*a proof by contradiction, and

**3**looks like

**2.**

To the classical mathematician, **2** and **3** look the same, and since classical mathematicians don’t usually distinguish between negative and positive propositions, **2** looks like **1**, so the three forms of argument all look the same to the classical mathematician. And so the statement “intuitionistic logic doesn’t allow proof by contradiction” ends up looking to the classical mathematician like a heavy restriction indeed.

In fact, the *only* way to prove a negative statement in intuitionistic logic is to show a contradiction: the definition of *not foo* in intuitionistic logic is “foo implies a contradiction.” So **3** *must* be valid.

Now, Cantor’s Diagonal is usually presented as follows:

**Claim:** There is no bijection from the set of naturals to the set of reals.

**Proof:** *Assume the claim is false. That is assume there is such a bijection* *f*. [Costruct the diagonal] contradiction. Therefore the claim is true.

Observe that the form of this argument is that of **2**. Instead we shouldn’t assume the claim is false, but rather *assume directly such a bijection exists*, and end up with an argument with the same form as **3**. We can actually do one better, but this has (almost) nothing to do with intuitionism:

*surjective.*And it does so in a remarkably constructive way: if you give me any function

*f*, I can give you a real number not in the range; that is, a term

*witnessing*the fact that

*f*is not surjective. The fact that we can construct an explicit term is usually a good indication that a proof is intuitionistically valid.