Bourbaki and Foundations

[jodmos.horon]

> 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.

To which, on Tuesday, May 17th, 2022 at 15:33, Colin McLarty <colin.mclarty at case.edu> replied:
> 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.

Thank you. I just checked it. For the record, the axiomatic definitions of
categories may be found on pages 237 and 238, section I.1 of that document.

General Theory of Natural Equivalences, Samuel Eilenberg and Saunders MacLane,
Transactions of the American Mathematical Society, Vol. 58, No. 2 (Sep., 1945),
pp. 231-294.

I just reread the section I.6 concerning foundations. It acknowledges the
issues pertaining to set theory, but nonetheless states the following:

"Any rigorous foundation capable of supporting the ordinary theory of classes
would equally well support our theory. Hence we have chosen to adopt the
intuitive standpoint, leaving the reader free to insert whatever type of
logical foundation (or absence thereof) he may prefer." (page 246)

So, as far as I see it, their position is more that of a form of agnosticism
that acknowledges that set theory or variants thereof does the job, but also
sort of states that the "intuitive standpoint" is their default position. So it
declares axioms for a model and leaves open to discussion the foundational
framework in which model theoretic constructions may be carried out.

However, it also states that categories are kind of a side construct that
should be avoided if it could be:

"It should be observed first that the whole concept of a category is
essentially an auxiliary one; our basic concepts are essentially those of a
functor and of a natural transformation." (page 247)

In a sense, it seems like the focus is on "arrows" rather than "objects", even
when it comes down to the "category of categories". It therefore implictly asks
the question "can one do category theory without objects ?" Having studied
partially defined semi-groups a bit (which is almost the closest I can come up
to the notion of an object-less category) I came to the conclusion that
categorical units do bring some form of coherence to a category compared to a
partially defined semi-group. My attempts to mimick categorical units or
represent categorical units in mere partially defined semi-groups led me to
some idempotents that may not be arranged into idempotents of a categorical
unit. There is a coherence issue (that I won't go into here) that leads me to
think that a category is indeed something more that a mere partially defined
semi-group, even one with "enough idempotents". There is a coherence condition
for these idempotents that I haven't yet been able to properly pinpoint.

Bottom line: It seems to me MacLane and Eilenberg downplayed the role of
categorical units in that document. Or that there is a generalisation of
categories into object-less categories that hasn't yet made it through in the
litterature.

"Perhaps the simplest precise device would be to speak not of the category of
groups, but of a category of groups (meaning, any legitimate such category)."
(page 247)

As far as my model theoretic tastes go, I'm quite fine talking about a model of
the first order theory of the category of all groups in the language of
categories. That fits most of my needs, and it does not pose much
set-theoretical problems, if I'm bent on enforcing compatibility with set
theory (which I usually am not).

"A functor such as "Hom" is then a functor which can be defined for any two
suitable categories of groups, G and H. Its values lie in a third category of
groups, which will in general include groups in neither G nor H." (page 247)

This is the approach I tend to follow. When I study a category model
theoretically, I feel no shame about considering binary relations whose domains
and codomains are the whole of the category. Of course, if one takes "the"
category of "all" binary relations, that binary "meta"-relation is not an arrow
of that category. It lies outside.

In fact, that construction is implicit in the notion of subobjects in
elementary topoi. Aside for the requirement that we deal with monomorphisms, it
essentially is a quasi-order on the "meta"-collection of all arrows having a
given target object. It's big. It's only because we quotient it into an
ordering properly that it becomes small enough.

Topoi axioms require that the subobject functor may be internalised. While that
makes them nice to work with, I believe it obfuscates the possibility that
analogues of the powerset functor in non-topoi may be dealt with if we allow
ourselves to work outside of that non-topos category, just like we would do in
model theory, if only we allowed ourselves to think of a category as a model in
itself.

"One might choose to adopt the (unramified) theory of types as a foundation for
the theory of classes. [...] One can also choose a set of axioms for classes as
in the Fraenkel-von Neumann-Bernays system. A category is then any (legitimate)
class in the sense of this axiomatics."

While the approach I tend to adopt seems to fit in the theory of types, I do
not believe it fits well (as far as I see) within the Bernays class system. In
the end, I treat a category as a model, and I'm being agnostic of the
foundational framework in which I do this model theoretical approach. I tend to
find that approach practical and pragmatic, and I have seen scant potent
objections to the way in which this approach may be retroffited into a given
foundational framework.

Bottom line: Take a category C as Bernays class. Consider that as a model. Call
T(C) its theory in the language of categories. Consider models of T(C) in
whatever foundational framework you may wish. And then stop worrying too much.
Or worry about it in the same way you would about models of, say, ZFC.

Sometimes I wonder what the foundational fuss and semi-false-paradoxes about
category theory is all about.

What I am frustrated about, however, is the current status of axiomatics of
categories. On four main counts:

1. There is an ideology about category that seems to make the connection with
its axiomatics obscure, and very much anti-relational. I sometimes see axioms
stating stuff like "A category is the data of (among other things) for all A,
B, C in Ob(C), a mapping o_A,B,C : Mor(C)(B,C) x Mor(C)(A,B) → Mor(C)(A,C)".
The level of cluttering and obfuscation of the simple fact that there is a bona
fide partially defined composition law, all that because of this fixation on
objects ? Honestly, it irritates me. I do not see axioms there, but a mimickry
of axioms.

2. There is a stratification of associative structures such as semigroups,
monoids, regular semi-groups, groups, partially defined semi-groups,
categories, groupoids, inductive groupoids. There honestly could be a much
tighter combinatorial setup to sum up all these structures in one unique
axiomatic scheme. I have one in mind that I will illustrate on the case of
groups: the two axioms below axiomatise groups under the additional assumption
that the ternary relation interprets a (fully defined) binary operation (ab⇝c
iff a.b = c) admitting a unit. (A fun exercise.)

xy⇝u    xv⇝w
yz⇝v    uz⇝w
----    ----
xv⇝w    xy⇝u
uz⇝w    yz⇝v

In this custom notation, it is clear that premisses and conclusions are
reversed in these two axioms. In more conventional logical notations, below,
this is a bit less obvious:

∀x,u,v,z, (∃y, xy⇝u ∧ yz⇝v) => (∃w, xv⇝w ∧ uz⇝w)
∀x,u,v,z, (∃y, xy⇝u ∧ yz⇝v) <= (∃w, xv⇝w ∧ uz⇝w)

Analogously, partially defined semi-groups may be axiomatised by the three
axioms below (whose combinatorial commonality with the two above should be
apparent) under the additional assumption that the ternary relation interprets
a partially defined operation.

xv⇝w    xy⇝u    xy⇝u
yz⇝v    yz⇝v    uz⇝w
----    ----    ----
xy⇝u    xv⇝w    xv⇝w
uz⇝w    uz⇝w    yz⇝v

∀x,v,z,w, (∃v, xv⇝w ∧ yz⇝v) => (∃u, xy⇝u ∧ uz⇝w)
∀x,u,v,z, (∃y, xy⇝u ∧ yz⇝v) => (∃w, xv⇝w ∧ uz⇝w)
∀x,v,z,w, (∃u, xy⇝u ∧ uz⇝w) => (∃v, xv⇝w ∧ yz⇝v)

Add similar axioms for units, and you axiomatise category. Add again the second
axiom for groups above, you axiomatise groupoids. Drop the unit requirement in
the axiomatisation of groups, you get a stronger class than regular semi-groups
that includes some so-called regular bands. So there exists a combinatorial
stratification of axiomatisations of associative structures into which
categories do fit.

3. On top of that stratification, there is the question of higher categories.
The structures mentioned in point 2. above all are algebraic in nature. Higher
categories are define algebraically whenever I read a definition of them, but
the reality is that people understand composition in such higher categories not
as "u.v is w" but rather as "u.v is roughly w, up to some wiggly arrow that we
take much pain to write compatibility conditions for". The generalised law of
associativity is indeed induced by the following additional axiom when
interpreting ~ below as equality:

uv⇝w
xy⇝z
u~v
x~y
-----
w~z

This is a construct akin to congruence, which, when properly relaxed, yields
(as far as I've investigated) decent axiomatisations for higher categories.

4. As mentioned in MacLane and Eilenberg's paper, the core focus of categories
was to investigate the notion of naturality. The rest is cruft outside of the
initial scope. And this is where I believe the notion of model is,
unfortunately ill suited. As Lawvere did set it up, one may view a domain as a
cartesian functor S: F° → Set where F is the category of finite sets and
mappings thereof. And there is a way to encode a substitutional fragment of
manipulations of first-order formulas as a functor T: F → Set, which one may
put in correspondance with S to encode (very roughly) a relational model. As
the category Δ of finite totally ordered sets and injective isotone mappings
thereof can be embedded into F semi-canonically, one may also consider a
relaxed notion of domain of a model as a functor S: Δ° → Set. With further
(admittedly painful) refinements, it is possible to note that the fact that the
variables in the axioms we gave for groups and partially defined semi-groups
occur without repetition in a given order (if one sees xy⇝u in an atomic
statement in an axiom, one never sees yx⇝u as the transposition of x and y
would break the ordering of variables) seem to insinuate that S: Δ° → Set is a
better conceptualisation for the notion of "natural structure". Categories as
bona fide models yield a functor S: F° → Set to encode its domain, and,
precomposed by Δ → F, this yields a natural structure S: Δ° → Set. This is a
widening of what one may think of to be a model. But a widening that I think
would be required to conceptually capture the notion of naturality more
correctly.

In a nutshell: As much as I'd like a categorically friendly foundations for
maths, I do not believe topos theory is the endgame in foundations: seems, as
discussed above, that even the notion of a model, whether of a topos or of ZFC,
may be put in dispute.

> 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.

Thank you for the reference.

1964, "An Elementary Theory of the Category of Sets", Proceedings of the
National Academy of Sciences U.S.A., 52: 1506–1511.

I have a problem with axiom 4 which states that 1 is a generator. I believe
there are reasons to study analogous systems, where 1 is not a generator and
does not even exist (which viciates axiom 1 and 3).

The statement of axiom 5 (axiom of choice) as the existence of a g such that
f.g.f = f however raises my interest.

One of the reasons it does is that I'd be much more interested in axiomatising
the category Rel of binary relations between sets than the category of mappings
between them. (And a partial mapping indeed is a peculiar binary relation
characterised by the property that if (x,z) and (x',z') are in its graph, then
x = x' implies z = z', much like the relation ~ in point 3. above).

One of the properties of the category Rel that does not a priori derive from
its categorical axioms is the existtence and properties of the functor Rel° ->
Rel fixing objects that sends a binary relation to its converse relation. Which
makes Rel a dagger category.

It turns out that all possible daggers in Rel may be classified (they are
uniquely determined by the data of an involution on each object of Rel). And
among all these daggers (as far as I can trust my personal notes) the
conversion is the unique one that coincides with pseudo-inversion when defined.
Pseudo-inversion is indeed, roughly, the existence of a unique such g such that
f.g.f = f (as in axiom 5) and conversely so too when transposing the role of f
and g.

A result which helps in the axiomatisation of the category Rel: conversion in
Rel is second-order definable in the language of categories.

Best regards.

Jodmos Horon.