Vanilla 1.1.9 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 22 of 22
The question in the title Proofs of the uncountability of the reals has two votes to close. I don't think it's an inappropriate question for MO. Of course, I'm by no means an expert, but since the only proof I know is the one based on the diagonal argument, I'm certainly interested in the possible answers, if only for pedagogical reasons.
I've left a virtual vote against closing, just in case, with a link to this thread in hopes people will pop over here first before casting any more votes to close.
I am alarmed by some users' urge to vote to close without at least leaving a note.
The positive answers I get from MO answers truly drive me become part of the community of such mathematicians...Though down-voting is perfect for moderating MO, doing it without a positive excuse will have no effect other than pushing away the challenged/confused. I did never down-vote without stating a reason, except when I did once just to get the Critic badge in my early days of MO participation.
They do seem quick, yes. My first impulse was that it looks like a duplicate, but all I can come up with is Earliest diagonal proof of the uncountability of the reals, which is not quite the same. The question might have been better if it were stated in the context of this older question, though. It's not like it is all that hard to find.
At the end of the day, thank you all. I have had a lot to wonder about before sleep tonight.
I'm almost tempted to cast the final vote to close just to find out who it was that cast the other four votes without coming here and saying why! Or leaving a comment on the original question.
If you expose me, Andrew, I'll make you regret it!!!
I was almost tempted to unilaterally reopen the question! The lack of alternatives to the diagonalization method is a key problem in logic and theoretical computer science. I think this question pokes at the heart of the matter. This may be the first question which is too deep for MO...
@Kevin: in the specific example you give of P1 and P2, you actually hit one of the cases where it is possible to give a rigorous argument that that the two proofs are the same. In structural proof theory, there's a criterion called normalization or cut-elimination, and this basically says that a system is well-behaved if it is possible in principle to expand away all lemmas from a proof. (As an aside, this is a condition stronger than consistency -- all systems with cut-elimination are consistent, but not vice versa.)
This induces an equivalence relation on proofs, in which two proofs are equated just in case they have the same cut-free form. In the case of a spurious use of a lemma, a cut-elimination algorithm will simply delete it from the normal proof. So P1 and P2 will end up with the same normal form, and this normal form will not have a subtree corresponding to a diagonal argument unless P1 relied upon one to begin with.
However, while equivalence of cut-free proofs seem to capture an awful lot of proof equivalences, it's still not a sharp enough notion to let us talk about the similarity of proofs. (Eg, various fixed point theorems all tend to look similar, but obviously they don't have equal proofs.) Moreover, even natural deduction isn't terribly natural when compared to proper mathematical discourse, so I rather suspect we still lack some fundamental ideas about the invariants and/or symmetries of proofs.
@Kevin: you might be interested in some existing discussion on this subject, e.g. this MO question and this blog post by Tim Gowers.
Whoops! That's what I get, I guess.