UP

Category Theoretic Perspectives on the Foundations of Mathematics

See also the Categories Home Page.

I don't pretend to understand what category theory has to say about the foundations of mathematics, but I would rather like to understand. To that end these notes are compiled recording my impressions, such as they are, about the why Category theorists have misgivings about classical set theory as a foundation for mathematics and what (if anything) they would like to offer in its stead.

problems
solutions
links

Problems for Category Theory in Classical Set Theoretic Foundations

Alternatives to Classical Set Theory

First a brief restatement of "the problem", which is to find some alternative to classical set theories which would fix the problems mentioned above and also touched upon in [MacLane71], Chapter I, Foundations and discussed in [Hatcher82], Chapter 8, Introduction and Sections 3 and 4.

This is still pretty much of a muddle to me and I invite comments on this material, especially from anyone who can clarify any of the approaches (preferably by means other than referral to a weighty tome which I may not have the time to read), or identify other approaches, or give links to relevant online materials.

Here I attempt a classification of the approaches of which I am aware to fixing problems in classifications perceived from the standpoint of category theory. Let me emphasise, for those of you to whom this is not obvious, that I don't understand most of this work.

I will discuss this under the following headings:

  • Non-well founded systems
  • Tinkering with classical set theory
  • Category theoretic treatment of set theory
  • Categorical Logic
  • A Universe of Functors
  • Non-well founded systems

    It is often recognised that some of the problems which category theory has with set theory are due to the restricted forms of set comprehension available. i.e. they are to do with the non-existence of things that you might wish existed (e.g. the category of all groups, the category of categories) which don't exist for exactly the same reasons that the set of all sets doesn't exist.

    It is sometimes recognised that not all set theories (among the exceptions are those of Quine) share these constraints, but I've never seen anyone suggest that a non-well founded set theory should be used, or any analysis of how well this works. (another possibility is to use some other kind of non-well-founded foundation system, such as an illative combinatory logic). Presumably when you get the universal set and such goodies you loose something else which is important (e.g. cartesian closure, though I don't know whether that is important).

    Even if you don't like this idea, you should bear in mind that insofar as the problem is these ontological weaknesses, tinkering with classical set theory but leaving it well-founded is not going to make much difference.

    That's too strong. There are two other ways of ameliorating the ontological problems. A traditional way of weakening the constraints imposed by well-foundedness is to introduce some kind of polymorphism (this is usually thought of as overcoming rigidity in type systems, but you get exactly the same problems in untyped well-founded systems, which is one of the reasons category theorists don't like classical set theory). Set theories admitting classes or universes can also help, and sometimes you get hybrids of these various approaches (e.g. dependent type theories with universes).

    Tinkering with classical set theory

    There seem to have been many variants on classical set theory proposed by category theorists or others inspired by category theory. I have to confess I havn't a clue what most of them are supposed to do.

    Let me first mention the things that do make sense to me. It is common to use a set theory with classes in preference to one without, e.g. NBG rather than ZFC (Mac Lane does this in "Categories for the Working Mathematician" [MacLane71] Notes). This leads to the distinction between small and large categories, and you find that you can have a category of all groups (say) but only of all small groups (which are sets) and it is a large category (i.e. its "hom-sets" are classes). Similarly, you get a category of all categories, but only a large category of all small categories (which isn't a member of itself). One step further is to use a set theory with a "Universe" (Mac Lane [MacLane71] also discusses use of a universe, and in Cohn's Universal Algebra a set theory is adopted in which every set is a member of a universe, giving a hierarchy of universes). These are palliative, and with them category theorists may grudgingly get by.

    One I've tried myself is the use of a polymorphic higher-order logic (I've tried this with the cambridge HOL system, and you do get to reason about the category of categories, but it isn't exactly the category you might have hoped it to be). I doubt that would appeal to a category theorist.

    There seem to have been lots of other proposals which I don't understand. Some of them are weaker than ZF, on the grounds that the strength isn't needed. Some of them are stronger (don't know why). Some of them are intuitionistic (which in itself makes no difference to strength). In the latter case the initial motivation may come from the connection between Topos theory and higher order intuitionistic logic (whose models are the toposes). As far as I am aware these proposals stick with well-founded set theories.

    Category theoretic treatment of set theory

    There seems to me to be a big difference between using set theory as a foundation for mathematics (and what kind of set theory you need to do that), and studying set theory as a subject in its own right. In terms of logical foundations, set theory is primarily about ontology, which is in turn primarily about providing a framework in which mathematics can proceed by definition, or, more liberally, by conservative extension.

    Topos theory is the platform from which category theory approaches set theory. This solves some of the problems which category theorists may have with the way in which set theory is done. However, its not clear to me whether or how this solves the problems arising from the well foundedness of classical set theory. (this isn't saying much!)

    Categorical Logic

    I put this heading in because I feel there ought to be something to be said here. But I don't really have a clue what, so its just a placeholder. (sorry)

    A Universe of Functors

    This isn't a serious proposal but a little game I played, which has some minor merit perhaps in making people think about what they mean by founding mathematics in category theory rather than set theory.

    When you found mathematics in set theory, what you do is take a universe in which there are lots of sets, and use these as the raw material in which to do mathematics. (or else you are just using them as raw material to establish the consistency of conservative extensions).

    If you ask "so what would it be like to found mathematics on categories rather than sets?" the naive answer would be "You construct a universe in which everything is a category and use that as the raw material for doing mathematics."

    Now would that be possible?

    Well I did spend some time, for reasons not connected with category theory, playing with foundational systems which are similar to set theory except that the things in the universe aren't sets. The simplest example I worked with was a theory of pure functions, which was closely analogous to set theory except that everything in the universe was a function. At one point when I was engaged in this kind of foundational innovation it occurred to me that one could just as well do it with categories. It seemed at the time that a two sorted theory involving both categories and functors would be nicest. I spent a small amount of time on this but the construction I first attempted failed (because I tried to inject some "up to isomorphism" constraint on the ontology and the universe collapsed). However I don't have the slightest doubt that it can be done, though my most recent inclinations have been to do the construction in the first instance just with functors.

    What you would get would be a foundation system equal in strength to ZFC in which the ontology was entirely category theoretic. It is instructive (if at all) only in ruling out this intepretation of category theoretic foundation, since I doubt that it would solve any of the problems which have been raised. Though it certainly would yield a foundation for mathematics as a theory of categories (or functors). I'm still curious to find how it works out.

    Some Links related to Category Theory and the Foundations of Mathematics

    Categories mailing list
    A discussion in this area may be found in the archives of the categories mailing list.

    fom (foundations of mathematics) mailing list
    A debate on "set theory versus category theory" (though that characterisation of the debate is also disputed) has raged on the FOM mailing list, and can be observed in the archives. It was certainly raging through January 1998, so you could start there or use the search on the FOM info page..

    Frederik Muller's Thesis
    There is some discussion of this topic in Friedrich Muller's doctoral thesis, an extended abstract of which is online on his homepage.

    Paul Taylor's Book Practical Foundations
    This is a substantial book available in hard copy and in various online electronic formats. It is all to do with foundations and is permeated with category theory. However, I have so far (admittedly having devoted very little time to it) been unable to interpret his position on the issues discussed on this page.

    Some books on categories and foundations.


    up home © RBJ created 1995/3/12 modified 2009/04/01