FOM: Categorical vs set theoretical foundations

[Vaughan Pratt]

From: Mayberry
>	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).

From: Friedman
>They are wrong.

More precisely, "Had they said that, they would be wrong."  I hope the
following makes clear that I for one didn't say that.

From: Mayberry
>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.

From: Friedman
>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.

No need to ask me, just read the three sentences preceding the so-called
"retort" that Mayberry lifted out of context:

>To avoid misunderstanding it should be said that ZF itself does not start
>with a preconceived notion of collection and go from there.  ZF assumes
>only the language of first order logic with equality and an uninterpreted
>binary relation (membership).  In fact there is no a priori assumption
>at all about the universe being described by the axioms, other than the
>traditional (but unnecessary) assumption that it is nonempty.

I had hoped these would make clear what I was saying, namely that ZF
is not a supplement to a prior theory but rather one that starts from
scratch.  Perhaps I could have made this yet clearer by saying "ZF weaves
*its* entire notion of set..."  But the very next sentence, "How one
*reads* ZF is another matter," should have dispelled any misimpression
that I was claiming ZF defines *our* notion of set, or that my analysis
was "final" as Mayberry puts it.  And thirdly, as Harvey points out,
had I indeed been claiming that ZF is all we will ever know about sets,
I would be implying that we will never know about Choice.  I could not
in conscience claim both knowledge of Replacement and the impossibility
of knowledge of Choice.

From: Mayberry
>I tried to intervene on Friedman's side against the category theorists

You write efficiently.  Apparently Harvey didn't welcome the intervention,
while I don't welcome being labeled a category theorist (you were
focusing mainly on McLarty and me, so I assume the plural was intended
to include me).

In the 1950's some defenders of communists were branded communists
themselves.  That I see technical merit in category theory does not
make me a category theorist, I see comparably much technical merit in
set theory.

Technical merit aside, one of the biggest advantages of set theory
is the same one Windows 95 has: it's what most people use.  For most
computer users today, other platforms are not only incomprehensible
but not worth getting out of the mainstream for.  The first driver a
peripheral manufacturer needs to write therefore is for Windows 95,
one can worry about other platforms later.

The analogue of this for mathematics is that if you have a new theorem
you won't get much of a market for it if you start out by selling it in
categorical language.  That I see merit in Unix and category theory does
not blind me to this common advantage of Windows 95 and set theory.

Ironically one of Windows 95's biggest technical shortcomings is its
weak treatment of networking: in striking contrast to all Unix vendors
Microsoft does even provide telnet or ftp daemons let alone a remote
GUI facility like X-windows, nor even offers any assistance in locating
third party vendors of such capabilities.

By the same token the Z[F][C] axioms do not directly provide for any form
of connectivity, but leave it to higher levels that proceed by way first
of pairing, secondly sets of pairs defining a notion of binary relation,
and thirdly a notion of composition.  (This only seems simple from long
familiarity; by any objective measure this notion of composition is
quite complex.)  In contrast category theory starts out by axiomatizing
composition at ground zero, where the notion is very elementary.

In this sense one could say that category theory is founded on networking,
just like Sun Microsystems whose slogan since 1984 has been "The network
is the computer."

I hasten to add that this networking metaphor for composition is entirely
consistent with the geometric metaphor I described last week, both being
fundamentally path-theoretic.

Name: Vaughan Pratt
Position: Professor of Computer Science
Institution: Stanford University
Research interests: Foundations of computation and mathematics
For more information: http://boole.stanford.edu