FOM: Categorical vs set theoretical foundations

[Harvey Friedman]

Reply to John Mayberry 4:13PM 1/26/98.


>	I thought I was entering a scholarly discussion/argument over
>the possibility of category-theoretic foundations, not a barroom brawl.

It's just my way of saying that in my humble opinion, I think that what you
are saying makes no sense, is inexplicable, and indefensible. That's just
my opinion. I have been wrong many times in a variety of circumstances. And
if you read my postings, you see that I often write this way when that is
my opinion.

>But even in a brawl you ought to find out what side a man is on before
>you try to punch him in the nose.

I saw by the last statement you made that you perhaps perceived that you
were on my side. But there is the old saying: with friends like this, who
needs enemies? (Said with a smile).

>I tried to intervene on Friedman's
>side against the category theorists, and I found him throwing punches
>at me. Can't he see that I am on his side?

Not really.

>	Let me try to put my argument in a different way. McLarty and
>Pratt (and MacLane, for that matter) seem to think that the claim that
>set theory provides the foundations for mathematics ultimately boils
>down to the claim that mathematics can be "translated into" or
>"interpreted in" the formal first order axiomatic theory ZF (or ZFC).

They are wrong. Otherwise I would agree that category/topos theory also
provides a foundaiton for mathematics.

>Moreover, he [McLarty] has argued vigorously, and not by any means without
>success, that this is the case.

If you mean that McLary has argued for the previous statement, then he has
done so without success. If you mean that McLarty has argued that
mathematics can be "translated into" some first order thoery of topoi, then
I agree.

>Friedman objects that these other
>theories are not properly "motivated" - that they are not backed up
>with a clear notion of what their primitive symbols stand for, or of
>what their intended universes of discourse consist in.

Correct, well known, and fatal for categorical foundations. However this
fatality is actually an **advantage** for the normal purposes of category
theory/topoi in core mathematics.

>But Pratt
>retorts (in the passage I quoted) that, in the final analysis, whatever
>may be our "motivation" or intention, "ZF weaves the entire notion of
>set from the whole cloth of first order logic". He is saying, I think,
>that once we have converted our "motivating" ideas into a formal
>axiomatic theory, formal logic takes over and tells us all we will ever
>know about our primitive notions. As is sometimes said, those notions
>are "defined" by those axioms.

I don't believe that's what Pratt meant at all. Let's ask him. Pratt??? By
the way, it is false. E.g., the axiom of choice is missing in ZF.

>	How can this powerful and familiar general argument be
>answered? Clearly it won't do simply to say that *my* axioms are more
>elegant, or more economical, or better motivated, or easier to teach to
>undergraduates, or more nearly in accord with engineering practice, or
>whatever. Because these are clearly all matters for judgment - often
>something akin to aesthetic judgement - and different people can arrive
>at different judgements without any of them lapsing into obvious
>irrationality.

I disagree with this. They are matters for judgment (not aesthetic
judgment), and the judgment is already in by how we in fact teach and
explain in Mathematics Departments.

>	I say that the problem is *not* one of judging whose formal
>first order axioms are best "motivated".

Why not?

>The point is that *none* of
>these formal first order theories, qua formal first order theory, can,
>as a matter of *logic* (taking "logic" in its broadest sense), qualify
>as a foundation for mathematics.

As I said earlier, ZFC together with the usual standard motivation
constitutes a foundation for mathematics. The fact that ZFC is not complete
in various senses does not contradict this.

>*That* was what I was trying to say in
>my earlier posting.

I know. I think you are wrong.

>But it is the natural, pre-formalized set theory that
>provides the real foundation for mathematics, not its formalized
>simulacrum.

Not if it couldn't be represented so well by a simple and elegant and
powerful system such as ZFC.

>	Finally, let me address a few words to Harvey Friedman. I cannot
>understand why a man with your superior gifts and reputation should find
>it necessary to indulge in the kind of fierce polemics that you
>directed at me.

Well, perhaps my reputation is going down. I regarded it as ordinary
conversation between two professionals. By the way, Simpson forced me to
tone down my response to you very considerably. I gave in. He's a
convincing moderator, and apparently actually reads these postings!

>Had I been wrong, and had your criticism been of
>substance, I should still not have deserved the sort public drubbing
>that you attempted to administer.

Too sensitive. After all, I am a well known character.

>In fact, however, none of your
>criticism hit its mark, because you have systematically, and, it seems
>to me, willfully, misunderstood or misinterpreted what I was saying.

I'm trying to be responsive. Maybe I misunderstand your point. But I do the
best I can.

>For example, you have clearly mistaken my remarks about the
>completeness of systems of logical proof for first order logic as being
>about the completeness of first order axiomatic theories. Of course you
>know that these are different senses of "completeness". How could Godel
>have thought that the completeness of first order logic was "an open
>ended process", as you say, when he himself established it. He was
>obviously thinking of "completeness" in the other sense.

Godel regarded the axiomatization of set theory as an open ended process.
E.g., to him ZFC is merely a tiny fragment of the full story. That didn't
cause him to declare that ZFC was not a foundation for mathematics. Now,
wasn't this posting more mild?