Bourbaki and Foundations

[Colin McLarty]

Responding to Harvey's observation that MacLane uses set theoretic
foundations, On Mon, May 16, 2022 at 11:50 PM jodmos.horon <
jodmos.horon at protonmail.ch> wrote:

Well, in fact this observation goes back even to the original paper of
> MacLane
> by MacLane and Eilenberg in 1945. They did not mention set theory
> explicitly in
> that paper, as far as I recall. But, clearly, it's taken to be a model of
> some
> axioms.
>

They name unramified type theory, and  "the Fraenkel-von Neumann-Bernays"
system (today's Godel-Bernays).  It is in their section "1.6 Foundations."
Within type theory they say you could, if you like, limit yourself to
specific types and increase their level as needed, or you could
use "typical ambiguity."  Within Godel-Bernays they note proper classes are
legitimate, or you could, if you prefer to avoid proper classes, always
talk about groups satisfying some cardinal bound which you will adjust as
needed.

That paper is free at
https://www.ams.org/journals/tran/1945-058-00/S0002-9947-1945-0013131-6/S0002-9947-1945-0013131-6.pdf

That was 1945.  In 1962, when Saunders first heard Lawvere's claim that you
could axiomatize set theory directly in the language of category theory,
not presupposing any prior set theory, he declared that impossible.

Then he did something that I recommend to anyone interested in the topic:
he read Lawvere's axioms.  Saunders put those axioms in the PNAS and has
advocated them ever since.

The PNAS article is free at
https://www.pnas.org/doi/pdf/10.1073/pnas.52.6.1506

Colin


> But, on the other hand, so is set theory: it's all about a model of ZFC...
>
> So, whether one chooses set theory or the notion of model as primitive,
> it's a
> chicken and egg question. Of course, you do have an axiomatic setup for set
> theory that allows one to create models and categories as such models
> within
> it. On the other hand, one can take a model of set theory, and carve out
> from
> it all the mappings between sets. And one then gets a model of the
> category of
> sets from the model of ZFC. Or of the category of binary relations (I like
> that
> one better...)
>
> And one can then do model theory on that category of sets carved out from a
> model of ZFC itself seen as a model. Pretty much the same way as we do
> considering models of ZFC.
>
> From where I stand, what I'd like is not set theory, but an axiomatisation
> of
> models. A bunch of ZFC-like axioms that would allow us to axiomatise
> models the
> same way ZFC axiomatised sets.
>
> And it may perhaps be possible to do that in a structuralist feel that
> would
> take lessons from what category theory did teach us in terms of naturality
> and
> universal problems.
>
> > How can this be explained?
> > Well I think that Mac Lane realized that any attempt to remove set
> theory from the picture, and have notions like category as primitive, is
> likely doomed not only in terms of its complexity, but also in terms of its
> Philosophical Coherence.
>
> The only objection I have is that one cannot avoid attempting to justify on
> philosophical grounds that sets exist and that there is a model of it
> somehow
> outside in nature. There needs to be philosophical arguments (not formalist
> ones, we know they failed) to claim that sets exist in some way or another.
>
> The same goes for a notion of a model. In fact, I believe that it's more or
> less an equivalent question.
>
> So this does not preclude considering a category (of sets) itself as a
> model at
> the same ontological level as one would put models of set theory.
>
> > Or you can adopt Mac Lane's approach in [1] and have a page or two with
> precise definitions to start things out sitting on top of set theory.
>
> Well, I'm still not satisfied with the axioms MacLane and Eilenberg gave.
> There
> are hidden subtleties about associativity that arise even in the special
> case
> of groups that people do not seem to care much about, though I do find them
> rather curious to study in themselves.
>
> > For getting the real mathematics going in the sense of mathematical
> culture, it doesn't make any difference which of these two. If
> philosophical coherence is desired or at issue, the second way is best. At
> least until there is a philosophically coherent version without sitting on
> set theory.
>
> What would make set theory more "philosophically coherent" than an
> axiomatisation of constructions in model theory itself ?
>
> > The mutual interpretability of set theory and category theory of various
> kinds is very strong in that they preserve the truth of statements about
> the ring of integers and even the ordered field of real numbers with
> distinguished part Z.
> > So basically, the point is that for reasonably well grounded mathematics
> of a standard kind, the mathematics one has is completely interchangeable -
> and automatically.
>
> What kind of mutual interpretability of set theory and category do you
> have in
> mind, precisely ? I'm not really convinced that any formalisation of
> category
> theory or of a specialisation thereof has managed to adequately interpret
> ZFC.
> I'd be curious to know. I know quite a lot of mimickry can be done, but
> I've
> yet to see a proof of interpretability. But perhaps I haven't looked far
> enough.
>
> Best regards.
>
> Jodmos Horon.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220517/171db543/attachment-0001.html>