Lemmas and Theorems

Lemmas and Theorems

[Paul Taylor]

> 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/ ]