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.
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:
“Cantor’s argument actually shows that no function from the naturals to the reals is surjective”
An even nicer way to say this is that it shows that for every function there exists an element in the complement of the range (in the strong constructive sense, as you point out). When discussing Cantor’s theorem I like to phrase it in this positive sense, that every function N –> ( N –> N) (say) “misses” at least one element in the codomain, and even going so far to set things up to define relative size of sets so that this is exactly the definition of N being smaller than N –> N, rather than ‘there exists an injection but no bijection’.
Yes! I had the same thought on rereading this 4 years on.