I am sure several other readers of this list will have the same reply to this specific point of Paul's message:
I'm sorry, Martin, did I post to FOM instead of "categories" by mistake?
There is a very nice paper by Lawvere that shows that the essence of Cantor's theorem is fundamental and beautiful:
Yes, and this illustrates the distinction that I am trying to make between Lemmas that do the work and Theorems that take the credit. Lawvere's argument is a Lemma about fixed points that has many uses elsewhere. I might even stretch to crediting Cantor with a good idea, since it reappeared as Turing's insolubility of the halting problem and Goedel's incompleteness theorem. As a Theorem, on the other hand, Cantor's result was the basis of the theory of cardinality, which was more or less immediately recognised as being completely useless for ordinary mathematical purposes such as distinguishing between R^2 and R^3. It is dogma. As I said, we use "Theorems" to summarise how a piece of work fits into the currently prevailing mathematical dogma. When that dogma changes, the Theorems go out of the window, but the Lemmas survive, being reorganised in a new way according to the new dogma. To give an example in category theory, it is a Theorem that a certain structure is the "classifying category" or "classifying topos" for some theory, because this terminology comes from a particular world view. However, the same underlying calculations have been organised in different ways under different names (such as "clone" and "Lawvere theory") in the past, and will be reorganised in other ways in the future. The thing that makes Mathematics interesting is that there is something there that is essentially independent of the world view according to which it is currently organised. In approaching a particular topic, you can choose the Definitions one way and then have to prove a particular Theorem, or go round the circle the other way, rewriting the Theorem as the Definition and proving a different Theorem. But when you look carefully at the two versions, you realise that the same Lemma is there either way. I used to illustrate this with Galois Theory, but I regret that I can no longer remember that beautiful subject sufficiently clearly to do so now. Instead, I gave a more prosaic example in Section 1,2 of my book, called the Lineland Army. (As a Theorem, it is the free monad on a monoid.) You can approach it as a pure mathematician would, using equivalence classes, in which case the Theorem says that its binary operation is associative. Or you can approach it as a theoretical computer scientist would, and prove a normalisation Theorem. But either way there is the same Lemma. In a particular topic, therefore, rather than in a whole discipline such as category theory, there may well be a Fundamental Lemma -- the one thing that you have to prove, whichever way you go round the circle. But I think we should wrap up this thread now.
There is also a post by Andrej Bauer in his Mathematics and Computation blog: http://math.andrej.com/2007/04/08/on-a-proof-of-cantors-theorem/
Funny you should mention this, because I was going to cite it for a completely different reason. Andrej originally posted this to FOM, but it was censored, and he received a "referee's report" from the "editorial board". Those who have been anywhere near FOM will know of its notoriety. For example, two categorical logicians who attempted to engage with set theorists there c1998 were on the receiving end of a lot of personal abuse from one specific person. I have heard similar stories from about four other sources in completely unrelated disciplines. In particular, some of us recently attempted to discuss some points of constructive real analysis there. I have to be careful in posing my question, otherwise I will get a mailbox full of examples of dogma, abuse and censorship. On "categories" we ask questions, advertise our work and discuss issues of research and professional matters. Set theorists appear to do the same on FOM, but the list is called "Foundations of Mathematics" and not "Set Theory". In both cases I expect that there are isolated graduate students for whom these lists are their one contact with the outside world and source of information about mathematical research. FOM ought to provide them with a diversity of points of view, as "categories" does. Has anyone EVER managed to discuss constructive mathematics, type theory, categorical logic, or any other "heretical" topic, on FOM, in a professional way, without being shouted down or censored? Please reply privately, and don't copy long postings or "referee's reports" to me. Just tell me briefly the month in which the exchange took place and who participated in it, then I can look it up myself in the FOM archive. Paul Taylor [For admin and other information see: http://www.mta.ca/~cat-dist/ ]