How analogous are categorial and material set theories?

How analogous are categorial and material set theories?

[Neil Barton]

Dear All,

I'm very interested in how categorial and material set theories
interact, and in particular the advantages of each.

It's well-known that categorial viewpoints are good for isolating
schematic structural relationships. We can look at sets through this
lens, by considering a categorial set theory like ETCS (possibly
augmented, e.g. with replacement). A remark one sometimes finds is
that once you have defined membership via arrows from terminal
objects, you could use ETCS for all the purposes to which ZFC is
normally put.

My question is the following:

(Q) To what extent can you ``do almost the same work'' with a
categorial set theory like ETCS vs. a material set theory like ZFC?

Just to give a bit more detail concerning what I'm thinking of:
Something material set theory is reasonably good at is building models
(say to analyse relative consistency), or comparing cardinality.
However, there's no denying that for representing abstract
relationships the language is somewhat clunky, since the same abstract
schematic type can be multiply instantiated by structures with very
different set-theoretic properties. So, to what extent can a
categorial set theory like ETCS supply the good bits of the fineness
of grain associated with material set theories, whilst modding out the
`noise'?

For example, the following are easily stated in material set theory:

1. \aleph_17 is an accessible cardinal.

In material set theory, it's easy to define the aleph function and
then state that the 17th position in this function can be reached by
iterating powerset and replacement. But I wouldn't even know how to
talk about specific sets of different cardinalities categorially. I
suppose you could say something in terms of isomorphism between
subobjects, and then exponentials, but it's quite unclear to me how
the specifcs would go. Is that an easily claim to state (and prove) in
ETCS?

2. How would you state that {{}} and {\beth_\omega} are very different
objects? Set-theoretically, these look very different (just consider
their transitive closures, for instance). But category-theoretically
they should look the same---since they are both singletons they are
isomorphic. So is this a case where their different set-theoretic
propeties are considered just `noise', or where ETCS just wouldn't see
a relationship, or where ETCS can in fact see some of these properties
(and I'm just missing something)?

3. How would ETCS deal with model theory and cardinality ascriptions?
(This links to a question asked earlier on this mailing list
concerning syntactic theories in category theory, and whether from the
categorial viewpoint we should be taking notice of them at all.) For
instance, it's an interesting theorem (for characterising structure)
that a first-order theory categorical in one uncountable power is
categorical in every uncountable power (Morley's Theorem). But I have
no idea how one might formalise this in something like ETCS---I know
of Makkai and Reyes textbook (which I am currently reading) on
categorial logic (where theories are represented by categories and
models by functors), but I don't see how you could get
categoricity-in-power claims out of the set up there. Can this be
done?

Any help and/or discussion would be greatly appreciated!

Best Wishes,

Neil

-- 
Dr. Neil Barton
Postdoctoral Research Fellow
Kurt Gödel Research Center for Mathematical Logic
University of Vienna
Web: https://neilbarton.net/


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: How analogous are categorial and material set theories?

[Patrik Eklund]

Dear Neil,

Others in this list are much more prominent to answer to your question,
but let me provide one viewpoint.

Set theoryvis really about the theory of sets. Functions and powersets
are there, and complicated structures can evolve. However, a striking
thing about sets is that they are "untyped", which can be given a number
of meanings.

When we move into category theory, the category of sets and functions is
the simplest one. Sets come with no structure, so functions do not
prserve any such structure.

Now, functors over a category become important, the powerset functor
over that most simple and unstructured category of sets being a prime
example.

We need structure, and many real world applications require quite
elaborate structure. Functors over more elaborate categories become
important, where monoidal closed categories as unnderlying categories
bring in fundamental algebraic structures, even for a generalized
powerset functors.

Let me also speak warmly about the term functor, i.e., the functor that
formally constructs terms over a given signature. Such a term functor
over the category of sets and functions produces nothing but
conventional terms, but a term functor over a monoidal category with
more structure can provide terms and expressions with richer structure
and attributes. Stochastic and many-valued aspects are good examples,
and I often refer to nomenclatures in health care, where additions
structure is needed. Expressions e.g. involving diagnoses, functioning
and drugs do not run over the same category, and doing all of it in set
theory is basically ridiculous.

Not sure if these remarks help you at all, so I sincerely hope that more
prominent category theorists subscribing to this mailing list will
provide more enriched comments.

All the best and good luck with your work!

Patrik



On 2017-11-25 00:36, Neil Barton wrote:
> Dear All,
>
> I'm very interested in how categorial and material set theories
> interact, and in particular the advantages of each.
>
> It's well-known that categorial viewpoints are good for isolating
> schematic structural relationships. We can look at sets through this
> lens, by considering a categorial set theory like ETCS (possibly
> augmented, e.g. with replacement). A remark one sometimes finds is
> that once you have defined membership via arrows from terminal
> objects, you could use ETCS for all the purposes to which ZFC is
> normally put.
>
> My question is the following:
>
> (Q) To what extent can you ``do almost the same work'' with a
> categorial set theory like ETCS vs. a material set theory like ZFC?
>
> Just to give a bit more detail concerning what I'm thinking of:
> Something material set theory is reasonably good at is building models
> (say to analyse relative consistency), or comparing cardinality.
> However, there's no denying that for representing abstract
> relationships the language is somewhat clunky, since the same abstract
> schematic type can be multiply instantiated by structures with very
> different set-theoretic properties. So, to what extent can a
> categorial set theory like ETCS supply the good bits of the fineness
> of grain associated with material set theories, whilst modding out the
> `noise'?
>
> For example, the following are easily stated in material set theory:
>
> 1. \aleph_17 is an accessible cardinal.
>
> In material set theory, it's easy to define the aleph function and
> then state that the 17th position in this function can be reached by
> iterating powerset and replacement. But I wouldn't even know how to
> talk about specific sets of different cardinalities categorially. I
> suppose you could say something in terms of isomorphism between
> subobjects, and then exponentials, but it's quite unclear to me how
> the specifcs would go. Is that an easily claim to state (and prove) in
> ETCS?
>
> 2. How would you state that {{}} and {\beth_\omega} are very different
> objects? Set-theoretically, these look very different (just consider
> their transitive closures, for instance). But category-theoretically
> they should look the same---since they are both singletons they are
> isomorphic. So is this a case where their different set-theoretic
> propeties are considered just `noise', or where ETCS just wouldn't see
> a relationship, or where ETCS can in fact see some of these properties
> (and I'm just missing something)?
>
> 3. How would ETCS deal with model theory and cardinality ascriptions?
> (This links to a question asked earlier on this mailing list
> concerning syntactic theories in category theory, and whether from the
> categorial viewpoint we should be taking notice of them at all.) For
> instance, it's an interesting theorem (for characterising structure)
> that a first-order theory categorical in one uncountable power is
> categorical in every uncountable power (Morley's Theorem). But I have
> no idea how one might formalise this in something like ETCS---I know
> of Makkai and Reyes textbook (which I am currently reading) on
> categorial logic (where theories are represented by categories and
> models by functors), but I don't see how you could get
> categoricity-in-power claims out of the set up there. Can this be
> done?
>
> Any help and/or discussion would be greatly appreciated!
>
> Best Wishes,
>
> Neil
>
> --
> Dr. Neil Barton
> Postdoctoral Research Fellow
> Kurt G??del Research Center for Mathematical Logic
> University of Vienna
> Web: https://neilbarton.net/
>
>
> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: How analogous are categorial and material set theories?

[Michael Shulman]

Sorry, forgot to include original citations: the comparison of ZFC to
ETCS goes back to Osius, Cole, and Mitchell in the 1970s, while
various replacement axioms for ETCS have been formulated by Lawvere,
Cole, Osius, and McLarty.

On Mon, Nov 27, 2017 at 4:06 AM, Michael Shulman <shulman@sandiego.edu> wrote:
> In general, I don't think ETCS has any more trouble building models or
> comparing cardinality than ZFC does.  A model in the abstract sense of
> model theory doesn't use any of the "internal" membership-structure of
> a ZFC-set; it is a purely structural entity: a set equipped with
> certain functions and relations.  So I don't see why any
> model-theoretic theorem would be any harder to formalize in ETCS than
> in ZFC.
>
> To translate statements from ZFC to ETCS that *do* involve internal
> membership-structure, like distinguishing between {{}} and
> {\beth_\omega}, one has to make that structure explicit by talking
> about sets equipped with certain well-founded relations.  There are
> various ways to recover a model of a ZFC-like set theory inside ETCS:
> rigid trees, accessible well-pointed graphs, etc.  If one only wants
> to talk about ordinal numbers, which is much more common, then one
> doesn't need all that machinery; one can just talk about well-ordered
> sets (up to isomorphism, like any other kind of structured set).
>
> ETCS is weaker than ZFC in that it doesn't include an analogue of the
> axiom of replacement, which is needed for things like defining the
> aleph function in generality.  However, there are various ways to add
> a replacement axiom to it, generally stated as a sort of "stack"
> condition.  This in particular allows defining families of sets by
> recursion over well-founded relations, so that you can recurse over
> any ordinal to get an aleph function on that ordinal, and then play
> games with the analogue of proper classes to get "one aleph function"
> if you like.
>
> Some of these issues are discussed in my preprint
> https://arxiv.org/abs/1004.3802 .
>
> On Fri, Nov 24, 2017 at 2:36 PM, Neil Barton <bartonna@gmail.com> wrote:
>> Dear All,
>>
>> I'm very interested in how categorial and material set theories
>> interact, and in particular the advantages of each.
>>
>> It's well-known that categorial viewpoints are good for isolating
>> schematic structural relationships. We can look at sets through this
>> lens, by considering a categorial set theory like ETCS (possibly
>> augmented, e.g. with replacement). A remark one sometimes finds is
>> that once you have defined membership via arrows from terminal
>> objects, you could use ETCS for all the purposes to which ZFC is
>> normally put.
>>
>> My question is the following:
>>
>> (Q) To what extent can you ``do almost the same work'' with a
>> categorial set theory like ETCS vs. a material set theory like ZFC?
>>
>> Just to give a bit more detail concerning what I'm thinking of:
>> Something material set theory is reasonably good at is building models
>> (say to analyse relative consistency), or comparing cardinality.
>> However, there's no denying that for representing abstract
>> relationships the language is somewhat clunky, since the same abstract
>> schematic type can be multiply instantiated by structures with very
>> different set-theoretic properties. So, to what extent can a
>> categorial set theory like ETCS supply the good bits of the fineness
>> of grain associated with material set theories, whilst modding out the
>> `noise'?
>>
>> For example, the following are easily stated in material set theory:
>>
>> 1. \aleph_17 is an accessible cardinal.
>>
>> In material set theory, it's easy to define the aleph function and
>> then state that the 17th position in this function can be reached by
>> iterating powerset and replacement. But I wouldn't even know how to
>> talk about specific sets of different cardinalities categorially. I
>> suppose you could say something in terms of isomorphism between
>> subobjects, and then exponentials, but it's quite unclear to me how
>> the specifcs would go. Is that an easily claim to state (and prove) in
>> ETCS?
>>
>> 2. How would you state that {{}} and {\beth_\omega} are very different
>> objects? Set-theoretically, these look very different (just consider
>> their transitive closures, for instance). But category-theoretically
>> they should look the same---since they are both singletons they are
>> isomorphic. So is this a case where their different set-theoretic
>> propeties are considered just `noise', or where ETCS just wouldn't see
>> a relationship, or where ETCS can in fact see some of these properties
>> (and I'm just missing something)?
>>
>> 3. How would ETCS deal with model theory and cardinality ascriptions?
>> (This links to a question asked earlier on this mailing list
>> concerning syntactic theories in category theory, and whether from the
>> categorial viewpoint we should be taking notice of them at all.) For
>> instance, it's an interesting theorem (for characterising structure)
>> that a first-order theory categorical in one uncountable power is
>> categorical in every uncountable power (Morley's Theorem). But I have
>> no idea how one might formalise this in something like ETCS---I know
>> of Makkai and Reyes textbook (which I am currently reading) on
>> categorial logic (where theories are represented by categories and
>> models by functors), but I don't see how you could get
>> categoricity-in-power claims out of the set up there. Can this be
>> done?
>>
>> Any help and/or discussion would be greatly appreciated!
>>
>> Best Wishes,
>>
>> Neil
>>
>> --
>> Dr. Neil Barton
>> Postdoctoral Research Fellow
>> Kurt Gödel Research Center for Mathematical Logic
>> University of Vienna
>> Web: https://neilbarton.net/
>>
>>
>> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: How analogous are categorial and material set theories?

[Neil Barton]

Dear All,

Thanks so much for your kind and patient responses, and apologies for
the slow reply (I wanted to check out some of Michael's
recommendations before replying).

@Patrik: Thanks for the nice examples and applications. I certainly
don't want to deny that category theory has applications where
material set theory would be inappropriate, but rather to specifically
see if there were any applications to which material set theory was
more suited (and how this can then be incorporated into the structural
setting). However, your examples are useful to see just how different
the two perspectives are (I agree that systematising certain subject
matters in material set theory would be a fruitless project).

@Michael: Thanks very much for the reference. I think I see the proof:
One recovers a model of ZFC not by considering the membership relation
of ETCS (given by various f: 1--> X), but rather by finding the
`membership graph' for the relevant sets in a category satisfying ETCS
(with the replacement stack axiom added).  I do have a question here
though---here we are expected to take the *class* of  all well-founded
extensional accessible pointed graphs, and note that ZFC holds within
this class. Whilst I'm happy that the lemmas showing that the required
graphs exist in the category Set are categorial, it seems to me that
to isolate all these and talk about the *class* of all of them
requires some material-set-theoretic machinery. Is there a *purely
categorial* way of talking about this `collection' of subgraphs in
Set? Or have I missed something?

I suppose this is equivalent to the requirement of asking for a (set)
model of ZFC in material set theory. So could one simply state an
extra axiom to be added to ETCS+: ``Set contains an well-founded
extensional accessible pointed graphs such that...[list the APG ZFC
axioms].''. Is this acceptable in a *pure* categorial framework, or do
you think that presupposes some material set theory? I suppose there
is also the question of how to recover the cumulative hierarchy in
this framework---in the paper you sent me this is done with a
non-categorial theory of ordinals (possibly given by material set
theory).

(This relates to a more general question I have concerning categorial
foundations: Are there people who claim we should do foundational
research *solely* in the language of category theory, or does almost
everyone accept that the `external' (possibly material set-theoretic)
perspective is also allowed? So, for example, when considering the
category of sheaves over a topological space, whilst I could take a
purely categorial outlook, nonetheless sometimes I might want to just
look at the equivalence class of an open set U relative to a point i
in the topological space defined in material set theory. The two
perspectives seem to complement rather than contradict each other, but
I wonder what the general feeling is concerning the interellation of
the two foundational systems.)

(This in turn relates to the wider question: How can material and
structural set theories inform one another? It *seems* to me (without
any deep arguments for the claim) that material set theory is just
better suited to certain roles (such as the formulation of large
cardinal hypotheses) whilst structural set theory better suited to
systematising the algebraic roles we want sets to perform. This is
despite the fact that we can simulate one perspective within the
other; for example just because you *can* simulate talk of categories
with, say, Grothendieck universes, doesn't mean that it's a
particularly *natural* interpretation.)

@Steve. You ask:  When you look at making set theory more categorical,
are you just looking for a categorical way to do essentially the same
thing, or are you trying more deeply to expose possible limitations of
set theory?

I don't think I'm clearly aiming at either (though I am interested in
these questions). I'm trying to understand more clearly what purposes
each foundation is best suited to, and how we can relate the two. I
suppose it's a mixture of the two---the present paper I'm currently
writing looks to modify material set theory to get something more
`structure respecting', but nonetheless facilitating the combinatorial
power and conceptual simplicity it offers (allowing us to easily work
with notions such as cardinality). I'm trying to get a better picture
of the landscape though, and doing this requires understanding the
other direction (i.e. how one can mimic material set-theoretic claims
in the structural setting).

Thanks again!

Best Wishes,

Neil


On 27 November 2017 at 17:49, Steve Vickers <s.j.vickers@cs.bham.ac.uk> wrote:
> Dear Neil,
>
> This is not an answer to your question, so please ignore it if you're not  so
> interested in these broader issues.
>
> My broad question is this. When you look at making set theory more
> categorical, are you just looking for a categorical way to do essentially
> the same thing, or are you trying more deeply to expose possible limitations
> of set theory?
>
> One thing shared by ETCS and ZFC is the well-pointedness: that the object  is
> determined by its global elements (morphisms from 1).
>
> That can seem obvious if what you're trying to capture is some idea of
> collection, but in fact it breaks down when the collection has topological
> structure. The cohesion between points goes beyond what can be explained in
> terms of the global points themselves, and in point-free topology we see
> non-trivial spaces with no global points at all. This is not necessarily a
> pathology of point-free topology but can be related to topological facts
> such as the existence of principal bundles with no continuous global
> sections. It also feeds back into "sets" as discrete spaces, with
> non-well-pointed toposes of sheaves (= local homeomorphisms = fibrewise
> discrete bundles).
>
...

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: How analogous are categorial and material set theories?

[Steve Vickers]

Dear Neil,

Some comments below.

All the best,

Steve.

On 03/12/2017 16:12, bartonna@gmail.com wrote:
> ...
>
> (This relates to a more general question I have concerning categorial
> foundations: Are there people who claim we should do foundational
> research *solely* in the language of category theory, or does almost
> everyone accept that the `external' (possibly material set-theoretic)
> perspective is also allowed? So, for example, when considering the
> category of sheaves over a topological space, whilst I could take a
> purely categorial outlook, nonetheless sometimes I might want to just
> look at the equivalence class of an open set U relative to a point i
> in the topological space defined in material set theory. The two
> perspectives seem to complement rather than contradict each other, but
> I wonder what the general feeling is concerning the interellation of
> the two foundational systems.)
Yes, I think I would claim that the foundational work should be in the
language of categories. Much of the justification for that is pragmatic
methodology, in that category theory has proved itself effective in
elucidating the underlying mathematics common to different foundations.

I have been hugely influenced in this by my experience of relating
topology to logic, and point-set approaches to point-free. It is
category theory that shows us how point-set and point-free are doing
similar things, using structure shared by the categories of topological
spaces and of point-free spaces such as locales. And we don't have to go
far down this road before the comparison starts to show point-set
topology in an unfavourable light.

A similar example of the categorical analysis of foundations is
Grothendieck's discovery of toposes. (This is my rational
reconstruction, so apologies - to you and to Grothendieck - if it's
bollocks historically.) Grothendieck asked what mathematics was needed
to do sheaf cohomology, known from sheaves over topological spaces, and
gave an answer using categorical structure. Abstracting that gave us
Grothendieck toposes, thus generalized spaces in the sense that you can
still do sheaf cohomology over them.

The methodology is not entirely pragmatic, however. Categorical
structure explicitly describes how objects relate to each other (via
morphisms) as opposed to how they are structured internally. The real
mathematics lies in those mutual relationships. Any foundational
discussion that says the mathematics _is_ the structures - the sets or
whatever - is answering the wrong questions. Those structures are just
particular solutions to the mathematical problem. It is the same as the
difference between the API of a software library (how the calling
program relates to the library routines it calls) and the implementation
of the library routines - which is best left hidden and subject to revision.
>
> ...
>
> @Steve. You ask:  When you look at making set theory more categorical,
> are you just looking for a categorical way to do essentially the same
> thing, or are you trying more deeply to expose possible limitations of
> set theory?
>
> I don't think I'm clearly aiming at either (though I am interested in
> these questions). I'm trying to understand more clearly what purposes
> each foundation is best suited to, and how we can relate the two. I
> suppose it's a mixture of the two---the present paper I'm currently
> writing looks to modify material set theory to get something more
> `structure respecting', but nonetheless facilitating the combinatorial
> power and conceptual simplicity it offers (allowing us to easily work
> with notions such as cardinality). I'm trying to get a better picture
> of the landscape though, and doing this requires understanding the
> other direction (i.e. how one can mimic material set-theoretic claims
> in the structural setting).
Cardinality is in fact what I had in mind when I asked the question. It
is one of those notions that tends to fade away when category theory
takes you from one foundational setting to another, say from classical
maths to constructive, or from point-set topology to point-free.

  From one point of view ("making set theory more categorical") you would
be interested in finding a categorical description that can still deal
with cardinalities. From the other ("exposing possible limitations") you
would use the categories as reason for losing interest in cardinalities.



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: How analogous are categorial and material set theories?

[Patrik Eklund]

Is Category Theory a Theory? I think not. At least not in a logical
sense.

Is Logic a Theory. Of course not. Logic is a construction that embraces
ways of creating logical theories.

Can we describe Category in Logic? No, we cannot.

Can we describe Logic in Category. Yes we can. Topos, and all that, even
if I regret we are happy about quantifiers being adjoint functors to the
contra powerfunctor. Logic should be a bit more than just that,
shouldn't it?

---

Can we describe Logic over Category? Yes we can. This is less
recognized. This is the lative construction of logic from signatures,
through terms, to sentences, and so on, as Goguen (Institutions) and
Meseguer (Entailment Systems) did, without being explicit about
signatures. This is Category Theory as a construction embracing ways of
creating logics. We must be explicit about the starting point, the
underlying signature. Just think about it, we potentially have the
object of types in a monoidal category! It's just around the corner.
Let's go get it, and the world will never be the same!

---

Discussions under FOM now related to distinctions between first, second
and third order logic is really bizarre, or boring to say the least.
Much of what they try to say could be said more clearly if they would
understand to use category theory as a construction site to build what
they try to build.

Hilbert was not a bad person, if you ask me.

---

Best,

Patrik


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: How analogous are categorial and material set theories?

[Steve Vickers]

Dear Patrik,

The theory of categories is a first order theory, so what exactly are you denying here?

Steve.

> On 7 Dec 2017, at 18:58, peklund@cs.umu.se wrote:
> 
> Is Category Theory a Theory? I think not. At least not in a logical
> sense.
> 



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: How analogous are categorial and material set theories?

[Cory Knapp]

Dear Neil,

(Sorry for the echoed mail: I forgot to scrub the html when sending to the list)

The discussion of cardinality reminds me of something that I had meant
to say earlier, but didn't quite find the words for.

It seems to me that in material set theory, the role of cardinality is
to give us an arithmetic--a way of computing with sets. This is a
response to the fact that sets  of material set theory are not (as you
point out) in any way algebraic objects. Essentially, cardinals give
us an arithmetic which respects bijection.

Cardinal arithmetic breaks down in a constructive setting: we need
choice to see that the cardinals are linearly ordered, and LEM to even
have them partially ordered. So, in constructive settings, cardinality
is simply not a well-behaved notion. However, I have never found
myself missing cardinals in type theory, and I spent a while wondering
why. The answer is that, in type theory (and also in structural set
theories) the objects are essentially algebraic objects, which means
we have a direct arithmetic of sets. We don't need to pass to a
surrogate arithmetic.

We can see this even with large-cardinal axioms, which are ultimately
not about cardinals, but about what sorts of objects exist in the
universe: an inaccessible tells us we have a (transitive, set-sized)
model of ZF; a Mahlo tells us (among many other things) that every set
is included in one. There's an order-theoretic way to express the
Mahlo condition on a cardinal (every monotone, continuous function on
the cardinal has a fixed point), and this in-turn allows us to relate
the notion to computational principles. In particular, see (e.g.)
Dybjer and Setzer's "Induction-recursion and initial Algebras" and
related work comparing induction-recursion to Mahlo cardinals.

The point of this (very sketchy) Mahlo example is that large cardinal
axioms tell us that certain sorts of arithmetical operations on
cardinals are well-defined. We can state such principles about the
objects of our theory directly if the objects are sufficiently
algebraic to begin with.

Best regards,
Cory

On Wed, Dec 6, 2017 at 11:33 AM, Cory Knapp <cory.m.knapp@gmail.com> wrote:
> Dear Neil,
>
> The discussion of cardinality reminds me of something that I had meant to
> say earlier, but didn't quite find the words for.
>
> It seems to me that in material set theory, the role of cardinality is to
> give us an arithmetic--a way of computing with sets. This is a response to
> the fact that sets  of material set theory are not (as you point out) in any
> way algebraic objects. Essentially, cardinals give us an arithmetic which
> respects bijection.
>
> Cardinal arithmetic breaks down in a constructive setting: we need choice to
> see that the cardinals are linearly ordered, and LEM to even have them
> partially ordered. So, in constructive settings, cardinality is simply not a
> well-behaved notion. However, I have never found myself missing cardinals in
> type theory, and I spent a while wondering why. The answer is that, in type
> theory (and also in structural set theories) the objects are essentially
> algebraic objects, which means we have a direct arithmetic of sets. We don't
> need to pass to a surrogate arithmetic.
>
> We can see this even with large-cardinal axioms, which are ultimately not
> about cardinals, but about what sorts of objects exist in the universe: an
> inaccessible tells us we have a (transitive, set-sized) model of ZF; a Mahlo
> tells us (among many other things) that every set is included in one.
> There's an order-theoretic way to express the Mahlo condition on a cardinal
> (every monotone, continuous function on the cardinal has a fixed point), and
> this in-turn allows us to relate the notion to computational principles. In
> particular, see (e.g.) Dybjer and Setzer's "Induction-recursion and initial
> Algebras" and related work comparing induction-recursion to Mahlo cardinals.
>
> The point of this (very sketchy) Mahlo example is that large cardinal axioms
> tell us that certain sorts of arithmetical operations on cardinals are
> well-defined. We can state such principles about the objects of our theory
> directly if the objects are sufficiently algebraic to begin with.
>
> Best regards,
> Cory
>
>
> On Mon, Dec 4, 2017 at 11:09 AM, Steve Vickers <s.j.vickers@cs.bham.ac.uk>
> wrote:
>>
>> Dear Neil,
>>
>> Some comments below.
>>
>> All the best,
>>
>> Steve.
>>
>> On 03/12/2017 16:12, bartonna@gmail.com wrote:
>>>
>>> ...
>>>
>>> (This relates to a more general question I have concerning categorial
>>> foundations: Are there people who claim we should do foundational
>>> research *solely* in the language of category theory, or does almost
>>> everyone accept that the `external' (possibly material set-theoretic)
>>> perspective is also allowed? So, for example, when considering the
>>> category of sheaves over a topological space, whilst I could take a
>>> purely categorial outlook, nonetheless sometimes I might want to just
>>> look at the equivalence class of an open set U relative to a point i
>>> in the topological space defined in material set theory. The two
>>> perspectives seem to complement rather than contradict each other, but
>>> I wonder what the general feeling is concerning the interellation of
>>> the two foundational systems.)
>>
>> Yes, I think I would claim that the foundational work should be in the
>> language of categories. Much of the justification for that is pragmatic
>> methodology, in that category theory has proved itself effective in
>> elucidating the underlying mathematics common to different foundations.
>>
>> I have been hugely influenced in this by my experience of relating
>> topology to logic, and point-set approaches to point-free. It is
>> category theory that shows us how point-set and point-free are doing
>> similar things, using structure shared by the categories of topological
>> spaces and of point-free spaces such as locales. And we don't have to go
>> far down this road before the comparison starts to show point-set
>> topology in an unfavourable light.
>>
>> A similar example of the categorical analysis of foundations is
>> Grothendieck's discovery of toposes. (This is my rational
>> reconstruction, so apologies - to you and to Grothendieck - if it's
>> bollocks historically.) Grothendieck asked what mathematics was needed
>> to do sheaf cohomology, known from sheaves over topological spaces, and
>> gave an answer using categorical structure. Abstracting that gave us
>> Grothendieck toposes, thus generalized spaces in the sense that you can
>> still do sheaf cohomology over them.
>>
>> The methodology is not entirely pragmatic, however. Categorical
>> structure explicitly describes how objects relate to each other (via
>> morphisms) as opposed to how they are structured internally. The real
>> mathematics lies in those mutual relationships. Any foundational
>> discussion that says the mathematics _is_ the structures - the sets or
>> whatever - is answering the wrong questions. Those structures are just
>> particular solutions to the mathematical problem. It is the same as the
>> difference between the API of a software library (how the calling
>> program relates to the library routines it calls) and the implementation
>> of the library routines - which is best left hidden and subject to
>> revision.
>>>
>>>
>>> ...
>>>
>>> @Steve. You ask:  When you look at making set theory more categorical,
>>> are you just looking for a categorical way to do essentially the same
>>> thing, or are you trying more deeply to expose possible limitations of
>>> set theory?
>>>
>>> I don't think I'm clearly aiming at either (though I am interested in
>>> these questions). I'm trying to understand more clearly what purposes
>>> each foundation is best suited to, and how we can relate the two. I
>>> suppose it's a mixture of the two---the present paper I'm currently
>>> writing looks to modify material set theory to get something more
>>> `structure respecting', but nonetheless facilitating the combinatorial
>>> power and conceptual simplicity it offers (allowing us to easily work
>>> with notions such as cardinality). I'm trying to get a better picture
>>> of the landscape though, and doing this requires understanding the
>>> other direction (i.e. how one can mimic material set-theoretic claims
>>> in the structural setting).
>>
>> Cardinality is in fact what I had in mind when I asked the question. It
>> is one of those notions that tends to fade away when category theory
>> takes you from one foundational setting to another, say from classical
>> maths to constructive, or from point-set topology to point-free.
>>
>>  From one point of view ("making set theory more categorical") you would
>> be interested in finding a categorical description that can still deal
>> with cardinalities. From the other ("exposing possible limitations") you
>> would use the categories as reason for losing interest in cardinalities.
>>
>>
>>
>>
>> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
>
>


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: How analogous are categorial and material set theories?

[Vaughan Pratt]

I prefer to think of what Steve presumably has in mind here as an
equational theory where composition is 2-ary where 2 is not 1+1 but
rather o--->o.

One difference between equational logic and first order logic is that
only the former has well-defined homomorphisms (not sure if Gerald Sacks
would have agreed).?? Just as group theory (in Steve's sense) has
homomorphisms, so does category theory in that sense have functors.

I'm not sure how one argues that CT has natural transformations
however.?? They seem to enter as part of the metatheory, which as usually
presented seems to be pretty set theoretic in its outlook. How do NT's
look in an HOTT account of CT?

The language of the Big Bang Theory is pretty family-oriented, except
for equality which seems somewhat controversial.?? But I digress.

Vaughan

On 12/07/17 10:49 PM, Steve Vickers wrote:
> Dear Patrik,
>
> The theory of categories is a first order theory, so what exactly are you denying here?
>
> Steve.
>
>> On 7 Dec 2017, at 18:58, peklund@cs.umu.se wrote:
>>
>> Is Category Theory a Theory? I think not. At least not in a logical
>> sense.
>>
>
>
> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: How analogous are categorial and material set theories?

[Neil Barton]

Dear All,

Thanks once again for the responses---I appreciate it!

@Cory. Thanks! This was helpful to see that the two perspectives
respond to different `needs' within mathematics, and that for many
applications the algebraic perspective suffices.

I did just want to pick up on the point about large cardinals. I
suspect that those sorts of `arithmetical definability'
characterisations will only work for cardinals you can characterise
from below (i.e. by stating that there's a fixed point for some sort
of describability property) and thus are likely to be consistent with
V=L. However, there are really interesting categorial
characterisations of *very* strong large cardinals, some of them
dating back to the 1960s (see Brooke-Taylor and Bagaria, `On Colimits
and Elementary Embeddings'). But I'm not really on top of this
material, so don't have a feel for how the proof works yet (other than
that the embeddability in the category-theoretic setting somehow
transfers to the existence of large cardinal embeddings in set
theory).

@Mike. Thanks for the points about the meta-theory---all clear to me
now. Similarly for ordinals.

I was talking about the etale space. My claim wasn't meant to be that
it *couldn't* be done structurally, just that sometimes the
set-theoretic perspective is useful for seeing what's going on in a
particular construction (but maybe this is just a holdover of how I
first came across sheaves---then there was a lot of quotienting in
material set theory).

You're right of course about the large cardinals (as I mentioned to
Cory). This strikes me as very interesting stuff that I'm just not on
top of yet. The example of L is also super-nice...thanks! I will have
a think about this.

@Patrik: I'm also unsure how category theory is not a `theory'.
Obviously were interested in many and varied categories but the core
axiomatisation of what a category is is still first-order. Similarly
in material set theory, even though ZFC is the `core' set theory (for
many people anyway) we still consider lots of different theories. So I
don't see how the phrase `is category theory a theory? I think not.'
wouldn't apply mutatis mutandis to material set theory.

I *do* think however there's an important philosophical difference:
Set theory aims at an intended interpretation (the cumulative
hierarchy), whereas category theory doesn't (the whole *point* of it
is to apply across diverse contexts). But maybe things are more subtle
than I realise [plus I'm maybe straying into off-list philosophical
territory with this claim].

Best Wishes,

Neil

On 8 December 2017 at 06:49, Steve Vickers <s.j.vickers@cs.bham.ac.uk> wrote:
> Dear Patrik,
>
> The theory of categories is a first order theory, so what exactly are you  denying here?
>
> Steve.
>
>> On 7 Dec 2017, at 18:58, peklund@cs.umu.se wrote:
>>
>> Is Category Theory a Theory? I think not. At least not in a logical
>> sense.
>>
>
>
>
> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]



-- 
Dr. Neil Barton
Postdoctoral Research Fellow
Kurt Gödel Research Center for Mathematical Logic
University of Vienna


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Is Category Theory a Theory?

[Patrik Eklund]

Thank you, Hidekazu-san, for you reply.

You use several important keywords that we could debate much more, and I
sincerely hope Catlist will.

One word you use is "role". I find that very appealling and intriguing.
What is the role of zero in the natural numbers signature? What is the
role of zero as a term and number in the axiomatized number system. Does
that role change and does it appear as a 'subrole' in another role? I
don't know, and I am certainly overly intuitive saying so, but if we do
not allow ourselves to do that, we will forever remain applying
"ignorabimus", something Hilbert fiercely rejected, ending his famous
radio speech with "We must know! We will know!".

When I said "Is Category Theory a Theory? I think not. At least not in a
logical sense." I obviously refer to "theory" as logically defined by
the set of all 'clauses' we can 'infer' starting from all acceptable
clauses ('axioms'), iteratively throwing them into the acceptables, and
exhaustively doing that over and over again. Is Category Theory such a
Theory. Of course it isn't. It's much more. If it isn't, why are we
here? A monoidal category is a good example. It's not a category. It
contains one, but as a structure it's not a category. Yet, monoidal
categories are part of category theory. I allow myself to say that the
category in a monoidal category plays a certain Role in that structure.
So does the tensor, and soon we almost feel more algebraic than
categorical. If we do, well, is a monoidal category then a foundation
for a signature?! Signature in a broader sense, of course. Why not? We
obtain expression, words, and so on. Maybe somewhere along that line
somebody starts to think "What is a Turing Category?". What I try to say
is that if we disallow ourselves to think in these ways, we apply that
"ignorabimus". Your intuition about "role" seems to be quite rich, and I
surely do not provide it with the appreciation it deserves, but I hope
to hear more about it in years to come.

You also use "properties", which in logic often means fixing how certain
expression relate to each other. Algebra may be more fundamental than we
think, and myself I am inclined to explore this more than I have before.
Indeed, when in 'lativity' I underline that "signatures come first, and
then we create sentences, and so on, latively", am I not actually
speaking warmly about algebra being among the first ones in line?
"Algebra studying itself" may be interesting to further explore, and to
compare it with "logic studying itself" and "set theory studying
itself". Clearly we also have "logic studying set theory", "algebra
studying logic", "logic studing algebra", and in fact all combinations.
Do we not even have "algebra studying how logic is studying itself", and
so on? I think we do, and this really to me is one of the reasons why we
sometimes so little understand each other, because we do not always
clearly acknowledge what we really are doing and why, when we e.g.
describe category theory as a logic, logic in a topos, categories as
algebras, logic over a monoidal closed category, and so. Why do we do
these things. I develop logic over monoidal closed categories because I
see how underlying rich structures of a certain information scope (like
health ontology) suitable can be represented because of such a category
so that reasoning involving that information enables us to say more than
we have used to be hearing (in health care). I am seriously starting to
believe that we are able to save lives by enriching health language with
category theory.

So thank you once again again, Hidekazu-san, for sharing your thoughts.
It is not unskillful at all, and certainly has no mistakes. It's
Excellent Harmony.

Looking forward to more debate on these aspects.

Best regards,

Patrik

PS My origical catlist posting was forwarded also to FOM, in the hope
that the FOM community would be even more interested to bridge
foundations with aspects learned within Category Theory. That forward
was rejected:
   "Your message was deemed inappropriate by the moderator after
   consulting our editors. One of them wrote: "This message seems to be
   mainly an expression of Eklund's personal opinions, with no supporting
   arguments and little clarity. I recommend rejecting it.""
I replied to the fom-owner as follows:
Thank you for your response.
   The reason why I sent it to Catlist was to raise some debate more than
presenting my personal opinion. Catlist accepted it, and I thought I
would bridge it over to FOM, since recently FOM has taken up an interest
to undestand the role of category theory for foundations.
   Obviously the content was less kind and more provocative to the FOM
readers, and my guess was it will be rejected.
   Anyway, I appreciate very much to be part of dialogue within FOM and I
take this opportunity to thank you for all acceptances so far of many of
my postings.
   My gut feeling is that foundations discussions are finding and
exploring new dimensions. There are Pandora boxes around some corners,
and there is resistence to open some of these.
   Anyway, it's all up to us, and we will all jointly continue to do the
best we can. I feel very confident about what will come in 50 years from
now, yet I feel sad not to live to experience it.


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: How analogous are categorial and material set theories?

[Jacques Carette]

Natural Transformations are homomorphisms of Functors. Working in a
dependently-typed setting, this becomes very clear. You don't even need
to go to HoTT to see this.

By this I mean that if you work 'syntactically', and figure out what it
means for a presentation of a theory X to have homomorphisms, then the
presentation of Functors qua theory has a natural (ha!) notion of
homomorphism, which turns out to be Natural Transformations 'on the nose'.

Jacques

On 2017-12-08 20:15 , Vaughan Pratt wrote:
> I prefer to think of what Steve presumably has in mind here as an
> equational theory where composition is 2-ary where 2 is not 1+1 but
> rather o--->o.
>
> One difference between equational logic and first order logic is that
> only the former has well-defined homomorphisms (not sure if Gerald Sacks
> would have agreed).?? Just as group theory (in Steve's sense) has
> homomorphisms, so does category theory in that sense have functors.
>
> I'm not sure how one argues that CT has natural transformations
> however.?? They seem to enter as part of the metatheory, which as usually
> presented seems to be pretty set theoretic in its outlook. How do NT's
> look in an HOTT account of CT?
>
> The language of the Big Bang Theory is pretty family-oriented, except
> for equality which seems somewhat controversial.?? But I digress.
>
> Vaughan
>
> On 12/07/17 10:49 PM, Steve Vickers wrote:
>> Dear Patrik,
>>
>> The theory of categories is a first order theory, so what exactly are
>> you denying here?
>>
>> Steve.
>>

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: How analogous are categorial and material set theories?

[Michael Shulman]

On Fri, Dec 8, 2017 at 5:15 PM, Vaughan Pratt <pratt@cs.stanford.edu> wrote:
> I'm not sure how one argues that CT has natural transformations
> however.?? They seem to enter as part of the metatheory, which as usually
> presented seems to be pretty set theoretic in its outlook. How do NT's
> look in an HOTT account of CT?

I'm not sure what you mean by "metatheory" here.  You can define
categories, functors, and natural transformations inside HoTT in
roughly the same way that you can inside set theory.  If you're
thinking of a "synthetic" theory of categories analogous to how HoTT
is a synthetic theory of (higher) groupoids, then that's not a very
well developed idea and there are various competing proposals (I'm
most familiar with https://arxiv.org/abs/1705.07442); but in all of
them that I know of natural transformations also arise "naturally",
generally as a sort of "directed homotopy" using a "directed equality
type" analogous to the undirected equality type of ordinary HoTT.

> The language of the Big Bang Theory is pretty family-oriented, except
> for equality which seems somewhat controversial.?? But I digress.
>
> Vaughan
>
>
> On 12/07/17 10:49 PM, Steve Vickers wrote:
>>
>> Dear Patrik,
>>
>> The theory of categories is a first order theory, so what exactly are you
>> denying here?
>>
>> Steve.
>>
>>> On 7 Dec 2017, at 18:58, peklund@cs.umu.se wrote:
>>>
>>> Is Category Theory a Theory? I think not. At least not in a logical
>>> sense.
>>>

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: How analogous are categorial and material set theories?

[Neil Barton]

Thanks to everyone for their replies. I provide some quick
clarifications to some of Patrik's comments below:

``You now introduce the word "core", and I would need to understand
what that mathematically and logically really means, at least
intuitively.''

I mean ``core'' in the trivial sense. The axioms defining what it is
to be a category (of some kind) are just first-order. The same is
true, of course, for ZFC. However, in the set theory context it seems
at least sensible to try and provide a second-order (quasi)
categoricity proof, despite the diversity of models for first-order
ZFC (and indeed we have one by the work of Zermelo, Shepherdson,
etc.). To attempt the same for category theory would seem to be an
absurd strategy---the point of categories is that they can be
instantiated in many non-isomorphic models.

``Yes, indeed, across diverse contexts, with "context" somehow related
to "system" in Hidekazu Iwaki's reply involving "mathematical
system".''

I cannot find Hidekazu Iwaki's reply (this is rather strange, I do not
know why). However it seems like similar usage to me: I don't have a
formal definition of `mathematical context', but the point is just
that there's diverse non-isomorphic models where the same categorial
properties pop up. e.g. (somewhat obviously for this list, but I found
it striking learning some category theory) the notion of topos appears
all over the place in diverse structures, and allows us to have a
reasonable notion of internal logic.

Your comments on the different notions of hierarchy are interesting,
but I will have to think about this some more before I have anything
reasonable to add.

Best Wishes,

Neil

-- 
Dr. Neil Barton
Postdoctoral Research Fellow
Kurt Gödel Research Center for Mathematical Logic
University of Vienna


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]