tea.mathoverflow.net - Discussion Feed (Proofs of the uncountability of the reals)

Todd Trimble comments on "Proofs of the uncountability of the reals" (11014)

Todd Trimble — Tue, 23 Nov 2010 13:22:32 -0800

Kevin, you can get an idea of what I'm talking about from reading Manfred Szabo's Algebra of Proofs. (I have to sound an obligatory warning that some of his coherence-theoretic claims do not hold, but these are highly technical matters and not likely to impede one's understanding of the basics of categorical semantics of sequent calculi.) I think I can highly recommend Girard's original Linear Logic and Geometry of Interactions articles, which spawned a vast literature on another type of substructural logic with significant categorical models (*-autonomous categories).

Kevin Buzzard comments on "Proofs of the uncountability of the reals" (11013)

Kevin Buzzard — Tue, 23 Nov 2010 12:52:45 -0800

I think I'm at the point now where "superficial" thoughts about this problem will get me nowhere and I have to get my hands dirty and e.g. try and understand some of the details of what Todd is talking about.

Qiaochu Yuan comments on "Proofs of the uncountability of the reals" (11012)

Qiaochu Yuan — Tue, 23 Nov 2010 12:23:12 -0800

Whoops! That's what I get, I guess.

Kevin Buzzard comments on "Proofs of the uncountability of the reals" (11010)

Kevin Buzzard — Tue, 23 Nov 2010 12:03:59 -0800

@Qiaochu: you might be interested in reading my answer to the MO question you pointed me to ;-) In fact, my thoughts about trying to formalise things like this started with some conversation with Gowers in London when he gave the colloquium here.

Todd Trimble comments on "Proofs of the uncountability of the reals" (11006)

Todd Trimble — Tue, 23 Nov 2010 09:39:24 -0800

@Kevin: somewhat related to what Neel was saying, there is a large amount of work in categorical logic whereby it is meaningful to interpret formal deductions as morphisms in certain structured categories (at least under certain restrictions on the logic, e.g., intuitionistic propositional logic), so that it becomes meaningful to say that two proofs of the same underlying proposition $A \vdash B$ are fundamentally different: yield distinct morphisms under the appropriate semantics of proofs. So even though proof theory is not a hugely developed field IMO, I do not yet share your pessimism.

Qiaochu Yuan comments on "Proofs of the uncountability of the reals" (11002)

Qiaochu Yuan — Tue, 23 Nov 2010 09:02:27 -0800

@Kevin: you might be interested in some existing discussion on this subject, e.g. this MO question and this blog post by Tim Gowers.

neelk comments on "Proofs of the uncountability of the reals" (11001)

neelk — Tue, 23 Nov 2010 08:45:09 -0800

@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 Buzzard comments on "Proofs of the uncountability of the reals" (11000)

Kevin Buzzard — Tue, 23 Nov 2010 08:05:42 -0800

@Todd: let me stick my neck out and say that, contrary to Francois' opinion that "mathematics is not ready to rigorously define what it means for an argument to "contain a diagonal argument"", I think I'm of the opinion that "mathematics will never be able to rigorously define what it means for an argument to contain a diagonal argument". That's, I think, the heart of my desire to vote to close.

I thought about this briefly recently, in fact. I was trying to figure out what it means for two proofs to be "the same", or, more precisely, a good equivalence relation on proofs of a statement for which proofs which were "the same" should be equivalent. I didn't get close to a good answer to this. However I did convince myself that "inserting a spurious extra argument" should perhaps count as not changing a proof. So, for example, here is proof P1 of x: it goes "blah blah blah". Now here is proof P2: it goes "blah blah [insert proof of something else here] blah". I concluded that any reasonable notion of "the same proof" should have P2 and P1 down as being "the same proof".

But now there's the precise problem: what if the random thing I inserted was a "diagonal argument" but what if P1 really "had no diagonal argument"?

I cannot resolve these issues: In fact I am almost saying that I have some sketch of a proof that one cannot formulate rigorously what it means for a proof to be not a diagonal argument.

Todd Trimble comments on "Proofs of the uncountability of the reals" (10993)

Todd Trimble — Tue, 23 Nov 2010 03:41:14 -0800

@Kevin: In a way, we may be converging on agreement. I certainly see your point. Francois wrote, "this may be the first problem that is too deep for MO," and your position is not inconsistent with that (if it's too deep to make perfectly precise, then it doesn't belong).

What I was saying above (in response to Robin and Bill, mostly) is that it's not an elementary question at all. It is an interesting question, and maybe not far from cutting-edge research. But, I'm not ready to argue for it with the rigorous formulation you ask for -- even if a la Potter Stewart, I know a diagonal argument when I see it. In view of that, I won't object if people want to close it again. (Not that I was one of the re-openers.)

I am glad you at least enunciated a *proper* reason for closing. I would enjoy it if one of our esteemed logicians/set theorists would be inspired to write up a precise question which touches upon these issues.

Kevin Buzzard comments on "Proofs of the uncountability of the reals" (10987)

Kevin Buzzard — Tue, 23 Nov 2010 01:44:47 -0800

@Todd: My objection to the question is that it cannot be formulated precisely. If you can give me a rigorous notion of "a diagonal argument in disguise" then that's fine. If you can't, then we will continue to get more answers of the form "X: here is a diagonal-free argument" "@X: no, that's a diagonal argument in disguise". This is already happening! Whatever is the point of that?

Andres Caicedo comments on "Proofs of the uncountability of the reals" (10978)

Andres Caicedo — Mon, 22 Nov 2010 16:06:45 -0800

I voted to re-open. The version that Todd just mentioned seems subtle and interesting to me. I sketched a proof, and would appreciate feedback in case I missed a hidden diagonalization somewhere.

Todd Trimble comments on "Proofs of the uncountability of the reals" (10975)

Todd Trimble — Mon, 22 Nov 2010 14:03:11 -0800

The question seems to be: can anyone give a proof of uncountability of $\mathbb{R}$ that is not a diagonal argument in disguise? How is that an elementary question? It seems like a perfectly reasonable question to me.

Looking at the replies, no one came up with such a proof, but at the same time no one knows how to show there is no such proof (cf. Timothy Chow's answer), and yet no one quite asserted a belief there is no such proof (AFAIK). If it were that elementary, it seems a more decisive answer would be available.

Bill Johnson comments on "Proofs of the uncountability of the reals" (10974)

Bill Johnson — Mon, 22 Nov 2010 13:59:46 -0800

Prove that the reals are connected.

Prove that every countable dense subset $X$ of the reals must be order isomorphic to the rationals.

Prove that the rationals are not connected.

François G. Dorais comments on "Proofs of the uncountability of the reals" (10973)

François G. Dorais — Mon, 22 Nov 2010 13:52:01 -0800

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

Bill Johnson comments on "Proofs of the uncountability of the reals" (10972)

Bill Johnson — Mon, 22 Nov 2010 13:50:35 -0800

It is IMO an elementary question that did not belong on MO. I am amazed that it got so many responses.

The number of inappropriate questions has gotten to be distracting; again, IMO.

Robin Chapman comments on "Proofs of the uncountability of the reals" (10970)

Robin Chapman — Mon, 22 Nov 2010 13:06:49 -0800

A fishing expedition about a topic far from present-day research:
let's close at once!

Harry Gindi comments on "Proofs of the uncountability of the reals" (10968)

Harry Gindi — Mon, 22 Nov 2010 12:06:57 -0800

If you expose me, Andrew, I'll make you regret it!!!

Andrew Stacey comments on "Proofs of the uncountability of the reals" (10967)

Andrew Stacey — Mon, 22 Nov 2010 11:50:28 -0800

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.

E.S comments on "Proofs of the uncountability of the reals" (10966)

E.S — Mon, 22 Nov 2010 11:19:16 -0800

At the end of the day, thank you all. I have had a lot to wonder about before sleep tonight.

Harald Hanche-Olsen comments on "Proofs of the uncountability of the reals" (10963)

Harald Hanche-Olsen — Mon, 22 Nov 2010 10:08:17 -0800

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.

E.S comments on "Proofs of the uncountability of the reals" (10962)

E.S — Mon, 22 Nov 2010 10:05:15 -0800

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.

José Figueroa comments on "Proofs of the uncountability of the reals" (10960)

José Figueroa — Mon, 22 Nov 2010 09:45:16 -0800

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.