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/ ]