basic constructions:
strong axioms
further
In the context of foundations of mathematics or mathematical logic one studies formal systems – theories – that allow us to formalize much if not all of mathematics (and hence, by extension, at least aspects of mathematical fields such as fundamental physics).
There are two different attitudes to what a desirable or interesting foundation should achieve:
In proof-theoretic foundations the emphasis is on seeing which formal systems, however convoluted they may be conceptually, allow us to formalize and prove which theorems.
The archetypical such system is ZFC set theory. Other formal systems of interest here are elementary function arithmetic and second order arithmetic, because they are proof-theoretically weak, and still can derive “almost all of undergraduate mathematics” (Harrington).
In practical foundations (following a term introduced in (Taylor)) the emphasis is on conceptually natural formalizations that concentrate the essence of practice and in turn use the result to guide practice (Lawvere), as in (Eilenberg-Steenrod, Harper).
Formal systems of interest here are ETCS or flavors of type theory, which allow natural expressions for central concepts in mathematics (notably via their categorical semantics and the conceptual strength of category theory).
There are two big questions about category theory and the logical foundations of mathematics:
These questions also apply to higher category theory, which also involves the relation between them. (2-categories as a foundation for categories, for example.)
For a philosophical treatment of category theoretic foundations see foundations and philosophy.
The problem with mathematical foundations of category theory is that in category theory we frequently speak of large categories, which it is tricky to deal with rigorously in the usual sort of set theories.
One common view seems to be to found category theory on a theory of sets and classes; see the English Wikipedia's definition, for example. But the standard reference, Saunders Mac Lane's Categories for the Working Mathematician, assumes the existence of a universe (an inaccessible cardinal) instead. Both of these approaches rely on a distinction between small and large categories. There is a category of all small categories, but this category is not itself small; there is no category of all categories.
Alexander Grothendieck used more (although apparently he did not need to); he used what we now call Grothendieck universes. He assumed that every set is contained within a universe; that is, for every cardinal number $\kappa$, there is a cardinal inaccessible from $\kappa$. (This is still a rather moderate axiom, compared to some of the large-cardinal axioms studied by set theorists.) Now one has a relative notion of small and large; the category of all $U$-small categories (where $U$ is some universe) is $U$-large but must be $U'$-small for some other universe $U'$, and there exists a category (which is both $U$-large and $U'$-large) of all $U'$-small categories.
If one does not accept the axiom of choice, then there are additional complications in general category theory. In particular, one must distinguish between a universal property (for example, having all products) and having a universal structure realising that property (in the example, a functor taking each pair $(x,y)$ of objects to a specific product cone $x \leftarrow x \times y \rightarrow y$). This difficulty was overcome by Michael Makkai using anafunctors, but these have not been widely adopted, even by constructivists.
For a summary of the mathematical foundations of category theory, see Mike Shulman, Set theory for category theory, arXiv:0810.1279.
One way to think of category theory is as a framework in which the idea is formalized that every kind of equality is really secretly a choice of isomorphism or equivalence. In some sense the notion of identity is potentially evil, in a technical sense.
Michael Makkai works on a language, FOLDS (‘first-order logic with dependent sorts’), which is designed to make it impossible to formulate any evil statements.
Bill Lawvere proposed to found mathematics on ETCC (for ‘ Elementary Theory of the Category of Categories’), a first-order axiomatisation of the category of categories. This has not been very successful, but his other proposal, a first-order axiomatisation of the category of sets, works well. These and related approaches to foundations may be called structural or categorial (or categorical, which is more common but clashes with another sense of ‘categorical’ in logic).
Lawvere's system ETCS (for ‘the Elementary Theory of the Category of Sets’) essentially states that the category of sets is a topos with certain properties, in particular a well-pointed topos. This can be stated in elementary (first-order) terms; indeed, the system of axioms for ETCS in 1965 was retrospectively an important step in Lawvere’s quest to give a first-order axiomatization for the topos concept that was originally formulated in higher-order terms by the Grothendieck school, resulting in 1970 in the by the now-default notion of elementary topos that subsumes the original notion, now called Grothendieck topos, as an important special case.
It is also possible to found mathematics on the internal language of a topos. In this case, the topos need not be well-pointed (and indeed, the condition that a topos be well-pointed cannot be stated in its own internal language; or if you prefer, every topos is well-pointed internally). This is equivalent to a certain formulation of type theory, so it is (in a sense) nothing new, although it leads to new perspectives, as in the next paragraph.
Categories (not just toposes) can serve as models of type theories, each type theory corresponding to a certain class of categories. Toposes correspond directly to a constructive but impredicative type theory; to make the theory predicative (in the constructivists' sense) you generalise to a pretopos (maybe locally cartesian closed), to make the theory nonconstructive you specialise to a Boolean topos, and so on. More specifically, every category's internal language is a type theory (with many odd constants), and every type theory (of appropriate form) defines a category (its free model); this is an adjunction between categories and type theories. Paul Taylor's book Practical Foundations of Mathematics is essentially all about this subject, as is (at a more advanced level) most of the career of Michael Makkai.
Jim Lambek proposed to use the free topos as ambient world to do mathematics in. Being syntactically constructed, but universally determined, with higher-order intuitionistic type theory as internal language he saw it as a reconciliation of the three classical schools of philosophy of mathematics, namely formalism, platonism, and intuitionism. His latest views on this variant of categorical foundations can be found in (Lambek-Scott 2011).
Certain ‘strong’ axioms of set theory (those involving quantification over all sets) are difficult to state in category-theoretic (or type-theoretic) terms, but this can be overcome in a theory like ETCS; talk to Mike Shulman. (Ironically, this makes it harder to do foundations with categorial foundations!)
In contrast, many of the optional or controversial axioms of set theory (such as the axiom of choice) can be stated quite directly in ETCS. These can be examined quite well in a naïve set-theoretic language that never need be precise about whether one's foundations are traditional (membership-based), categorial, or whatever.
Relevant topics: ETCC, FOLDS, homotopy type theory
A big picture intro to the comparison between set theory, type theory and topos/category theory as approaches to foundations is in
It may seem on first sight that foundational questions in mathematics are remote from “real mathematics”. This is not quite so. For a list of “real world” problems that do depend on foundations see
L. A. Harrington (ed.), Harvey Friedman’s Research on the Foundations of Mathematics, Studies in Logic and the Foundations of Mathematics (2012)
William Lawvere, Foundations and applications: axiomatization and education, Bulletin of Symbolic Logic 9 (2003), 213-224 (ps, Euclid)
Practical foundations in terms of type theory language are laid out in
Under computational trinitarianism this corresponds to a practical foundation in programming, laid out in
A foundation for algebraic topology in this practical spirit is laid out in
The following contains a careful discussion of Gödel's incompleteness theorem in the context of categorical foundations using the free topos:
A comparative discussion of complexities of different foundations is in
Freek Wiedijk, Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics (pdf)
Abstract This paper presents Automath encodings (which also are valid in LF/P) of various kinds of foundations of mathematics. Then it compares these encodings according to their size, to find out which foundation is the simplest.
The systems analyzed in this way are two kinds of set theory (ZFC and NF), two systems based on Church’s higher order logic (Isabelle/Pure and HOL), three kinds of type theory (the calculus of constructions, Luo’s extended calculus of constructions, and Martin-Löf predicative type theory) and one foundation based on category theory. The conclusions of this paper are that the simplest system is type theory (the calculus of constructions) but that type theories that know about serious mathematics are not simple at all. Set theory is one of the simpler systems too. Higher order logic is the simplest if one looks at the number of concepts (twenty-five) needed to explain the system. On the other side of the scale, category theory is relatively complex, as is Martin-Löf’s type theory.
Colin Mclarty, Set theory for Grothendieck’s number theory, pdf
Some old discussions from this page archived here