The Foundations of Mathematics

This article examines what is meant by ‘foundation’ in different contexts, and it focuses on four prominent mathematical theories, each of which have been claimed to play some kind of foundational role. Emphasising different features which might be desired from a foundation has led to a variety of different proposals. For this reason, in order to make sense of the claims made by advocates of a given theory, it can be helpful to initially get clear on what exactly they hope to achieve by providing a foundation in the first place — what job is their preferred theory supposed to do? When we ask this question, it quickly becomes clear that different thinkers often have different goals in mind for their proposals, and as a result, there is disagreement among philosophers of mathematics not only with regard to which theory ought to be accepted as foundational, but also disagreement concerning what the criteria for a foundation ought to be.

Ultimately, when it comes to the question ‘what is or ought to be the foundation for mathematics?’ there seem to be three solid answers — set theory, category theory, and type theory. But without a better understanding of the terms ‘is’, ‘ought’, ‘the’, ‘foundation’, and ‘mathematics’ it is unclear how these theories provide an answer. As Stewart Shapiro quipped, it is like a game of Jeopardy: If these are the answers, then what is the question?

Introduction
What is a Foundation?
Set Theory
1. The Case for Set Theory
2. Questions and Debate
  1. Independence and Axioms
  2. Universes and Multiverses
Category Theory
Type Theory
Univalence and Homotopy
Conclusion
Refereces and Further Reading

1. Introduction

The foundations of mathematics is a broad topic with deep interconnections to many areas of philosophy, mathematics, linguistics, and computer science. Historically speaking, research into foundations can be divided broadly into three phases. The first begins in the late 19th century, accompanying the process of rigourisation, undertaken by notable figures such as Richard Dedekind and Karl Weierstrass. Alongside the rejection of a reliance on geometry, this phase is marked by the development of formal symbolic logic from Boole (1847) and Frege (1879); the discovery of different sizes of infinite collections and development of naive set theory by Cantor (1891), and the work into the rigourisation of analysis by Dedekind (for example Dedeking (1872)). The second phase began in the early twentieth century, sometime around 1930, and was marked by a number of limitative results in mathematical logic. Notably, the completeness and incompleteness theorems of Gödel (1931), the study of truth in a formalised language and the Undefinability Theorem of Tarski (for example Tarski (1931)), and the impossibility of an algorithm for deciding the validity of a given statement of mathematics due to Church (1936) and Turing (1936) . The third phase is arguably still ongoing, and has been marked by the exploration of new and exciting mathematical theories, such as the algebraic development of category theory, and attempts to explore the depth of the limitative results established in phase two. Readers interested in more information regarding the history of foundational research are urged to consult Mostowski (1965), Wang (1958), Sommaruga (2011).

This article distinguishes between Foundations of mathematics, and Philosophies of mathematics. For our purposes, foundations of mathematics are formal mathematical theories or branches of mathematics purporting to play a foundational role for the whole discipline (in some specified sense). On the other hand, philosophies of mathematics are understood as philosophical theories of mathematics (For an overview of the latter see Shapiro (2001)). Unfortunately, this distinction between foundational and philosophical theories is, as we shall see, not as cleanly delineated as one might hope. Nevertheless, it can be gestured towards by noting that whatever one embraces foundationally need not entail a particular philosophical perspective. That is, any of the candidate foundational theories we will be discussing can be understood according to any given philosophical view. For example, a set theoretic foundationalist can equally be a platonist or a nominalist. Advocates of category-theoretic foundations can coherently embrace structuralism or formalism as their fundamental philosophy. While these views might inform each other, they do not strictly speaking entail one another. Although these philosophical accounts of mathematics are undeniably fascinating, our focus will be on the theories themselves which purport to play a foundational role for mathematics.

Section 2 begins with a discussion of the notion of foundation itself. The goal is to clarify what role foundational theories are supposed to play in mathematics, and the different ways in which the notion of foundation can be understood. The ways in which mathematicians and philosophers use the term are sometimes divergent, and that this can potentially create misleading discussion.

Later sections discuss particular candidate theories which are often claimed to play a foundational role. We first discuss set-theoretic foundations (in section 3), before exploring the category-theoretic proposal (section 4), then turning to the more syntactic approach of type theory (section 5), and finally the relatively new proposal of univalent foundations (section 6). This is followed by a survey some of the distinctive features and claims put forth by each theory in order to establish their case as a/the foundation, and to introduce some of the debates between them. The purpose of this article is to provide an accessible introduction to the topic of foundations alongside some of the primary debates within this field, and to guide interested readers towards more specific literature where appropriate. As such, any form of adjudication in these debates will be beyond the scope of the present article.

2. What is a Foundation?

Here are two initial questions. What is a foundation? What does it mean for a mathematical theory to provide a foundation or play a foundational role for mathematics? As it turns out, these are surprisingly tricky questions to answer. Indeed, the wider literature shows advocates of various positions passionately arguing the case for their preferred theory. As such, one might be forgiven for thinking that the issue of what a foundation is and what it is supposed to do had been settled long ago.

Mathematicians sometimes talk of foundational theories as providing a framework for interpreting mathematical terms, or a language of sufficiently strong expressive power so as to capture a significant amount of mathematics within a single theoretical framework. Indeed, as we will see, there are some who think there is nothing more to the concept of a foundation than this (but that is hardly an uncontroversial claim). However, if a formal framework is all that is meant by the term ‘foundation’, it would be highly surprising to have found such lively philosophical debate. All parties in the discussion should agree that the variously proposed foundational theories meet this minimal desideratum. One can reconstruct most of mathematics in terms of either sets or categories, both are capable of recasting mathematical discourse within their proposed vocabulary. Why then do we see such vehement disagreement? It seems that in order for the notion of foundation to give rise to the substantial debate that it has, at least some theorists must take something else to be involved in the concept of ‘foundation’.

Unfortunately, exactly what this ‘something else’ is, is rather unclear. Philosophers discussing foundations have put forth many different conditions which a theory must meet in order to be successfully regarded as a/the foundation. A foundation for mathematics in this philosophical sense is supposed to provide not only a language for the interpretation of mathematical terms, but also some sort of pre-theoretical, conceptual, or even epistemological basis for mathematics which can be formulated in isolation without appeals to other foundations. However, there is little agreement about which (if any) of these are necessary.

This has led to a situation where although proponents of each candidate confidently put forth the case for their preferred foundational theory, it is not clear whether they are all operating with the same understanding of the term ‘foundation’. Perhaps then there is no disagreement at all, and the advocates of each theory are simply taking the term ‘foundation’ to have different meanings. In this section, we will examine some different proposals for what the criteria for a foundation should be, and what the philosophical nature of a foundation amounts to.

a. Metaphysics?

The first sense in which one might understand the term ‘foundation’ is as a metaphysical claim. In the broadest sense, the proposed foundational theory would describe the fundamental objects of mathematics as a whole. Interpreted this way, the set-theoretic advocate claims that all mathematical objects are sets, the category-theorist claims that all objects are categories or morphisms in categories, and so on. An obvious caveat to this discussion is that to understand the claim in this robustly metaphysical sense, one must accept that there are mathematical objects. Such a commitment could presumably be done away with via nominalistic paraphrase; to make overtly metaphysical statements into something like ‘if there were mathematical objects they would be reducible to sets’. However, although this is possible, it’s not clear why such an anti-realist would bother to engage with the metaphysical conception of a foundation in the first place, so for the time being we can set that aside.

In the most robust sense then, metaphysical foundations are understood as a claim regarding the ultimate subject matter of mathematics, and the underlying nature of the objects studied by mathematicians. As such, we can understand this position as a descriptive thesis: the foundations of mathematics tell us what there is at the most basic level. Accordingly then, while it might look like there are numbers, points, planes, functions, spaces, rings, and so forth.: this is a mere illusion. At the most basic level there are only the objects provided for by the foundational theory. Such a view can thus be understood as a part of classical metaphysics, trying to get at the ‘essence’ of mathematics.

It should be unsurprising that this reading is controversial, not least given the aversion to metaphysics displayed by many mathematicians. There are obvious questions to be asked: why is the philosopher uniquely positioned to uncover the nature of reality, and what would count as evidence in favour of one proposed foundation ahead of a rival? After all, mathematics is not like physics where one can postulate entities then seek experiments to confirm or refute the hypothesis of their existence. How then would we decide whether the fundamental nature of mathematical reality is set-theoretic or category-theoretic?

These concerns over foundations have led to profound debates concerning realism more generally. Of particular note are Benacerraf (1965), and Benacerraf (1973). The first of these concerns a question of adjudication; if there were a unique metaphysical foundation for mathematical objects in the sense we have been discussing, it could be represented equally well in a multitude of different ways. For example, the natural numbers could be represented set-theoretically with the Von-Neumann ordinals, or the Zermelo ordinals (or indeed, any -sequence since the appropriate characteristics can be induced via the push-through construction (see Button & Walsh (2018) pp. 35-44)); and so there is nothing in mathematics to determine what the ‘true’ reduction might be. The second paper concerns knowledge and reference. If the foundation is robustly metaphysical as described, then these objects really do exist and account for mathematical practice. But if that is so, they must have a fundamentally different character than anything in our physical universe; so, the question becomes: how could we possibly know about them or refer to them? As such, the claims of foundational theories providing ultimate metaphysical grounding for mathematics are hotly contested.

i. Ontology?

Although the robust conception is a natural starting point, it is not the only sense in which one can understand a metaphysical foundation for mathematics. Instead of the descriptive claims made above, one might instead motivate a metaphysical account of foundations as a more holistic proposal. According to this kind of picture, when we look at mathematics we see what appears to be a rather piecemeal endeavour. There are functions, groups, natural numbers, complex numbers, morphisms, spaces and so much more. These, on the face of it, seem to have nothing at all in common. The ontological proposal is to unify these seemingly disparate areas of mathematics under a single banner.

Such a proposal can be motivated by considerations of ontological parsimony: instead of viewing algebraic, analytic, geometric, or topological objects as sui generis entities, we should instead view them all as special kinds of sets (or categories, and so forth). Such an account is more taxonomical than it is robustly metaphysical. Instead of committing to the many varieties of mathematical objects which mathematicians study, one can instead be committed only to the objects provided by the foundational theory, and thus view the apparent diversity of mathematical objects as merely different species within the same genus.

Note that this is not the same as the descriptive thesis offered above. In this instance, the ontologist is not trying to get at the fundamental nature of the objects in question. Rather, they find themselves looking at a discipline littered with existential claims, and perhaps wishing to ‘trim the fat’ find the minimal number of objects which they must be committed to in order to account for the activities of this discipline. Of course, as we will see in later sections, there are a number of ways in which one might go about such a project, and indeed there need not be a single unique method for achieving this goal. What all such approaches have in common however, is the conviction that our philosophical understanding of mathematics would be (in some sense) better if the underlying ontology were unified into a single foundational theory, and we need not accept any more than that.

However one interprets the metaphysical reading of a foundation, we see that it takes the term ‘foundation’ seriously, as providing a bottom-up account of mathematics and its objects. Awodey (2004) summarises the situation nicely. On the metaphysical understanding of foundations, one seeks to build up the objects of mathematics within a particular foundational system such that two criteria are met:

(1) There are enough objects to represent the various kinds of numbers, spaces, groups, and so forth. of everyday mathematics and

(2) There are enough laws, rules, and axioms to warrant all of the usual inferences and arguments made in mathematics about these things, as well as at least some of the most obvious ‘rounding off’ statements dealing with features of the system itself… (Awodey (2004), pp.55-56).

In sum, the metaphysical approach seeks to understand the proposed foundation as providing the objects of mathematics. The foundation provides the criteria for mathematical existence claims and the corresponding commitments they entail. This can be understood in either a stronger or weaker sense, but either way it understands the foundation as either specifying or providing the kinds of objects with which mathematics is fundamentally concerned.

b. Epistemology?

Another way of conceiving of foundations concerns epistemology. According to this conception, the role played by the foundational theory is to vouchsafe our mathematical knowledge. This is somewhat familiar when one considers the classical axiomatic approach to mathematics; one begins with a list of obvious truths which are taken as self-evident, and then via a series of agreed upon inference manoeuvres, one derives theorems from these axioms. As such, when the process runs smoothly, we are justified in our mathematical conclusions since we arrived at them from obvious truths via truth preserving inferences.

A particularly strong version of this idea is that one lacks genuine mathematical knowledge unless they have derived it directly from the proposed foundational theory themselves. Presumably, no one holds such an extreme position. Clearly there was mathematical knowledge prior to the implementation of foundational theories in mathematics. Gauss, Euler, and Euclid surely knew mathematical propositions if anyone ever did, despite the fact that set theory, category theory and so forth. had not been invented yet. Indeed, the practising mathematician in say algebraic topology surely counts as having mathematical knowledge, even if she finds questions of foundations thoroughly uninteresting.

As such, we should be careful when seeking to articulate epistemic foundationalism. Shapiro (2011) p.101, delineates possible epistemic conceptions of foundation along three lines: Mathematical, Logico-Cartesian, and Knowledge of Sources.

i. Mathematical

According to mathematical epistemic foundationalism, the goal of a foundational theory is to prove as much as possible. The spirit of this approach is perhaps best exemplified by Frege’s claim that whatever admits of proof ought to be proved. This style of foundationalism asserts that no propositions should be taken for granted. For example, in the case of elementary arithmetic if even simple propositions like ‘2+2=4’ are derivable from the foundational theory, then they should be so derived. This simple example may seem merely pedantic, so for a case with more substantial insight, consider the principle of induction. Recall that mathematical induction is a technique used to establish a general statement about some possibly infinite collection of objects (such as natural numbers). Usually, induction is taken as an axiom, and as such is never proven. However once we explore the theory of arithmetic within the context of our foundational theory (for example ZFC) we learn that the equivalent set-theoretic principle can actually be derived. This, presumably, provides some sort of epistemic gain: rather than take the principle for granted, we have derived it from something more fundamental.

It’s interesting to note that if this is taken to be the relevant sense of foundation, then it’s not at all obvious that there must be a single unique foundation. After all, it’s commonplace in mathematics for a theorem to admit of several proofs. Indeed, multiple proofs of the same result are often taken to grant greater insight into the result in question, allowing mathematicians to examine the result in a variety of different ways (this connects to debates concerning ‘purity’ in mathematics, see for example Detlefsen & Arana (2011) ). As such, since various set theories as well as category theory and HoTT all establish induction, one may well conclude that there is no need to choose between them, they are all simply different lenses through which we can view mathematical results.

ii. Logico-Cartesian

The second epistemic conception of foundation takes inspiration from Cartesian first-philosophy. In order to secure mathematical knowledge from skeptical doubt, we must ensure that our mathematical truths are as self-evident, certain, and clear as can be. If any mathematical proposition is in doubt, then according to this view we should investigate what our foundational theory has to say about it. In this sense, our foundation helps prevent doubts from creeping into mathematical practice. If our foundational theory is epistemically pristine, then it will alleviate any skeptical worry.

This appears to have been a dominant motivation throughout the history of mathematics, and indeed has arguably continued to play a prominent role in debates throughout the twentieth century (for example, in trying to decide the continuum hypothesis on the basis of ‘natural’ extensions of ZFC (Gödel (1947) ). This might seem to be quite an attractive proposal, if we can indeed supply a foundational theory consisting of only obvious self-evident propositions. Unfortunately however, it seems that in practice this is easier said than done. For one thing, what counts as self-evident to one mathematician is not necessarily self-evident to another. We can see this clearly when considering the historical controversies regarding the axiom of choice (for details see Moore (1982) ). Although some mathematicians viewed this principle as intuitive, others rejected it since it does not actually give a procedure for generating the relevant choice principle. Moreover, the situation is further complicated when one considers the logically equivalent principles (such as the principle of well-ordering) which many find to be intuitively false.

In addition to these concerns, as is noted by Shapiro (2004), when we consider the axioms of foundational theories they rarely appear more self-evident than those of the mathematics they are said to ground. Suppose that we’re faced with a skeptic who genuinely doubts the truth of the Peano axioms or some elementary propositions of arithmetic. It does not seem likely that this person’s skepticism will be alleviated upon being presented with the ZFC axioms and a derivation of the result in question from ZFC instead. Often times, the foundational theories being considered require a high degree of mathematical sophistication, and are certainly less obvious than propositions of elementary arithmetic.

This fact is further reinforced when one considers the activities of foundationalists. As far as we can tell, no one has developed a candidate foundation on the grounds that it is more self-evident and thus immune to skepticism. Lawvere for example did not propose category-theoretic foundations so as to alleviate skeptical concerns about elementary arithmetic, nor do the present day category theorists argue for their preferred theory on these grounds. Therefore, it is unlikely that any foundational theory can legitimately assuage skeptical doubts one might have about basic mathematics.

iii. Knowledge of Sources

The third and final epistemic approach we will consider concerns the philosophical status of mathematical knowledge. According to this proposal, if we are able to identify our foundational theory, and recast existing mathematics within the framework it provides, we will be able to better discern the epistemological character of mathematics. For example whether mathematical knowledge is fundamentally analytic or synthetic (in the Kantian sense), apriori or aposteriori and so forth. On this view, the fact that we have mathematical knowledge is uncontroversial. What the foundation seeks to provide is a characterisation of that knowledge. By recasting things within the foundational framework we see what-grounds-what, and thereby come to get a better understanding of the epistemic status of the propositions in question. This might be an attractive picture, but once again it’s difficult to square alongside actual foundational research. The prospects for gaining insight into the fundamental nature of mathematical knowledge via sets, categories, or types seems unlikely.

According to all three epistemic-foundationalist proposals then, it is the purpose of a foundation for mathematics to provide some sort of ultimate justification for mathematical knowledge. The foundation should provide some basic principles which in some sense ground or explain the epistemological character of mathematics. Again, it seems like few contemporary figures advocate a proposal along these lines. What’s more, it’s unclear whether the epistemic pedigree of a proposition is philosophically relevant. For most of us, we have come to believe the axioms of a given mathematical theory such as arithmetic or geometry without a lengthy detour through foundational definitions.

c. Criteria or Desiderata?

Perhaps the issue with the previous approaches is that they’ve sought to emphasise purely philosophical aspects of a foundation. Whether a foundational theory can give the basic objects or explain the epistemological character of mathematics are not properly mathematical issues. As debates have progressed over the last century or so, these traditional philosophical criteria have been somewhat displaced in favour of mathematical considerations. That is, rather than seek a criterion for the nature of a foundation itself, most contemporary approaches instead aim to provide desiderata for foundational theories. The relevant community seeks ways to evaluate different proposals in terms of one another, without appeal to the ultimate philosophical nature of a foundation. The material discussed in this section will be of recurring significance for later sections concerning specific foundational proposals.

i. A Mathematico-Linguistic Phenomena?

To get a handle on what these desiderata might be, we need to turn our attention from philosophical to mathematical considerations. This does come with some caveats however. After all, one could argue that settling the above ontological and epistemological questions would be of great mathematical benefit. One could also be too flat footed in articulating mathematical benefits, and thus declare the best foundation to be simply whichever theory has the largest sheer volume of theorems proven. Neither of these are what is typically intended when discussing the mathematical benefits of a foundational theory. Instead, what is often meant is that the foundational theory provides an arena for mathematical discourse, which allows one to study and compare a variety of different objects in one unified way (this will be discussed at length in 2.1).

A fairly standard articulation of these ideas can be found in Moschovakis (1994) who begins by considering the relationship between synthetic and analytic geometry.

A typical example of the method we will adopt is the “identification” of the (directed) geometric line with the set of real numbers via the correspondence which “identifies” each point… with its coordinate. What is the precise meaning of this “identification”? Certainly not that points are real numbers. … What we mean by the “identification” of with is that the correspondence… gives a faithful representation of in which allows us to give arithmetic definitions for all the useful geometric notions and to study the mathematical properties of as if points were real numbers (Moschovakis, 1994, pp.33-34, emphasis original).

Moschovakis’ claim then, is that by studying a mathematical object or structure of one kind as if it were of another kind, we can gain greater knowledge and insight as to its nature. Just as with the development of analytic geometry, which provides an understanding of geometric objects such as points and lines in terms of real numbers, so too the goal of a foundation for mathematics is to isolate the mathematically relevant features of an object, and find a surrogate within the foundational framework which exhibits those same features. In the case of set-theoretic foundations Moschovakis goes on to remark:

In the same way, we will discover within the universe of sets faithful representations of all the mathematical objects we need, and we will study set theory… as if all mathematical objects were sets. The delicate problem in specific cases is to formulate precisely the correct definition of a “faithful representation” and to prove that one such exists.

The key to this conception of foundations is to provide a theory which yields a variety of surrogate objects which faithfully represent the mathematically relevant features of the original object within the foundational theory (something which Maddy (2016) calls ‘generous arena’ – see 2.1). The foundation does not provide an ontological reduction. Mathematical objects are not identified with their foundational counterparts, nor will the foundation (typically) provide useful insight for proving theorems within the respective branches of mathematics. Rather, it is the surrogacy relation which is foundationally significant on this picture. By adopting a foundational theory, one seeks to offer surrogates for all objects and structures studied by mathematicians and thus ground mathematical discourse in a single unified arena such that the relationships between the different structures and objects can be precisely studied.

It should also be noted that this view has some interesting implications for questions of existence and proof. If this conception of foundation is agreed upon, then questions of which mathematical objects should be countenanced as legitimate are settled by whether or not they have a surrogate, that is whether a proof of satisfiability for the object/structure in question follows from the foundational framework.

Although this approach is appealing and is arguably the most prominent view discussed in this section, it is worth pausing to ask some questions concerning the surrogacy relation. It should be puzzling to a philosopher just why it is that mathematics benefits so much from finding surrogate objects. Why is it that insights about say, geometry can be gained by studying representations of objects rather than the objects themselves? What does the importance of surrogacy mean for studying those mathematical objects directly? Mathematics seems particularly special in this regard. While it is true that in physical sciences, models of the phenomena under investigation are often utilised, the practice is more direct than the surrogacy relation invoked here. Shapiro (2004) makes this point arguing that in no other science do we see the same methodology employed; biologists do not hope to gain insight into the function of an organ by finding a surrogate for it, psychologists do not seek to settle questions of the existence of a given psychological mechanism by finding a faithful representation of it (Shapiro (2004) p.32). Why then does this seem so important for mathematics? Answers to these questions are not at all obvious and take us beyond the bounds of the present article, but are certainly important considerations for anyone advocating this style of view.

ii. Frameworks

The surrogacy relation might provide a useful way of understanding foundations in purely mathematical terms, but even this is a fairly substantial proposal. To understand the next proposal we will introduce a distinction between a ‘foundation’ and a ‘framework’. The aim is to capture those more substantive proposals with the former, and weaker notions with the latter. Whereas foundations imply some more robust philosophical conception, frameworks provide a unifying language and conceptual apparatus for mathematics. This weaker notion is mathematically motivated, and often provides a way of interpreting particular mathematical propositions in terms of the framework. According to some theorists, this latter notion of a framework is all that is really required.

A paradigmatic example of this perspective is Awodey (2004), according to which, what is fundamental to mathematics is the following conditional:

if such-and-such is the case, then so-and-so holds (Awodey, 2004, p.58).

According to Awodey this is the schematic form of every mathematical theorem. For example, if a natural number is prime, then it is only divisible by itself and one. Or, for a less trivial example, in any group G, if it has a normal subgroup N then for every element g of G, gNg^-1 = N (of course the converse also holds, and thus this is a biconditional implication). According to Awodey, this type of conditional statement is fundamental to mathematics, and it should be the job of a foundation to capture as many of them as possible. Thus, for this style of view the purpose of a foundational theory is to provide a linguistic framework in which these conditionals can be formulated and stated.

Clearly, this view is reminiscent of traditional ‘if-thenism’, however Awodey is careful to distinguish his view by emphasising that the parameters occurring in the conditional should not be understood as implicitly bound variables. There is no domain presupposed. To make this explicit in the context of the above example, while traditionally the statement ‘in any group’ would seem to presuppose a universe of all groups (be they sets, categories, types, and so forth.) Awodey instead claims that the conditional should be understood purely schematically, and thus we can say that the theorem in question holds without even implicitly appealing to a domain of all groups. This, Awodey calls the ‘top down’ approach to foundations, where what really matters for foundational purposes is not some realm of objects, but rather a general framework of conditions where the mathematician can study various systems which meet these conditions. The role of a foundational theory on this picture, is to specify what we use as meta-variables for the ‘such-and-such’s and ‘so-and-so’s in the conditional.

Crucially, the only role for the foundational theory on this approach is to provide a linguistic framework. The theory should provide a language for mathematics, but in particular one wherein these schematic conditionals can be formulated with sufficient generality.

As one would expect, this is a contentious claim. Indeed, whether or not mathematics has such a schematic character is disputed (see for instance Shapiro (2005)). That said, Awodey is not alone in understanding the role of a foundational theory in this weaker sense – as a framework, language, or conceptual scaffolding for mathematics. Shapiro (1991) similarly advocates a weaker notion of ‘foundation’, rejecting so-called ‘foundationalism’ in favour of the idea that all that is required is a unified linguistic framework for mathematics (in his case this framework is a second-order logic).

Here then we see another complication arising: how robust a notion should we require ‘foundation’ to be? It is fair to say that all exigent views in the literature have adequate grounds for asserting themselves as a foundation in the weaker sense. As we will see below, set theory, category theory, and type theory all provide a unified linguistic framework within which one can interpret at the very least a substantial amount of mathematics. However, as the preceding sections have made clear, often when discussions concerning foundations occur, they do so with a much more substantial conception of ‘foundation’ in mind. Getting clear on exactly what these desiderata are, or ought to be, is half the battle, before one even broaches the further question of whether a given theory meets the proposed requirement.

As already noted, one might expect the foundational theory to provide an account of the basic objects of mathematics, and how it is that we might come to know them. One might expect a semantic account of how it is that the theoretical terms of the foundational framework ought to be understood. One might further insist that the purported foundation should supply a unified methodology for mathematical practice. A number of questions can be asked about each of these conceptions of foundation, and in this article we have only scratched the surface (interested readers can consult sources such as section 2 of Ladyman & Presnell (2018) for more on this). However we can note that the way in which one seeks to address any of these questions has important bearing on the prospects for answering the others. For example, if one furnishes mathematics with a robust ontology, it seems justifiable to require also an epistemological explanation of how it is that we can know about or refer to these objects (the so-called ‘Benacerraf dilemma’). As a result, the explanation is further complicated. Not only do we have to specify desiderata for a foundational theory of mathematics, but we must also be aware of how by meeting one putative requirement, we can affect others we may also be seeking.

It does not seem reasonable to insist that any candidate foundation must be able to answer every such philosophical question posed concerning its purported ontology, epistemology, semantics, or methodology. Indeed it would be entirely unreasonable to maintain that in order for a mathematical theory to claim the mantle of ‘foundation’ it must settle all disputes in the philosophy of mathematics. Nevertheless, it should be clear that even more modest tasks still provide a substantial theoretical challenge.

iii. Independence and Autonomy

Outside of linguistic frameworks and surrogacy relations, a consideration that has often been taken as important concerns whether a candidate theory can be properly regarded as independent of any other. This is seen as an important way to judge the suitability of a proposal relative to others since intuitively, a proposed foundation should not itself rest upon anything else. If the proposed foundation does require some further theory in order to successfully serve its purpose, then it surely seems that the latter theory is more deserving of the title ‘foundation’. In essence, for a theory to be truly foundational, it should not rely on any other. Therefore, one way to judge the suitability of a foundational proposal relative to others is whether or not it stands on its own two feet. That is, whether or not it is autonomous (This criterion was first introduced by Feferman (1980), and was significantly developed by Linnebo & Pettigrew (2011), and Ladyman & Presnell (2018)).

Intuitively, for a proposed foundation to be autonomous means that it should not itself rely upon some other antecedent piece of mathematics. Although this gloss is relatively straightforward, we require more for a philosophically useful criteria. One way to do this is (following Linnebo & Pettigrew (2011) ) to mark a distinction between logical, conceptual, and justificatory autonomy. Say that a theory is logically autonomous if it is possible to formulate that theory without appealing to notions from any other theory. This is a useful but rather weak criteria requiring that in order for a theory to properly count as foundational, it must rely only upon pre-mathematical ideas. Of course, the difficulty with such a criterion is what counts as sufficiently ‘pre-mathematical’. Often, the intuition of mathematicians working in these areas diverges significantly from those of the layperson. Moreover, in the other direction, certain basic principles such as counting are arguably part of mathematics proper and thus fail to be pre-mathematical. Part of the difficulty with specifying an autonomous foundation in this sense is delineating precisely what is acceptable for the theoretician to take for granted in their theory. A second specification is via conceptual autonomy. A theory is conceptually autonomous if it is possible to grasp the concepts involved in that theory without prior grasp of concepts from another theory. For example, field theory is not conceptually autonomous, since fields are defined to be commutative division rings, and so a prerequisite grasp of some concepts from elementary ring theory is required in order to study fields. Finally, we might say that a theory possesses justificatory autonomy if it is possible to motivate and justify its claims without further appeal to another theory. As we will see later, many of the recent discussions concerning alternatives to set theory concern precisely this issue of whether they can be regarded as properly autonomous, and if so, in what regard.

iv. A Standard of Proof?

Mathematics is a proof-based activity. In order to demonstrate the truth of some mathematical proposition, one proceeds by deriving it (either formally or informally) from some assumptions (axioms) via a process of agreed upon steps (inferences). One further desideratum for a prospective foundation then might be to codify and consolidate the standards of proof for the discipline of mathematics as a whole. On this picture, foundations provide a shared standard for what count as legitimate proofs across seemingly disparate branches of mathematics.

A theory capable of capturing all existing mathematics and codifying the inferences and proof procedures would guarantee the compatibility of differing areas of mathematics. If for example, algebra, analysis, and topology were each founded separately, there should be no prima facie guarantee that their results and methods be compatible with one another. Moreover, it would also prove difficult to explain the fruitful cross-pollination of techniques and ideas across seemingly unrelated branches of mathematics. To avoid this, it might be hoped that a foundational theory would unify these potentially disparate branches and provide a single unambiguous standard for proof.

Another proof-centered consideration which has started to come to the fore more recently concerns the use of assistive technology for mathematics (as exemplified by Buzzard (2024) among others). In recent years, automated theorem provers (ATPs) and interactive theorem provers (ITPs) – systems which can be ‘told’ the axioms of a theory and have a language rich enough to express its theorems – have come to hold a more significant place in mathematical discourse. This being so, a new perspective on foundational issues has begun to emerge: effective computability. What this means is that we should desire a foundation for mathematics which lends itself to implementation in some kind of ATP or ITP like Lean or Rocq. If the axioms of a proposed foundational theory can be implemented by such systems, then the process of discovering and verifying complex proofs could be made not only faster but more secure for having been run through a computer. In more traditional foundational proposals (those that predate the development of such systems) this property is understandably either absent or somewhat difficult to fully implement. As a result, effective computability is sometimes wielded as a trump card for newer proposals (as will be discussed in detail later). For the time being however, the community remains somewhat split over the importance of formalisability.

v. Foundational Desiderata

Unlike the metaphysical and epistemological criteria discussed in 1.1 and 1.2, the proposals considered in this section are much more reflective of contemporary foundational debates as they occur in mathematics. As we will see in later sections, questions of metaphysics, epistemology, and indeed the philosophical nature of a foundation have become largely superseded by how it is that we might evaluate one foundational proposal relative to another. This gives the questions discussed in this section further importance. In particular, questions concerning faithful representation, unification of mathematics, and autonomy have become central.

d. Do We Even Need a Foundation?

Perhaps in reading the above, and considering the disagreements in the literature, one forms the conclusion that all of this discussion is thoroughly wrong-headed. If we do not care for matters of metaphysics, epistemology, or what have you, why tolerate such debate? Indeed, in light of this, the conclusion drawn by some is that mathematics neither has nor needs a foundation at all. These so-called ‘anti-foundationalist’ views are, unsurprisingly, about as disunified as their foundationalist counterparts. On some readings, Awodey (1996), Baldwin (2018), and Shapiro (1991) all count as anti-foundational, in the sense that they each explicitly reject some robust notion of foundation. However, it does not seem right to count these figures as anti-foundationalist in the strongest sense, since they all subscribe to the weaker notion of a framework for mathematics (though of course they disagree on precisely what that framework is).

Closer to an outright rejection of foundations is Putnam (1967). Putnam claims that mathematics need not fear any so-called ‘foundational crisis’, and is in no need of philosophical rescue. In doing so, he rejects the idea that any theory has a unique privileged claim to be the foundation for mathematics. On this style of view, the various candidate theories are equivalent descriptions and as such foundational disputes should cease to be taken as important to philosophers of mathematics (see Putnam (1967), and Burgess (2018)).

Another anti-foundationalist view can arguably be found in Mayberry (1994). Though he claims explicitly that ‘mathematics not only needs, but in fact has, foundations.’ The way in which he conceives of a foundation is radically different and far more informal than is typically assented to. On Mayberry’s view, the foundations of mathematics concerns an Aristotelian conception of logic. These foundations are the tools, techniques and conventions adhered to by mathematicians in conducting their work, and are importantly not to be identified with any formal theory. Instead, on this view, the foundation for mathematics is simply the set of pre-theoretical concepts involved in the practice of doing mathematics, as well as the rules for deriving mathematical conclusions from premises. Indeed, Mayberry goes as far as to assert of set-theoretic and category-theoretic foundations:

Neither of these formal theories is of any use at all as a foundation for mathematics. The idea that any first-order theory could fulfill that role is simply incoherent. Indeed, no axiomatic theory, formal or informal, of first or of higher order, can logically play a foundational role in mathematics (Mayberry, (1994) p.34).

Hence, although Mayberry himself does propose an informal (and particularly idiosyncratic) view of foundations, his outright rejection of formal theories playing a foundational role suffices for our purposes to count him as an anti-foundationalist.

Of course, there are other ways that one may eschew foundationalism, but working out the details of such proposals in a way that acknowledges the relevant mathematical research is often much more difficult than it may seem.

e. Can There Be More Than One Foundation?

Perhaps, rather than reject the idea of a foundation altogether, one may come to reject the common presupposition that a foundation must be unique. In doing so, one embraces a kind of foundational pluralism according to which mathematics either can or does have foundations, but the idea that this must be only one is rejected.

Given the foregoing discussion, one of the most natural ways to motivate foundational pluralism is by noting the different ways that one can understand the term ‘foundation’. One may think that each position is in some sense legitimate. Perhaps each of the purported foundations is indeed playing a foundational role as claimed, and the debates can be simply dissolved by rejecting the presupposition that there can only be a single foundation. Perhaps one agrees that set-theoretic surrogates provide a useful unified arena of discourse, but think that the semantics of category theory provide a more useful language for actual mathematical practice. Any combination of theories can thus be introduced to play the relevant foundational role. To borrow a phrase, ‘let a thousand flowers bloom’.

This seems to be an appealing idea to at least some contemporary philosophers of mathematics (for example, Shapiro (2004), Dzamonja (2019)), and is arguably growing in popularity. However, it is nonetheless fair to say that at the time of writing the majority of foundational discussion still maintains a strongly monistic tone. For one thing, one might reject the idea that foundations are as multifaceted as discussed above. If there is but one desideratum which ultimately matters, why accept other theories serving ancillary roles? For another, if we allow there to be multiple foundations there are concerns that grounding different areas of mathematics in different foundational theories may lead to a fragmentation within the discipline or even contradictions. Ultimately, if one is engaged with foundational issues because one wants a unified account of mathematics, foundational pluralism will be unappealing.

f. Concluding Remarks

In this section, we’ve considered some different ways in which one can understand the term ‘foundation’ and what the corresponding job of a foundational theory might be. There is little agreement over what the key features of a foundation for mathematics are, and that this affects both the kind of theories that might be proposed, but also how they are evaluated. The discussion in this section should not be taken as conclusive, but rather as indicative. This article has not provided an exhaustive list of all the ways in which a foundational theory might be characterised, but instead it has focused on some natural and rather prominent views which are to be found throughout the literature. Readers interested in exploring these issues further should consider sources such as Sommaruga (2011), Benacerraf & Putnam (1984), Centrone and others (2019) which provide excellent collections of papers concerning these topics.

As was mentioned in 2c, purely philosophical analysis regarding foundations of mathematics has taken something of a back-seat. Foundational proposals have become less concerned with matters of ontology or epistemology, and have instead pivoted towards other, more clearly mathematical means of evaluation. That is, most contemporary proponents of foundational theories now try to outline desiderata for evaluating one proposal relative to one another, rather than provide a philosophical account of what the nature of a foundation is. That said, of course these issues still linger in the background. In the remainder of this article we will use this first section as a framework for discussion. So, with that said, let’s now turn to some of the particular candidate theories which have been claimed to provide a/the foundation for mathematics.

3. Set Theory

The most popular and widely studied foundational theory is set theory. As the name would suggest, the fundamental objects of set theory are sets, understood pre-theoretically as collections of objects (called elements). The language of set theory is typically classical first-order logic augmented with a binary predicate ‘’ denoting membership. Sets are understood extensionally – that is, they are exhausted by their members. As a result, any two sets containing all and only the same elements are identical. Sometimes, so-called ‘impure’ sets are considered sets containing members which are not themselves sets (so-called ‘urelements’) such as the set of all people in Manhattan. Typically however, for foundational purposes and thus for the purposes of this article, we will consider only pure sets — that is, sets whose only members are themselves sets.

A natural way to conceive of sets is as collecting together all the objects corresponding to a property. For example, we can think of the set of all chairs, the set of all natural numbers, the set of all red things and so forth. Unfortunately however, early on in its development this naive picture was shown to be inconsistent via the Russell Paradox ######## link to /par-russ/. In light of this, mathematicians sought to consistently axiomatise set theory in such a way as to exclude pathological sets like the Russell set, the Universal set, or the set of all ordinals (among others). The result of this process was the now standard axiomatisation of ZFC (Zermelo-Fraenkel set theory with the axiom of choice). Other axiomatisations of varying strength exist (Kripke-Platek, Vonn-Neumann-Bernays-Godel, Scott-Potter, and so forth) however, for present purposes we’ll restrict attention to ZFC as the most common. Since the 1930s it has become standard practice to view this theory as playing some sort of foundational role for mathematics. Indeed, when one examines almost any textbook concerning set theory one is faced with more or less explicit declarations to this effect:

All branches of mathematics are developed, consciously or unconsciously, in set theory (Levy 1979, p.3). Set Theory is the foundation of mathematics… From [the axioms of set theory] all known mathematics may be derived (Kunen (1980), p. xi).

[M]athematical objects (such as numbers and differentiable functions) can be defined to be certain sets. And the theorems of mathematics (such as the fundamental theorem of calculus) then can be viewed as statements about sets. Furthermore, these theorems will be provable from our axioms. Hence, our axioms provide a sufficient collection of assumptions for the development of the whole of mathematics – a remarkable fact (Enderton (1977), pp. 10-11).

Clearly then, set theorists themselves view their subject as playing an important, arguably indispensable foundational role. As is well known, set theory as given by ZFC (perhaps augmented with some suitable large cardinal hypotheses) can serve as a domain into which all of classical mathematics can be embedded. With few exceptions (such as more universal collections like the set of all sets, set of all groups and so forth.) all the results and concepts of classical mathematics are formalisable within the language of set theory.

Clearly, this is a remarkable technical achievement. However, in order to gain a better understanding of the purported significance of set-theoretic foundations, we must ask: what is the philosophical significance of this technical achievement? Answering this question is a relatively substantial challenge for both adherents to, and critics of set-theoretic foundations.

a. The Case for Set Theory

In this section, we’ll consider a variety of ways in which one might explain the foundational significance set theory, and gesture broadly towards wider questions in the literature. As should be expected, one can conceive of set theoretic (or any other) foundation(s) in line with section 1. So, we can ask whether or not set theory provides a fundamental ontology for mathematics, whether it gives epistemological insight into mathematical practice and so forth. It also considers claims put forward by advocates of set-theoretic foundations purporting to establish set theory as the unique foundation for mathematics.

As we’ve noted, almost all of classical mathematics can be carried out within the language of set theory. One way to cash-out the foundational value of this is by understanding the foundation as a ‘final court of appeal’ for mathematics. What this means in practice can be split into two separate functions which following Maddy (2016) (compare Maddy (2019)) we can call shared standard and generous arena. Let’s explore each of these.

One of the most important aspects of mathematical practice is proof. Articulating what the relevant standards of proof are is a function that one can conceivably expect of a purported foundation for the discipline. Set theory has often been viewed as providing exactly this: if we want to know whether a given conjecture is provable we enquire about whether or not it can be derived within set theory. Sociologically speaking, this is indeed the case. Often when proving theorems, mathematicians will note the strength of the assumptions required for the result relative to ZFC, and in particular whether their assumptions are stronger (for example requiring some large cardinal principles) or weaker (for example not requiring choice). In this way, set-theoretic foundations provide a shared standard for what counts as legitimate proofs across the various branches of mathematics.

Aside from this, the shared standard provided by set theory can potentially help explain one of the most remarkable and productive features of mathematics: that results and ideas from one branch can often be applied to others with little prima facie connection. For example, Wiles’ celebrated proof of Fermat’s last theorem involved bringing together elliptic curves and modular forms (via the Taniyama-Shimura conjecture) over rational fields to prove a statement of arithmetic. Often, we see some of the most astounding breakthroughs result from taking techniques and ideas from one area and transplanting them into another. This suggests some sort of overarching unity to mathematics as a whole, and that’s exactly what the notions of shared standard and generous arena are intended to explain.

As modern mathematics has developed, interconnections between different sub-disciplines have become increasingly important. As a result, philosophical questions about the transference of information across these branches likewise becomes more important. As Burgess (2015) remarks:

Interconnectedness implies that it will no longer be sufficient to put each individual branch of mathematics separately on a rigourous basis… The only obvious way to ensure compatibility of the starting points… is ultimately to derive all branches from a common, unified starting point (Burgess (2015), p. 60-62).

Clearly, for these results and techniques to be transferable and effective across different branches of mathematics, they must be in some sense compatible. Intuitively, if each discipline were founded in isolation, there should be no prima facie guarantee that they should be consistent when combined together. For this reason, set theory is often thought of as providing a generous arena for mathematics, a single, unified setting wherein the various structures studied by mathematicians can be manifested, studied, and related to one another. Since almost all of mathematics is capable of being embedded in set theory, one line of thought maintains that the significance of this embedding is in providing a unique domain wherein all branches of mathematics can coexist, and the relationships between them can be studied and developed in the same language. This approach emphasises the ‘faithful representation’ criteria and the standards of proof discussed in below. Although the desiderata of shared standard and generous arena can be thought of as more general foundational features to which ZFC has no exclusive claim (as we will see in subsequent sections), advocates of set-theoretic foundations believe that traditional membership-based set theory is the best candidate for achieving these goals. According to such advocates, set theory is uniquely able to provide the best representation of all (or almost all) other mathematical objects in a way that maintains their mathematically relevant features, and allows one to investigate the relationships between them in a single unified setting.

By providing a generous arena and a shared standard of proof, set-theoretic foundations purport to ensure that the various mathematical theories it formalised in ZFC do not contradict one another. As new branches of mathematics are developed and studied, new axioms are formulated, and new theories postulated, having a unified arena within which one can check the relative consistency of these ideas has become something of a mathematical safety blanket.

Of course, all of this consistency talk must be taken with a rather large pinch of salt. What these results show is that the theories in question are consistent under the assumption that set theory is itself consistent. This of course is a rather large assumption, and so these relative consistency proofs will not be able to convince a skeptic until they can be assured that the axiomatisation of set theory is itself consistent. This was keenly felt by the founders of set theory, who sought to establish for themselves an ironclad consistency proof of the axioms. For example, Zermelo (1908) remarks:

I have not yet even been able to prove rigourously that my axioms are consistent, though this is certainly very essential; instead I have had to confine myself to pointing out now and then that the antinomies discovered so far vanish one and all if the principles here proposed are adopted’ (pp. 200-201).

We in the post-Gödellian world have the benefit of hindsight to know that the search for such an ironclad guarantee is futile. What these instantiations in the set-theoretic universe show us is that the various theories instantiated therein are at least no more dangerous than set theory itself.

Although this situation might initially seem bleak, it has led to an extremely fruitful ongoing investigation of the consistency strength of various mathematical theories both stronger and weaker than ZFC, using these axioms as the benchmark. As one progresses through this consistency hierarchy, the risk of inconsistency becomes ever greater. From relatively weak subsystems of second-order arithmetic (Simpson (2009)) through to ever higher realms of the transfinite (Kanamori (2003)), we now have a well studied progression of the consistency strength of theories indexed by increasingly strong large cardinal hypotheses. This can be seen as yet another role for set-theoretic foundations: Risk Assessment. By augmenting ZFC with certain large cardinal principles we can study the level of potential danger that a given theory poses, by measuring where it falls on the relative consistency strength hierarchy. As such, we can understand set-theoretic foundations as providing a tool for assessing the risk of inconsistency incurred by various theories closely related to the desiderata of sectio 2.c.iii.

In addition to relative consistency results extending beyond ZFC via the large cardinal hierarchy, another benefit of the generous arena emerges from studying the meta-mathematical properties of theories embeddable within set theory. According to proponents of set-theoretic foundations, codifying mathematics in a specific axiomatisation (like ZFC) creates a controlled environment where meta-mathematical properties of different theories can be studied and compared. By regimenting various other areas of mathematics in the language of sets, one can investigate and prove claims about these branches themselves in quite a level of generality. This feature has become known as the ‘meta-mathematical corral’ (see Maddy (2016), Maddy (2019) ), and the central idea is that formalising mathematics within set theory affords the possibility of mathematically studying mathematics itself. On one hand, this process gives insight into the consistency of theories relative to ZF, since proving that a theory can be consistently instantiated somewhere within the iterative hierarchy is widely regarded as sufficient evidence that the theory in question is indeed consistent. On the other, it allows for the sharpening of previously imprecise statements and questions which then become amenable to mathematical investigation. For example, questions concerning the provability of a certain conjecture or the existence of a certain structure become mathematically tractable. Once formalised within set theory the mathematician can check whether the given conjecture is provable or not from the ZFC axioms, or whether the structure in question has a model within the iterative hierarchy.

This process suggests another, related foundational virtue set theory is sometimes claimed to possess. Namely, that by formalising other areas of mathematics within set theory, the concepts and ideas involved in that area become clarified or sharpened. One can improve upon previously imprecise notions and concepts by providing a more rigourous set-theoretic surrogate. In Maddy’s terminology, set theory comes to elucidate the ideas in these other branches (Maddy (2016)). For example, the historically geometric understanding of continuity was insufficient for providing rigourous proofs of the central theorems of calculus. Dedekind’s work in reconceptualising classical analysis using more exact set-theoretic apparatus led to the replacement of a previously imprecise notion with a more precise one. In a similar way, we can compare contemporary presentations of topics such as differential geometry or point-set topology with their original founding papers. The introduction of set-theoretic apparatus has made understanding many such ideas far more accessible for mathematicians and standardisation of vocabulary in set-theoretic terms has provided something of a universal language for mathematics; one which allows some degree of basic familiarity with the objects involved regardless of ones area of expertise. The key idea is that by recasting ideas in terms of sets, the objects in question become further articulated and studied (this once again connects to the foundational role of ‘faithful representation’ as discussed in 2ci). In this way, it is sometimes claimed that the study of other mathematical ideas via set-theoretic techniques can further elucidate and precisify the relevant notions and ideas involved.

To briefly summarise this section, there are a number of further characteristics that one might take their preferred foundational theory to possess: A tool for assessing the risk of inconsistencies, a generous arena in which surrogates for all mathematical objects can be defined, a shared standard for mathematical proof, a metamathematical corral in which formal techniques can be employed in order to study mathematics itself, and the elucidation of previously imprecise mathematical concepts. According to advocates of set-theoretic foundations (for example Maddy (2019) p.310) ZFC (or ZFC-like theories) are the best option for a theory which possesses all of these characteristics.

b. Questions and Debate

Whether or not set theory is successful in fulfilling all/any of the foundational roles that its advocates claim is the subject of heated discussion. Moreover, as we will see in the next section, even acknowledging that it does serve some/all of these purposes, the question of whether those foundational goals are best served by set theory or whether an alternative should be preferred is also hotly contested. In closing this section however, we point to some particularly lively current debates concerning set-theoretic foundations. Of course, the philosophy of set theory is itself a substantial area of investigation (see Bagaria (2023), Cunningham (n.d.), Potter (2004) ) so in this section we confine ourselves to certain questions which might be taken to have some bearing on the foundational significance of set theory.

i. Independence and Axioms

The first challenge to set-theoretic foundations emerges immediately upon acceptance. If the foundations of mathematics are to be captured in a theory of sets, which one should we choose? There are several available axiomatisations of set theory (ZFC, Morse-Kelley, Scott-Potter, Kripke-Platek, and so forth.) all of which vary in strength. So even if one endorses set theoretic foundations, there is still the further question of which set theory ought to be accepted.

The next question is once again brought to us by Gödellian considerations. It might be expected that a foundation for mathematics gives us a standard of truth for mathematical statements. At the very least, one might expect that the foundation will be capable of confirming the truth of those statements which are actually true. This aspiration was somewhat ubiquitous in the early days of foundational studies. It was widely hoped that set theory would provide just such a resource for mathematics; giving an ultimate judgement on whether or not a given conjecture or hypothesis is true or false in a mathematically precise formalised way. Unfortunately however, we know that such ambitions are impossible due to the incompleteness theorems. These results show that any theory capable of interpreting a reasonable amount of arithmetic will necessarily be incomplete. More precisely, assuming that the system in question is indeed consistent, such a system will contain a statement of the language which is neither provable nor refutable within that system. In particular then, if set-theoretic foundations are consistent, then there will be sentences in the language of set theory which are undecidable. Moreover, the second incompleteness theorem (a corollary of the first) establishes that in particular, the statement that the theory is consistent (Con(ZFC)) is one of these undecidable statements.

The existence of statements that are undecidable from the axioms of the theory gained renewed importance in 1963 when Cohen established that the Continuum Hypothesis – a natural statement about the cardinality of uncountable sets is independent of ZFC (, ). Cohen’s method of forcing was soon adapted and employed to yield a number of important independence results. Accordingly, it became increasingly clear to the mathematical and logical community that set-theoretic foundations were incapable of settling many open questions. As a result, many researchers have sought to ‘shore up’ the foundational enterprise by augmenting theories like ZFC with a number of so-called strong axioms of infinity also known as large cardinal axioms (though other classes of principles have been proposed). The sets declared by these principles cannot be proven to exist within ZFC, and often entail a ZFC-independent statement or its negation as a consequence. This is a lively area of contemporary research in the field and has generated significant philosophical and mathematical debate concerning the justification of such principles (See Kanamori (2003), (2010), Welch (2015) ). Once again then we are faced with the challenge of deciding which axioms to accept for our foundation. Even if one accepts set-theoretic foundations, should these be minimal or should they include large cardinals, and if so which?

Ultimately, even if one accepts that the foundations of mathematics are to be found in axiomatic set theory, the question remains: which axioms?

ii. Universes and Multiverses

Another question for set-theoretic foundations concerns the understanding of set theory itself. In particular, should we think that the domain described by our foundation is unique, or one of many? Should we believe that statements like the continuum hypothesis have a definite truth value in this privileged model, or should we think that it varies across interpretations? These issues are somewhat downstream of section 1. Even if there is agreement that the foundations are to be set-theoretic, what the correct interpretation of set theory is, and how we regard the truth value of independent statements such as CH, remains a debated question. Fundamentally, should we regard set theory itself as having a single, unique intended interpretation, or are there many equally acceptable interpretations?

This has become known as the multiverse debate in set theory. Those who view ZFC as fundamentally regarding a single set-theoretic universe (V) are known as universists, whereas those who reject the idea that any one interpretation of the ZFC axioms can be singled out as the set-theoretic universe, are known as multiversists.

There are a number of different multiverse proposals on the table (for a more detailed overview see Antos et al. (2015), Barton (2021), Väänänen (2014) ). Perhaps the most well known and discussed of these is due to Hamkins (2012). Hamkins’ account is motivated fundamentally by mathematical practice; in noting that the advent of forcing has driven the field of set theory to concern itself primarily with a variety of different models of the axioms, he claims that the fundamental objects of inquiry are these models themselves. Indeed, set theorists appear to move deftly between these structures in a way which Hamkins claims would be hard to account for if there were really only one single absolute background set theoretic universe (Hamkins (2012) p.418). Hamkins’ conception is strongly Platonistic in character. According to this view, each universe within the multiverse is a bona fide existing abstract object. Hamkins is not alone in considering a set-theoretic multiverse. Some more conservative varieties of multiversism have been put forth, for example by Wooding (2011), and Steel (2014). For Woodin, ‘generic multiversism’ is a useful heuristic for guiding set-theoretic practice, but he ultimately rejects it as a settled view (Woodin (2011)). Steel on the other hand sees more value in the multiverse project, and has gone so far as to provide an axiomatisation of the multiverse (Steel (2014)).

Ultimately, the question of interpreting set theory raises a number of fascinating discussions. Is there but one set-theoretic universe or a plethora of them? Must all legitimate universes be axiomatised by ZFC or are there others? Is there a unique core to the set theoretic universe (such as Woodin’s ultimate-L or Steel’s core model)?

Once again, there are some significant questions for set-theoretic foundations which remain unsettled even if disputes over whether or not foundations should be set-theoretic subside. In this case, even if all parties adopt set theory as a preferred foundation, we must still settle the question of which set theory to adopt, and how that theory should be interpreted.

4. Category Theory

So far, we’ve discussed traditional set theory which provides an axiomatic treatment of the concepts of collection, and membership. The various axiomatisations mentioned in section 2 take these ideas as fundamental and develop a rigorous mathematical system on that basis using ‘∈’ as the sole non-logical constant. In this section, we’ll turn to explore alternative foundational theories presented using the language of category theory.

First introduced in MacLane & Eilenberg (1945) category theory has a fundamentally algebraic nature. Unlike set theory, the basic concept involved is that of a function or morphism, which can be thought of as a structure preserving mapping between objects. The canonical presentation of category theory is MacLane (1971), but readers interested in a more accessible introduction to the mathematics involved are urged to consult Awodey (2006), Leinster (2014), and Riehl (2017). For an excellent collection of papers concerning the philosophical aspects of category theory see Landry (2017).

Category theory, in its full generality, is perhaps best understood as a language for the expression of mathematical ideas and relationships. This language provides a way of unifying and simplifying ideas from across mathematics, and provides an abstract description of mathematical objects and their relationships with a high degree of generality. Rather than focusing on particular objects directly, category theorists tend to emphasise properties and transformations between objects of a more general kind (that is, the process of characterising mathematical objects via their relational, so-called universal properties).

In general terms, we can think of a category as an algebraic object, analogous to a group, ring, or field. The intention behind categories is to capture the abstract notion of a system of mappings between some objects. Therefore, on a first pass we can think of a category as a collection of objects, as well as arrows on those objects which are closed under composition. Category theory emphasises treating both the objects and morphisms as equals, never considering one without the other. In this general sense the idea of a category mathematically formalises the concept of a structure preserving transformation between some objects of a given kind.

To get the hang of this, a comparison with other, more familiar objects from abstract algebra is helpful. Recall that a group is typically understood as a set equipped with a binary relation which satisfies associativity, identity and inverses. In the same way, we can think of a category as a sort of generalised or further abstracted group. A category consists of some objects, and some arrows which have special properties. In particular, they are associated with a domain and codomain, they are closed under function composition, associate to each object in the category a unique identity function, and satisfy both associativity and unit (unit here means that for any arrow f:A→B, with A,B objects in the category f∘1_A=f=1_B∘f. See Awodey (2006) and Leinster (2014) for details.

From these basic ideas of objects and arrows, category theorists have developed an increasingly sophisticated framework capable of capturing a variety of mathematical fields in categorical terms (for example the category of sets, groups, graphs, vector spaces, differentiable manifolds, and so forth.). One slogan which remains integral to the discipline is “it’s the arrows that really matter”. As such, one should be careful if trying to reconstruct the ideas in other terms which would eschew the importance of arrows in favour of some more familiar object.

a. ETCS and CCAF

Given the expressive resources afforded by category theory, a number of different proposals using category-theoretic ideas have been suggested as a foundation for mathematics. In this section, we will focus on two of the most prominent such theories which have been discussed as candidate foundations for mathematics. These are The Elementary Theory of the Category of Sets (ETCS) (Lawvere (1964)), and the Category of Categories as a Foundation (CCAF) (Lawvere (1966)). As with other sections in this article, technical details are largely overlooked in favour of a more general and descriptive approach to the theories in question.

i. ETCS

The Elementary Theory of the Category of Sets (ETCS) is, as the name would suggest, a theory of sets constructed in the language of category theory. The fundamental idea is that ZF-esque set theories do not have a privileged entitlement to the intuitive notion of a collection. Where traditional set theories axiomatise the binary relation of membership (), categorical set theory instead axiomatises the ternary relation of function composition. As a result, in traditional set theory, questions concerning membership between arbitrary sets are well-formulated since the membership relation is global. However in categorical set theory, the membership relation will be local to elements and subsets of some ambient set.

Originally ETCS arose as a result of Lawvere’s attempts to provide a more pedagogically useful foundational theory within which he could construct the algebra and analysis he was required to teach (Ernst (2017) p.70) but he soon came to realise how mathematically useful his framework could be. In Lawvere (1964), he provides an axiomatisation of a theory of sets using only categorical vocabulary, shows the uniqueness of the resulting category of sets , and demonstrates that:

The theory provides a foundation for number theory, analysis, and much of algebra and topology even though no relation ∈ with the traditional properties can be defined. (Lawvere (1964) p.1506)

Categorical set theory can be achieved either via the theory for a well-pointed topos with the axiom of choice, or more directly through Lawvere’s axioms which are equivalent (for an informal presentation of the axioms of ETCS see Leinster (2014) p.404. For a more rigorous treatment see Lawvere (1964)). The result is a powerful mathematical theory which takes as its only theoretical primitives the notions of mapping, domain/codomain, and composition. As such, ETCS does not presuppose a background universe of sets or other foundational theory in order to get going.

Mathematically, there is little to tell between categorical, and more traditional membership-based set theories as far as their strength is concerned. Although ETCS is equivalent to a slightly weaker membership-based theory (BZC) () there are a variety of extensions which can be made to yield a theory of equivalent strength to ZFC. Nevertheless, the fact that ETCS on its own is strictly weaker than ZFC highlights some remarkable foresight on Lawvere’s part when he remarked that ‘it is the author’s feeling that when one wishes to go substantially beyond what can be done in the theory presented here, a more satisfactory foundation will involve a theory of the category of categories’ (Lawvere (1964) p.1510). Two years later, he did just that.

ii. CCAF

The Category of Categories as a Foundation (CCAF) emerged out of a desire to capture the structural nature of mathematics in a theory which is strictly stronger than ETCS. As Lawvere puts the point:

The question thus naturally arises whether one can give a foundation for mathematics which expresses wholeheartedly this conviction concerning what mathematics is about, and in particular in which classes and membership in classes do not play any role. Here by “foundation” we mean a single system of first-order axioms in which all usual mathematical objects can be defined and all their usual properties proved (Lawvere (1966) p.1).

It should be noted that for any reader looking to study this theory, the original presentation has a few technical flaws, but these were later resolved by McLarty (1991).

CCAF describes a category whose objects are themselves categories, and ‘arrows’ which are functors between those categories. It contains the terminal category ‘1’ which is the canonical object category, as well as the two-object category (creatively named ‘2’), and a final unique category (‘3’) which allows the theorist to understand composition of arrows in arbitrary categories. In addition to the axioms describing this framework, we add assertory axioms which declare the existence of particular categories. Two particular methods of note which enhance the strength of the resulting theory are either the method of Grothendieck universes (leading to a theory roughly equivalent to ZFC+a proper class of inaccessible cardinals), or the Eilenberg-MacLane distinction between ‘small’ and ‘large’ categories (resulting in a system roughly equivalent to NBG set theory). Once these assertory axioms are in place, CCAF becomes a candidate foundational theory for mathematics possessing a uniquely structural character.

b. Motivating Categorical Foundations

The categorical perspective on the foundations of mathematics is one of a particularly structuralist disposition. Proponents of these theories tend to view the relevant properties of mathematics as those which are describable solely in terms of their abstract structure (see for example Lawvere (1966) p.1). This is one motivation for eschewing traditional set-theoretic foundations. Many category theorists believe that membership based set theories such as ZFC impose far too much extraneous structure upon mathematics and involve properties which are non-structural. This is one of the supposed benefits of categorical foundations: to trim the fat and have a foundation with maximal flexibility and minimal inherent structure.

In order to capture the features which they take to be fundamental to mathematics, the advocates of categorical foundations seek a foundational theory with a much more algebraic character, one which does not introduce or impose extraneous structure upon the discipline and does not involve any non-structural properties in its language. One of the key aims behind category-theoretic foundational proposals is to provide a foundational theory which would be of use to practicing mathematicians, and which would guide practice towards important structures which can be characterised solely in terms of their mathematically important features. In Maddy’s verbiage, these proposals provide ‘essential guidance’ for mathematical investigation ( Maddy (2019), p.303). This motivation ties in directly with the linguistic desiderata discussed in 2ci. According to many proponents of categorical foundations (such as Awodey (2004) ) the goal should not be to provide some robust universe of objects, but rather to provide a conceptual framework or language for mathematics which is highly flexible. Such advocates believe that the language of sets is too rigid, and thus imposes set-theoretic structure on the rest of mathematics where it need not be invoked. Instead, they emphasise that we should have a foundational language for mathematics with a sufficiently schematic character so that it can apply as widely as possible. Such a language for mathematics should itself be minimally structured so as to not limit in any way the expression of other branches. This is precisely what categorical foundations are purported to establish (for more on the relationship between category theory and structuralism see Awodey (2004), Mclarty (2004) and Landry (2017) ).

A second motivation for categorical foundations is universality. In the usual axiomatisations of set theory (at least as given by an iterative conception of set) certain kinds of universal sets are prohibited on pain of inconsistency. There can be no set of all sets, and in general no set-theoretic surrogate for the unlimited categories which are often used in categorical algebra. Thus if one finds themselves requiring the use of such collections, traditional set-theoretic foundations will restrict their practice. MacLane (1971) makes the point here nicely:

Categorical algebra… uses notions such as that of the category G of all groups… To realize the intent of this construction it is vital that this collection G contain all groups; however, if “collection” is to mean “set” in any one of the usual axiomatizations of set-theory, this intent cannot be directly realized. This raises the problem of finding some axiomatization of set theory — or of some foundational discipline like set theory — which will be adequate and appropriate to realizing this intent (MacLane (1971) p.231).

According to MacLane, some areas of mathematics require the use of certain universal collections. Collections which are explicitly forbidden in typical set-theoretic renderings. Feferman (1980) notes this in claiming that one desiderata for categorical foundations is to form the category of all structures of a particular kind (for example all groups, topological spaces, categories and so forth (p.154)). This emphasis on universality can be seen through the lens of 2ci. If category theory really is capable of representing all mathematical objects of a certain kind within its framework, and do so without distorting any mathematically significant properties, then it would seem that this is a boon to the ‘faithful representation’ desiderata. If we value faithful representation of mathematical objects highly, then the ability to represent the relevant class of objects in their entirety is surely a more faithful representation than one that is only partial. Thus if the advocates of category theory are correct, and this is something which can be done in categorical foundations but not set-theoretic foundations, it would be a telling point in favour of their proposals.

In order to meet these needs, it was proposed that category theory be adopted as the foundation for such unlimited categories, allowing for the formulation of ‘the category of all X’s’ for some mathematical object X, which can then be subjected to mathematical analysis and operations. It is interesting to note however, that although some incremental progress in this direction was made, a recent breakthrough due to Ernst (2015) shows that truly unlimited foundations cannot be formulated consistently. In particular, there can be no foundation which simultaneously yields the category of all structures of a given kind, the category of all functors between categories, and the existence of a category of natural numbers. The inconsistency of unlimited categories was shown via the assumption that one can form the category of all graphs.

Despite this, category theory remains a popular candidate foundational theory among those who seek a more flexible attitude towards foundations. Indeed, Lawvere himself asserted that foundations should not be thought of as static and unchanging. Rather, he believed that ‘foundations come out of practice, and will change as practice develops’ (quoted in McLarty (2011) p.148). This attitude towards foundations is, in some instances, close to the type of anti-foundationalism canvassed in section 1. While it does not explicitly deny the need for a foundational theory, it does take that theory to be somewhat provisional; and capable of changing over time in line with the needs of mathematics. The idea then is of foundations as a set of organisational principles for the actual practice of mathematics, and as mathematics develops, new and better organisational principles might be put forward.

c. Questions and Debate

The main criticisms of categorical foundations center around three issues: adequacy, autonomy, and assertion. In a nutshell, these concern firstly whether category-theoretic foundations are really capable of founding enough mathematics as their proponents claim. Secondly, whether category theory can stand on its own without the presupposition of a background set-theory. And thirdly whether the axioms of categorical theories can actually be understood as declaring the existence of certain classes of mathematical objects. Let’s briefly consider each of these in turn, before considering some direct comparisons with membership-based set theory.

i. Adequacy

Authors such as MacLane (1971) have motivated category-theoretic foundations as a solution to the perceived technical inadequacy of traditional set theory. In a similar vein however, proponents of set theory have themselves criticised category-theoretic foundations for their own alleged inadequacies in capturing certain aspects of mathematics. Notably, a series of complaints have been made by Mathias (1992, 2000, 2001) arguing that categorical foundations are incapable of adequately delivering a number of fundamental results in analysis, and iterated construction procedures which are easily formulated in traditional set theory. If these criticisms are correct, and category theory is incapable of capturing large swathes of mathematics, this would certainly tell against the adequacy of category-theoretic proposals especially in relation to the desiderata of 2c.

Many proponents of category theory have remained unmoved by these criticisms. For a response to these charges see Ernst (2017). As we’ve noted already, categorical set theories can be augmented with additional axioms so as to yield a theory of equivalent strength capable of delivering the results Mathias cites. However, critics of this approach often maintain that although the results can be formally recovered in categorical set theory, the way that this is achieved is often less natural than in traditional membership-based set theory. Of course, the question of what counts as ‘natural’ in this setting is as contentious as anything else – what appears natural to one person need not appear natural to another. That said, there does appear to be something of an interesting phenomena underlying these criticisms. Namely that the descriptive resources afforded by one language or another often appear to be more or less suited to describing different sub-disciplines of mathematics. For example, while many aspects of algebra and topology are comfortably described in categorical terms, some aspects of analysis and logic appear much less easy to capture. Ultimately however, this is not a question of formal adequacy since (as noted) both categorical and membership based set theory can be given equivalent formulations, but perhaps something closer to aesthetics.

ii. Autonomy

The question of whether categorical foundations can be rightly seen as autonomous originates in Feferman (1980), but was developed in great detail by Linnebo & Pettigrew (2011). In its original form, the objection is that category theory itself depends upon a prior grasp of the notions of operation and collection which are themselves prior to any structural notion (Feferman (1980) p.150). According to Feferman, these notions are both logically and psychologically prior to anything in category theory.

In developing these ideas, Linnebo & Pettigrew (2011) introduce several helpful distinctions to evaluate whether or not category theory can be regarded as properly independent of some further background set theory. As we saw in section 1.3.2, they distinguish between three forms of autonomy, and claim that for a foundational theory to count as truly autonomous it must meet all three criteria:

- A theory T is logically autonomous if it is possible to formulate the terms of that theory without appealing to notions from some other theory.
- A theory T is conceptually autonomous if it is possible to understand it without first understanding the concepts from some other theory.
- A theory T has justificatory autonomy if it is possible to motivate and justify the posits of the theory without appealing to another theory or its justifications.

Whether or not a given iteration of category theory actually meets these standards is still a matter of debate (though Linnebo & Pettigrew (2011) find ETCS to at least have conceptual and logical autonomy). Ultimately, what is at issue in these debates is whether or not category theory can be regarded as a bona fide foundational theory for mathematics, or whether set theory is really doing the work in the background.

iii. Assertion

The final criticism we will consider is whether the axioms of category theory can be truly regarded as assertoric. This criticism is most commonly associated with Hellman (2003) who claims that category theoretic foundations fail to make existential assertions about the fundamental objects of mathematics. This is in stark contrast to traditional set-theoretic foundations which contain axioms positing the existence of certain sets. Category theory on the other hand, according to Hellman, in virtue of its algebraic nature instead consists of axioms which provide a definition of certain sorts of structures (categories or toposes). For example, after giving the formal definition of a category, Awodey (2006) claims that ‘A category is anything that satisfies this definition… a category is an abstract algebra of functions… you may think of a category as a sort of generalised group’ (p.5). Once again the comparison with groups is helpful; the axioms describe what it is for some object to behave in the relevant way, but they do not make any assertions about the existence of such objects.

In the setting of generalised category theory, this seems undeniably true, at least if certain introductory texts on the matter are to be believed:

In set theory, one often begins with existential axioms such as “every set has a power set”… Our axiom that every arrow has a domain and a codomain is not to be understood in the same way as set theory’s axiom that every set has a powerset! The difference is that in set theory – at least as usually conceived – the axioms are to be regarded as referring to (or determining) a single universe of sets. In category theory, by contrast, the axioms are a definition of something, namely of categories (Awodey (2006) p.21).

There appears to be some sense then in which Hellman’s objection is correct. If the axioms of category theory fail to say whether or not any categories actually exist, this would seem to be reasonably regarded as a defect.

However, whether or not this is a fair reading of category theoretic foundations is a matter for debate. For one thing, there is an important distinction to be made between category theory simpliciter (that is, the formal language within which theories can be formulated) and the axiomatic systems using this language proposed as candidate foundations. It is uncontroversial that the former is not assertory, just as first-order logic (with a membership predicate) itself fails to assert the existence of sets. However, this does not appear to be what is under discussion in most debates. As we have seen, the kinds of mathematical languages for providing descriptions of objects are not themselves typically understood as a foundational proposal. Rather, it is a system of axioms cast in those languages (ZFC, ETCS, CCAF and so forth.) which are the subject of discussion. Authors such as McLarty (2004) and Linnebo & Pettigrew (2011), argue that theories such as ETCS do genuinely provide assertoric axioms, whereas others such as Awodey (2004) deny that this is either an important or necessary feature of mathematics.

iv. Comparison with Set Theory

In describing the potential benefits of set theory (2.1) we spent some time considering the virtues of a shared standard, generous arena, relative consistency strength, and consistency strength hierarchy. If these are indeed important desiderata to be met by any candidate foundation, then it is worth pausing to consider how they might be understood in the context of category theory.

The answers to these questions will to some extent at least, depend upon the answers to the question posed in the previous subsection. As we’ve noted, pure category theory (as described by Maclane (1971)) is not a foundation per se, but rather a powerful and flexible language for describing mathematical structure. However, as we’ve also seen, the foundational proposals made by category theorists involve the implementation of specific foundational theories – most often categorical set theories like CCAF and ETCS which have been argued to be suitably assertory so as to meet this challenge. Thus, a foundational theory which makes genuine assertions about the objects of mathematics can be formulated in categorical terms.

It is worth noting that the way in which one might evaluate category-theoretic foundations does seem to be a potential source of debate within the relevant community. For example, scholars such as who have a relatively minimal conception of foundation (see section 1.3.1) seem to reject the desiderata of shared standard, generous arena, and so forth as presupposing the idea of set-theoretic foundations. Thus, such authors would reject these as criteria for assessing the adequacy of a candidate foundational theory. However, this view is not universally held, since authors like McLarty (1991) seem willing to seek a theory (like CCAF or ETCS) which can be judged alongside traditional membership-based set theory in these terms.

Setting this internal schism aside, let’s briefly consider some direct comparisons. It seems that the shared standard of proof – at least as articulated in sections 2ciii and 3a, can be captured categorically. The significance of whether a given result can be derived from the foundational theory will not change, though what may change (and indeed somewhat radically) is what such a derivation might look like. Both set-theoretic and categorical foundations can provide derivations of significant results in other areas of mathematics, even if, for example, group theory in the language of sets looks radically different from group theory in the language of categories. Of course, one of these derivations might be more strained than the other, and perhaps seem more unnatural or complicated, but, in the ecumenical spirit, this article considers this something of a pedagogical question. Perhaps if mathematics education were to be reframed in categorical vocabulary, these derivations would seem just as natural as their set-theoretic counterparts. In principle then it seems that the shared standard desiderata could be met, at least in the abstract.

Similarly, it seems that the desiderata of generous arena can be met by categorical foundations, at least when expressed via CCAF and ETCS. This is especially true if the theory is augmented with Grothendieck universes or very large toposes as discussed in previous subsections. This would presumably also give something roughly equivalent to a large cardinal hierarchy and could thus in principle be used to formulate something like a consistency hierarchy for categorical theories.

d. Some Final Remarks

In conclusion, category theory appears to provide at least a plausible alternative to traditional set-theoretic foundations, based upon fundamentally structural insights and formulated with a uniquely algebraic character. The term ‘category-theoretic foundations’ encompasses a variety of candidate theories, but the most well-discussed of these are undoubtedly ETCS and CCAF. Although a great deal of exciting mathematical work has been done in developing these theories and studying their consequences, debate continues as to whether they constitute a legitimate replacement for set theoretic foundations or should instead be seen as a supplement to them, providing a useful perspective for working mathematicians.

5. Type Theory

As noted in section 2, the inconsistency of naive set theory presented a challenge for logicians at the turn of the twentieth century. In response to these worries, Russell (1908) proposed the theory of types. In order to block paradoxical collections from being formed, Russell’s theory emphasised the vicious circle principle: that no totality can contain members defined in terms of itself. This theory was then rigorously developed by Whitehead & Russell (1910) who demonstrated that many fundamental areas of mathematics could be formalised entirely within the theory of types. Type theory later received a great deal of subsequent development by Church (1940) who combined it with his λ-calculus, and was supplied with a completeness theorem by Henkin (1950). Important contributions to the development of type theory continued throughout the twentieth century, provided by Curry, Howard, Lawvere, Scott, and Tait. Most importantly for our purposes, constructive type theory (type theory cast in an intuitionistic logic), a descendant of the system of Russell, received extensive development by Per Martin-Löf (Martin-Löf (1973), Martin-Löf (1980)) and as a result is now frequently referred to as Martin-Löf type theory. (This article refers to it simply as constructive type theory, though others also refer to it as dependent type theory). This theory is the basis of many modern programming languages, and underlies proof assistants such as Agda, Rocq, and NuPRL. Readers interested in the development of type theory are urged to consult Kamareddine et al. (2005) for an excellent exposition of the field from the twentieth into the twenty-first centuries. For an introduction to the use of type theory as a formal system extending beyond first-order logic readers are referred to Andrews (2002), and for the particular development of constructive type theory readers are urged to consult Martin-Löf (1980) and Dybjer & Palmgren (2024).

To motivate the development of this theory, consider first-order predicate logic. It is well known that we can extend this familiar system by allowing quantification into predicate position acting on variables for predicates and functions as well as individual objects, to yield the system of second-order logic. From there, we can introduce variables for functions of functions and quantify over those to yield a third-order logic. We can continue this process indefinitely to obtain logics of arbitrarily higher order. By doing so, we eventually arrive at a system of logic that includes all logics of finite order (ω-logic) which (following Andrews (2002)) we will call finite type theory.

This theory contains two basic sorts: Types (denoted A,B…) and terms (denoted a,b…). Terms are sometimes also referred to as ‘objects’, ‘elements’, ‘points’, or ‘tokens’ of the type (for uniformity, in the present article we’ll stick with terms). Terms must always belong to a specific type. That is, there can never be a situation wherein we have a term which corresponds to an unknown type. To show that a term is of type A we write ‘a: A’. Thus, we can formalise a great many mathematical expressions such as ‘7 is a natural number’ in the language of types and terms as ‘7:N‘. From our so-called primitive types, we can generate further new types via type forming operators. For example, given two types and , we can construct the product type A x B. We can define many familiar operations in a type-sensitive way. For instance, we can think of addition as taking as input two terms of the type natural number and giving a single term of that type as output: ‘+: N x N –> N’. In order to deal with more complicated functions, one typically introduces a variable binding abstraction operator λ which acts on both a variable and a formula. This essentially creates a function that, when applied to an argument, substitutes the variable with the argument in the expression.

It is important to note that in a type-theoretic context identity is not a univocal global relation. What this means is that there will be instances of equality (such as 2² = 2 + 2) which despite receiving the same value, are not the same object (Martin-Löf (1984) p.31). The identity predicate thus requires more finesse to regiment in this system. To do so, one introduces the notion of an identity type ID_A which defines the identity relation between the terms of the type, corresponding to each type . As such, there are four closely related notions which are used in these systems: definitional equality ‘A ≡ B’, type identity ‘A = B’, the judgement ‘a = b ∈ A’, and a form of propositional equality ‘I(A,a,b)’ (Martin-Löf (1984) p.32). Initially, this may appear rather cumbersome. However, these distinctions have substantial logical payoff, allowing for a much more fine-grained analysis of various mathematical statements. Indeed, as noted by Awodey (2019) (p.18), the resulting formalism is somewhat intensional; different terms which can be used to identify the same function remain nevertheless syntactically distinct. This fact yields excellent computational and proof-theoretic properties. Moreover, it is common practice throughout mathematics to make important mental distinctions between different kinds of objects. Type theoretically, one can track these distinctions within the formal system and so some advocates of type theory (such as Andrews (2002) Ch5) have maintained that it is thus a more faithful formalisation of mathematical reasoning than alternatives.

Important for our discussions is the notion of a dependent type. These can be thought of as families which are indexed over a given type to allow the representation of predicates in the system under the ‘propositions as types’ interpretation (see the next subsection). The name ‘dependent type’ comes from the fact that the truth of a proposition depends upon the choice of term. For example, if we consider the statement ‘x is a prime number’, the truth of this statement is dependent upon the choice of x. The identity type I(A,a,b) is also an example of a dependent type, since it depends upon the terms a,b: A.

The result of this formal apparatus is a unique foundational theory which differs markedly from both set and category theory (though as one would expect, certain bi-interpretability results can be established, as will be discussed in 4.2). Constructive type theory was originally intended to provide a foundation for constructive mathematics with a distinctly predicative character, and has been studied extensively by computer scientists to form the basis of a variety of proof-assistant software.

a. Interpreting the Syntax of Constructive Type Theory

The typical semantics of constructive type theory is strongly proof-theoretic. That is, rather than understanding the meaning of the symbols through truth conditions and models (a la Tarski) the typed-language is instead typically understood via inferential behaviour (following the tradition of Gentzen (1969) , Prawitz (1974). For more on proof-theoretic semantics see Schroeder-Heister (2024) ). The proof-theoretic approach gives constructive type theory an interpretation of the logical connectives which differs markedly from that of classical logic. According to the so-called BHK interpretation of logical constants (eponymously named for Brouwer, Heyting, and Kolmogorov) the meaning of logical symbols is fixed by the kinds of constructions required for yielding a formula of that form. For example, conjunction A ⋀ B requires both a construction of A and a construction of B. For disjunction A ⋁ B, one must provide either a construction of A or a construction of B. Unlike its classical interpretation, under BHK the conditional A → B is understood as a kind of transformation: one which when applied to any construction of A yields a construction of B. Similarly, negation $◻ ϕ \leftrightarrow \neg ◊ \neg ϕ$ A is understood as a transformation which when applied to any object A yields a contradiction ⊥. The result is an understanding of logical connectives which eschews bivalence. Finally, the universal and existential quantifiers ∀/∃ are understood via the claims that every/some instance of quantification can be constructed.

This system emphasises proof, and proof construction as the fundamental account of mathematical truth. Indeed, on this view, what it is for a mathematical statement to be true or false, is for it to be proven or refuted. Thus, the conception of mathematical truth is thoroughly epistemic for constructive type theory. This point is perhaps articulated most clearly by Martin-Löf (1996):

To have proved = to know = to have understood, comprehended, grasped, or seen. It is now manifest, from these equations, that proof and knowledge are the same (p.30).

Given this attitude, the act of judgment plays a crucial role in the development of the theory. Judgments are a general kind of epistemic act. For example, we can make a judgment by affirming or denying a proposition. But we can also make other kinds of judgments. We can judge that a particular proposition is true or false, that something is indeed a mathematical object, or that a particular syntactic string is well-formed. We make such judgments frequently throughout the process of doing mathematics, and this is something which constructive type theory seeks to make explicit.

Judgments come in two kinds: categorical, and hypothetical. Categorical judgments are made without appeal to any particular context: such as judging that a type A is well-formed. On the other hand, hypothetical judgments are reliant upon some specified context or antecedent set of assumptions Γ. For example the judgment that two terms a,b of a given type A are equal in a particular context (Γ ⊢ a = b:A). These judgments form the basis of Martin-Löf’s ‘meaning explanation’ which is one of the most prominent semantic interpretations of constructive type theory (See Martin-Löf (1982) for details). This justification is somewhat Wittgensteinian, in that it explains the meaning of the language in terms of usage. The idea is that in order to understand what it means for a judgment to be correct in a pre-mathematical sense, we must examine the rules governing whatever it is that the judgment concerns. To see how this works, let’s consider the judgment that some term is indeed a mathematical object (say of type N). To check whether this judgment is correct, we must examine both the introduction rules for constructing terms of the relevant type (in this case natural numbers) as well as the elimination rules for computing with the relevant objects, and see whether the existence of this term follows from them (see 5bi for more on the arithmetic case). Via this ‘meaning explanation’ the syntax of the theory gains an interpretation, one which is widely regarded as providing substantial philosophical justification to the language of types.

i. Propositions as Types

From what has been discussed so far, it might be tempting for readers to regard types as a kind of collection with terms as elements contained within them. Although this interpretation is viable, an important alternative is available due to Curry (1934) and Howard (1980) which allows us to interpret types as propositions, and terms as proofs. Under the so-called Curry-Howard correspondence each proposition corresponds to a type, and the terms of this type are proofs of the given proposition (see also Wadler (2015) for more detail). Under this interpretation, predicates are naturally understood as dependent types. To return to our previous example ‘x is a prime number’ the predicate Prime(x) is dependent upon the choice of , and denotes the type (family) of proofs that x is a prime number. Generally then, under this interpretation, types are mathematical propositions, and the terms of a given type are its proofs.

This can be represented nicely with the following table:

0	1	A + B	A × B	A → B	Σ_x_:AB(x)	Π_x_:AB(x)
⊥	⊤	A ∨ B	A ∧ B	A ⊃ B	∃_x_:AB(x)	∀_x_:AB(x)

One can see from this table that when regarding the types A,B as propositions, a proof of the conjunction A ∧ B corresponds to a pair of proofs a: A and b: B and so the terms of the conjunctive type A ∧ B will be ordered pairs (a,b) of type A × B where a: A and b: B. In the same way, a proof of the material conditional A ⊃ B is a function f which, when applied to a proof a: A, yields f(a): B. That is, (since we’re understanding types as propositions and terms as proofs) it turns any proof of the proposition A into a proof of the proposition B, thus establishing that A implies B. The quantifiers are slightly more tricky. The quantifier ∀ corresponds to the cartesian product of the A-indexed family of types B. In other words, every instance of a proof of B given by terms indexed over A. ∃ corresponds to a disjoint sum. It involves a using a term a: A as a particular instantiating instance of a proof b: B to satisfy the judgment that B(a). This means that whenever an existentially quantified statement can be proven, one can always provide a particular witnessing instance of that statement. This feature emphasises the thoroughly constructive character of the system under discussion. It will not be possible in this theory to establish an existential claim using a classical proof by contradiction, since a demonstration that the negation of an existential statement is inconsistent does not provide an instantiating witness for the un-negated statement. Similarly, double negation elimination is impermissible since establishing that the negation of a proposition is false does not suffice for constructing a proof that the un-negated proposition holds. Although this fact means that the theory does not follow the rules of classical logic, this constructive understanding does yield a variety of nice computational properties, and is one reason why constructive type theory has been so useful in the development of proof assistant software.

b. Mathematics in Constructive Type Theory

The resultant type theory is a formal system which yields construction procedures for proofs of propositions. Originally it was intended as a foundation for constructive mathematics, and the system maintains a strongly predicative character (one cannot generalise a collection in terms of itself. As a result, there can be no such type as ‘the type of all types’). However, in order to formalise a substantial amount of existing mathematics the base system of constructive type theory needs a degree of supplementation. To do this, one typically regards the system as open-ended, allowing the addition of various type-forming operators to yield new types such as the type of natural numbers, a type of small types, and/or a schema for generating well-founded types. This allows constructive type theory to recover large swathes of constructive mathematics.

i. Arithmetic

Just as in Peano arithmetic, the natural numbers of constructive type theory are generated by the initial object 0, and repeated application of the successor function S. The introduction rule for natural numbers states that 0:N, and that given any a:N one may infer S(a):N. The elimination rule essentially encapsulates the principle of mathematical induction. It is worth noting that given the constructive nature of this type theory, the resultant arithmetic is not that of Peano, but is instead Heyting Arithmetic (HA). HA is the theory of PA cast in an intuitionistic logic, and so in this context we do not get classical arithmetic. Although this might be initially worrisome, thanks to a well-known trick of Gödel and Gentzen, it is possible to interpret all of PA within HA via the double-negation translation (for details on the construction see Avigad & Feferman (1998) and the references contained therein).

ii. Interpreting Set theory

Constructive set theory (CZF) can be naturally captured within constructive type theory. One direction of this bi-interpretability proof is quite easy, since we’ve already mentioned that one might naturally interpret types as sets, and terms as their elements, re-construing functions on types as ordered pairs. What is more interesting is the converse direction for interpreting set theory in the language of types.

To do this, we need to introduce the apparatus of inductively defined types or ‘universes’. As mentioned, there can be no type of all types in the theory. To get a suitably large construction while maintaining consistency one introduces a universe U of all the types in the theory closed under all type-forming operations which does not include U itself. The trick here is essentially analogous to the construction of inaccessible cardinals or Grothendieck universes. By constructing such a universe U, we have introduced a new, very large type into our system which characterises everything about the system except the behaviour of U itself. From there, we can iterate, and form further universes , U₁, U₂,… by adding into our extension the judgment U₂ ⊢ U₁ = U₁. This process is cumulative and is governed by the the following rules: U_i = U_i in U_i+1 and if U_n = U_n in U_i then U_n = U_n in U_j for i < j. We thus arrive at a cumulative type-theoretic hierarchy of universes which can be extended indefinitely. This process is then complemented by well-founded type construction, and leads to a very different perspective on what a set (in the sense of ZF) ‘is’. Indeed, the system can be further extended with a variety of principles analogous to large cardinal axioms (see for example Rathjen et al. (1998)). This process of model construction (that is, interpreting constructive type theory within set theory and vice-versa) has established the relative consistency of the theory (see for example Aczel (1999)). Similar procedures can be carried out using toposes. This further reinforces the claim from section 1 that the various theories discussed in this article all possess the expressive power to interpret one another.

c. Questions and Debate

Constructive Type theory offers a different viewpoint on foundational disputes, relying heavily upon a syntactic approach to mathematics, with a proof-theoretic emphasis, cast in a non-classical logic. In closing this section we will consider some criticisms of this approach to foundations. The main themes of these will be the use of a non-classical logic, the complicated syntax of the theory, and the separation of mathematics and logic. We will also make some further remarks to compare this proposal to the set-theoretic options discussed in section 2.

i. Constructive vs Classical Logic

Arguably, one of the most significant sources of controversy and debate in this area is the use of a non-classical logic for founding mathematics. The question of which (if any) is the correct logic for mathematics is a complex question beyond the scope of the present article. For that reason we will instead stick to some representative remarks and highlight how they pertain to constructive type theory.

Although classical theories are available, since our discussion here regards constructive type theory we must consider the use of a non-classical logic for founding mathematics. As we have seen, constructive type theory relies upon an intuitionistic logic and does not validate certain strictly classical inferences (such as double negation elimination or reductio). As we’ve also seen, this leads to some nice computational properties for the system since in order to talk about an object of a given kind one must provide a procedure for constructing it. Thus, in particular, every existential statement will be furnished with a procedure for constructing the object in question. Similarly, every proof of disjunction A ⋁ B will in particular provide a method for constructing either a proof of A or a proof of B. It is clear that this will have significant upshot for the computational properties of the system (although computational considerations do not necessarily adjudicate in favour of a constructive logic, again see Wadler (2015) ). The introduction rules associated with a type provide a method for actually constructing it, and the elimination rules provide a procedure for computing with the objects of a given type. Indeed, these are some of the central properties which made computer scientists so interested in exploring constructive type theory in the first place.

Despite these nice computational properties, it does raise a potential worry: namely that constructive type theory will be an inadequate foundation given that most of mathematics as it is actually practiced is classical. This may lead some to dismiss constructive type theory out of hand if they insist that a foundation must be capable of reconstructing all of existing mathematics as it is actually practiced. Were this insisted upon, then any theory cast in a non-classical logic would have to be immediately rejected.

However, the non-classicality of constructive type theory is not as significant of a barrier as one might think since constructive mathematics (for example as exemplified by Bishop (1967)) is a proper sub-theory of classical mathematics. That is, anything provable within constructive mathematics will also be a theorem of classical mathematics (although not vice-versa). This is a caveat worth emphasising, since although constructive type theory uses intuitionistic logic, this conservativeness is not shared by intuitionistic mathematics wherein one can famously derive results that are logically inconsistent with classical mathematics (for example, Brouwer’s fan theorem). Constructive type theory has been widely regarded as a successful formalisation of constructive mathematics. Nonetheless, its successes in this domain do not necessarily mean that it will be a suitable candidate for founding mathematics simpliciter. In particular, although constructive foundations will not allow the derivation of anything which is inconsistent with classical mathematics, one might fear that a foundational theory cast in a weaker logic will be insufficient for founding mathematics as a whole. In response to this, one can point out that it remains available to the constructivist to add a strictly classical rule (such as excluded middle) as a non-logical axiom of the system, and thereby ‘classicise’ the theory. One can even do so in something of a conditionalised manner. When confronted with a classical theorem of the form ‘if A then B’, the constructivist can recover the result by noting classical logic as an auxiliary hypothesis, and translate the statement to ‘if A and LEM then B’. In this way, one can recover the theorems of classical mathematics in a constructive system.

Of course, the assumption of classical mathematics as the default position can be questioned. Perhaps such an assumption unfairly stacks the deck against non-classical theories. Perhaps the ability to recover a great deal of mathematics combined with the computational properties of constructive type theory is enough to make this a preferable foundational proposal. Ultimately, the answer to this question will depend upon whether one is willing to accept a non-classical foundation, or whether one insists that the theory used to found mathematics must be strictly classical.

ii. Simplicity

At first glance, the language of constructive type theory can appear rather complicated. It is a formal system perhaps more reminiscent of a programming language than a mathematical language. Unlike first-order logic, which is somewhat bifurcated combining a system of proof (such as natural deduction) and a theory of meaning (such as Tarskian models), constructive type theory eschews the familiar syntax/semantics distinction. In type theory, everything happens purely syntactically – the behaviour of the system is dictated by rules governing which kinds of operations can and can’t be performed on well-formed formulae, all without the additional layer of interpretation on top of it.

This can make one’s first exposure somewhat jarring if one is expecting a theory with a sharply delineated syntax and semantics. However, this does not mean that there can be no semantic interpretation given for the theory. As seen in 5a, Martin-Löf’s meaning explanation is one possible way of interpreting the symbols of type theory, but there are others such as categorical and functional semantics available (one locus classicus for this being Lambek & Scot (1986), another being Streicher (1991)). That said, it is a familiar complaint that the language of types is far more complicated than first order language (Quine (1956), Florio (2023), Holmes (2025) ). In one sense, this is unsurprising. As we saw, finite type theory can be thought of as an -order logic, and thus will possess much more expressive power than first-order logic. But, even if this is correct there is of course the simple rejoinder than type theory – like any language – requires time, practice, and immersion in order to gain fluency. Thus, claims that the theory exhibits a higher degree of complexity than alternatives may not be an entirely justifiable criticism.

However, there does seem to be a more nuanced version of the criticism that might be offered. Namely, that there are many ideas and theorems of contemporary mathematics which appear relatively straightforward to represent in first-order logic plus set theory (or some alternative), but have a far less natural formalisation in type theory. This is because the model theory of first-order logic and sets is relatively standardised. This is not the case for type theory, though that is not to say that no good model theory for types exists. Rather there are several candidates each possessing their own relative merits for different purposes (for example contextual categories, locally cartesian closed categories, syntactic categories, and so forth.) Since there is no standardly agreed modeling of type theory, it is often unclear how one might best represent mathematics founded in type theory.

That said, proponents of type theory maintain that the apparent unintuitive formalisations of type theory really are only apparent. They maintain that like anything else, once you get used to working in the system these concerns dissipate. Therefore on this point is seems fair to wonder whether these criticisms of the apparent complexity of type theory are legitimate, or merely a product of when and how type theory is typically introduced. Overall however, the fact that alternative foundations seem to display a much more simple syntax and semantics than type theory is a potential source of criticism.

iii. Separation of Mathematics and Logic

As we noted at the beginning of this section, type theory originated with Bertrand Russell. It is therefore somewhat unsurprising given Russell’s prominent defence of logicism that in the theory of types mathematics itself is absorbed into the logical system. That is, unlike the other theories discussed thus far where one can separate the logical framework from the mathematical content of a theory, under this proposal mathematics is itself a part of logic.

This raises a familiar concern which has been previously levelled against second and higher-order logics. Many philosophers maintain that logic is topic-neutral, it has no particular subject matter and is thus applicable universally regardless of topic. Mathematics, however, is certainly not. Each branch of mathematics concerns itself with an explicit and well-defined subject matter (for example the integers) and therefore is not topic neutral. If this view regarding the subject matter of logic and mathematics is to be maintained, one may well find the use of types to be problematic as it seems to entail either a rejection of the topic-neutrality of logic, or a denial of the idea that mathematical theories possess a subject matter.

In the case of the theories we have discussed so far, one finds a clean divide between the language of first-order logic and the mathematical content of the theory (such as ZFC or ETCS). That is, the properly mathematical content of the proposed foundation is not to be found in the logic itself. This is not so with type theory. In a type-theoretic setting all of the mathematics one can capture is subsumed into the logical system itself. Therefore, if a type theoretic foundation is embraced, then any intuitive distinction between mathematics and logic cannot be easily maintained. Debates concerning the mathematical content of higher order logics are well known and ongoing (e.g. Shapiro (1991), Väänänen (2001), Väänänen (2012), ) but remain a potential source of dispute for type-theoretic foundations.

iv. Comparison with Sets

As in 4civ, it is worth briefly considering a direct comparison with set theory. To reiterate some of those concerns, we saw that the notions of a shared standard, generous arena, relative consistency strength, and consistency strength hierarchy have been espoused as important benefits of set theory. If the advocates of these desiderata are correct, it is worth taking a moment to consider how these concerns play out in the present context.

The idea of a shared standard of mathematical proof presents an interesting discussion given the strongly proof-theoretic character of type theory. As we’ve seen, constructive type theory not only underlies many contemporary proof-assistant and proof-verification softwares, but its most common semantics are understood entirely in proof-theoretic terms. Given these features, were constructive type theory to be accepted as the foundation for mathematics it would seem that it the theory would provide an even more stringent shared standard of proof than ZFC. As we’ve noted however, these properties come with potential costs. Namely, that theorems established using indirect proof methods would likely be deemed inadmissible by the standards of this foundation. As such, either these results would have to be given up, or the system be augmented with strictly classical principles. This may also be a problem if the generous arena is held as an important criteria for foundational theories, but this of course returns us to the discussion of 5ci and the more general debate about constructive vs. classical mathematics.

As far as measure of consistency/risk is concerned, a number of type-theoretic analogues to large cardinal axioms have been proposed and studied in detail (Rathjen et al. (1998)). It therefore seems reasonable to suggest that this theory is capable of meeting such a desideratum.

6. Univalence and Homotopy

So far this article has considered three rather longstanding candidate foundational theories. In this final section, we turn to consider the new kid on the block: Homotopy Type Theory and the Univalent Foundations project. In doing so, there are a few caveats to make clear up front. Firstly, this is very much a new area of research, and so comparatively little is known about it when considered against the decades of work in other candidate theories. Therefore, the content of this section still has a very strong feel of ‘work in progress’. Readers should not regard this as a deficit, but rather as an exciting opportunity. We are situated in a position to watch a new candidate foundational theory blossom and since it is such a young enterprise, who knows what exciting developments may arise as it comes to fruition.

To clarify some initial terminology. This section refers to both Homotopy Type Theory (HoTT) and Univalent Foundations (UF) somewhat interchangeably, though it should be noted that strictly speaking these are not identical. Rather, the researchers involved in both fields comprise a single community and the boundary between the two can be difficult to draw. In the spirit of seeking an accessible introduction to these ideas, and highlighting their philosophical content, we will occasionally gloss over certain distinctions between HoTT/UF in our discussion, which may lead to some slight inaccuracies when remarks are generalised across both.

a. What is HoTT/UF?

As with the other sections, this section begins with an overview of the key ideas involved. In keeping with the rest of the article, the aim is to provide an accessible overview of the main concepts involved and eschew technical detail, though citations will be provided for those seeking more precise formulations of the ideas.

HoTT/UF is a theory based upon a surprising connection between logic and topology. Specifically, between constructive type theory (as discussed in the previous section) and homotopy theory – a branch of algebraic topology concerned with continuous mappings between (and deformations of) certain kinds of topological spaces. The fact that a relationship exists between these areas is rather surprising. On the face of it, type theory and homotopy theory should have nothing to do with each other. The first concerns proof and verification procedures in computer science and logic, and the second concerns relationships and continuous deformations between topological spaces. It was no doubt a surprise then, that this connection was discovered. Since its discovery, this connection has received significant development from Awodey (2012), Awodey & Warren (2009), Voevodsky (2006), and Gambino & Garner (2008) which also included a ‘special year on Univalent Foundations of Mathematics’ at the Institute for Advanced Study in Princeton (2012/2013) the result of which is the Univalent Foundation Program (2013) .

This dual interpretation of types and homotopical spaces yields a natural reciprocity. On the one hand, interpreting type theory in homotopy theory allows one to construct new models of the logic and study them semantically using the language of homotopy. On the other, the typed theory provides a formal calculus for reasoning about abstract homotopical notions, and given the close connection between constructive types and computer assistants such as Rocq or Agda, opens up new avenues for proof construction and verification in homotopy theory. Thus, a first-pass answer to our question ‘what is HoTT/UF?’ is: an interpretation of dependent type theory via homotopy theory.

i. Homotopy Theory

Homotopy theory has its roots in algebraic topology, and features many striking connections with other areas of mathematics such as higher category theory and ∞-groupoids. Fundamentally, homotopy theory is concerned with spaces and continuous mappings between spaces. Two spaces X,Y are homotopy equivalent (written X≃Y ) if there are continuous mappings going back-and-forth between the spaces, which when composed stand in the special relationship of homotopy to the identity mappings on the spaces. This relationship exists when, given two continuous maps f,g: X → Y, a continuous map h: X ⤫ [0,1] → Y can be defined which satisfies h(x,0) = f(x) and h(x,1) = g(x). This new mapping can be thought of as a kind of continuous deformation of the first into the second. So, if there are continuous maps between two spaces which satisfy these conditions with respect to the identity mapping, we can say that the two spaces are homotopy equivalent, and we can think of them as differing only in terms of continuous deformation.

ii. Homotopy Type Theory

The fundamental idea which underlies HoTT is to interpret type theory within the framework of homotopy theory. More precisely, types are understood as spaces (or higher groupoids), terms are understood as points in space, and traditional logical constructions such as products and so forth. are understood as homotopy-invariant operations on spaces.

HoTT makes a number of conceptual revisions to preexisting ideas. Indeed, as was helpfully pointed out to me by an anonymous referee, it even revises the notion of ‘homotopy’ itself from the original point-set definition to the simplicial notion! Most importantly however, is the HoTT-theoretic understanding of Identity. Using the notation from the previous section, a: A is understood as meaning ‘a is a point of the space A’, a function term f: A → B is understood as a continuous function from one space to another, and the associated identity type (ID_A(a,b) declaring that two terms a,b of the type A are identical) is understood as representing the collection of paths from to within the space . This reconception of identity in terms of the existence of paths between points in a space is the fundamentally new idea which underlies much of the development of this field (Awodey et al. (2013) p.3). Indeed, when one understands identity as a path between points, one might wonder: ‘what makes this path unique?’. This question is the fundamental insight behind the Univalence axiom. In HoTT/UF, the concept of identity is generalised to allow two things to ‘be the same’ in more than one way (for more detail see Shulman (2018) p.37).

iii. The Univalence Axiom

The univalence axiom is not strictly required for the development of HoTT (though of course, as the name suggests, it is required for the development of univalent foundations). As such, not all advocates of HoTT wish to endorse the univalence axiom. On the one hand, leading figures claim it has far-reaching consequences which are natural, simplifying, and compelling, whereas soe philosophers argue that it should not be viewed as a fundamental part of the foundations of mathematics and instead regarded as an optional extra to be motivated on methodological grounds.

To explain the content of the axiom, we need first to introduce the notion of a universe from type theory. Universes (denoted U) are types whose terms are themselves also types. In order to avoid paradox, only certain so-called small types are allowed to feature as terms of a universe, and we thereby avoid a situation where U: U. Just as with other types, U has an associated identity type ID_U which defines the identity relation A = B between its terms A, B: U.

Now, under the homotopy interpretation of types as spaces, U itself is also a space, and the ‘points’ in are themselves spaces. Interpreting the identity type ID_U involves asking: what does it mean for there to be a path between spaces within U? The answer given by the Univalence axiom is that these paths correspond to homotopy equivalences, that is, there is a path from A to B iff A ≃ B.

To put this more precisely, given any small types A, B: U, there is not only the type of identifications of A, B: U given by ID_U, but there is also a more general equivalence type Eq(A,B) of equivalences between A and B.

Since we know that the identity mapping is itself an equivalence relation, there is a canonical mapping:

Γ: ID_U(A,B) → Eq(A,B)

The univalence axiom declares that this mapping Γ is itself an equivalence. For this reason, the univalence axiom is often stated more succinctly as:

UA: (A = B) ≃ (A ≃ B)

Or informally: identity is equivalent to equivalence. As the authors of make clear, this is not collapsing the idea of equivalence to that of identity. Rather, the direction is the other way around: this axiom actually expands the formal concept of identity to coincide with that of a more general equivalence (see Univalent Foundations Program (2013) pp.4-5). The result is that equivalent types are identical. As far as traditional mathematical logic is concerned this is a rather radical proposal: it implies that isomorphic objects can actually be identified with one another.

In essence then, given a universe U, under the Univalence Axiom the following three notions are all equivalent:

- Identity: for A = B for A,B: U
- Path p: p: A ⤳ B(the existence of a path from A to B in U)
- Homotopical Equivalence: A ≃ B for A,B: U.

It is in this way that UF formalises the idea that different mathematical objects can ‘be the same’ in more than one way. The result is a fascinating system which continues to develop and bear fruit. Indeed, one notable development due to Cohen et al. (2016) is that under the cubical interpretation of HoTT, the univalence axiom actually becomes provable as a theorem. As the HoTT/UF research program grows, it will no doubt continue to challenge orthodox mathematical understanding.

For those readers seeking to go beyond the material presented here, there are a number of recommendations. Original work by Awodey & Warren (2009), Voevodsky (2006), Awodey et al. (2013) is both detailed and concise. A more gentle introduction to some of the type-theoretic aspects can be found in Ladyman & Presnell (2014). Unquestionably however, at the time of writing the go-to source for substantially developed material on HoTT/UF is The Univalent Foundations Program (2013).

b. A Unique Foundational Perspective

Like our other candidate foundations, HoTT is capable of capturing a great deal of mathematics. In particular, HoTT/UF is able to define a theory roughly equivalent to ETCS (see Univalent Foundations Program (2013) p.6, Shulman (2018) p.43). To be a little bit more precise here, ‘classical’ versions of HoTT/UF (those which have the axiom of choice and excluded middle) will define a universe of -groupoids which properly contains a universe of sets satisfying the ECTS axioms (for HoTT/UF without choice/excluded middle, the universe of sets will not satisfy ECTS proper, but rather an intuitionistic variant. Again, we refer the interested reader to Shulman (2018) for further details). Given this degree of expressibility it seems that once again there is little to break the tie on these grounds. However, HoTT/UF provides a unique perspective on foundational issues, one which diverges quite significantly from the proposals discussed so far.

The computational properties of HoTT yielded by the underlying type theory is one of the primary motivations suggested by Voevodsky. Historically speaking, computability is very much a new criteria for evaluating foundational proposals. The desire for a foundation which can be implemented by a machine has only arisen since the construction of such machines, but as discussed in 2ciii, it nonetheless has some important payoffs. In the last few decades, the desire for a computer program to execute a mathematical procedure such as proof verification has become much more significant. Throughout the history of mathematics, the mathematical community has relied upon sociological standards and checks for determining the legitimacy of a proof (papers are submitted to journals which are refereed by experts, theorems are discussed at conferences and so forth). However, as mathematics developed in the twentieth century this became much more demanding. For example, in discussing the work of Grothendieck, Burgess (2015) remarks that ‘the intellectual faculties are strained to their uttermost limit’ (p.176), and this strain is only exacerbated by the results building upon his research. In particular, Voevodsky noted in his own work (and that of his peers) concerning cohomology and K-theory that the ideas were so complicated mistakes were beginning to slip through the cracks: ‘in 1998 a counterexample was reported to a 1989 paper of Michael Kaparonov and Voevodsky, but because of the complexities involved, Voevodsky reports that he didn’t believe it himself until 2013!’ (Maddy (2019) p.305). This is not an isolated incident, traditional sociological checks were no longer guarding against mistakes, and as such a need to address this problem emerged:

But to do the work at the level of rigor and precision I felt necessary would take an enormous amount of effort and would produce a text that would be very hard to read. And who would ensure that I did not forget something and did not make a mistake, if even the mistakes in much more simple arguments take years to uncover? (Voevodsky (2014) p.8).

These issues led Voevodsky to propose a new foundational goal: the foundation should provide a systematic method of proof checking and verification. As already discussed, it is in principle possible to formalise any given area of mathematics within say ZFC, but if implementation into a proof assistant is important, then this formalisation is not enough. What is required on this understanding is a foundation which can represent the actual proofs of mathematicians – not their set-theoretic surrogates: ‘A tool that can be employed in everyday mathematical work’ (ibid).

This is precisely what HoTT/UF is intended to provide. The computational character of type theory lends itself neatly to computational procedures. This motivation is articulated by a number of HoTT theorists:

‘oTT can be fully formalized in a computer programming language that can be used directly to construct completely formal proofs to check informal reasoning… This is a major motivation for HoTT (Ladyman & Presnell(2018) p.410).

One of Voevodsky’s goals (as we understand it) is that in a not too distant future, mathematicians will be able to verify the correctness of their own papers by working within the system of univalent foundations formalized in a proof assistant, and that doing so will become natural even for pure mathematics (Awodey et al.(2013) p.5).

its rules can be read as defining a programming language that can actually be executed by a computer.’ (Shulman(2018) p.47).

Of course, as we saw in the previous section, these computational properties in themselves are not unique to HoTT. Constructive type theory has been extensively developed and investigated independently of the homotopical interpretation for decades, and has served as the basis for many computer-assisted proof verification programmes. However, the computational aspect of HoTT/UF is nonetheless somewhat unique in terms of direction of proof. As the authors of Univalent Foundations Program (2013) remark, many of the results established in the book were actually first completed in a fully formalised manner via a proof-assistant software. The job of the mathematician was then to ‘unformalise’ the results for the first time (p.8). This is a reversal of the usual practice of mathematics whereby one typically proves a result informally before establishing its formal counterpart. If HoTT/UF catches on, we could potentially see a widespread change in everyday mathematics where results are first established in an automated theorem prover, verified for correctness by a proof checker, and then de-formalised by the mathematician for presentation to their peers.

Nevertheless, these computational properties are not the only factors driving investigation in this area. Many HoTT theorists are independently motivated to investigate HoTT as a synthetic theory (that is, involving direct manipulation and encoding of mathematical structure without a reduction to some more fundamental entity) with an internal language for thinking ‘within’ certain higher toposes. This provides an interesting point of contrast to other foundational proposals such as set theory. Set-theoretic foundations can be seen as something of a ‘bottom-up’ approach whereby a mathematical object is broken down into its constituent materials (or at least set-theoretic surrogates thereof). HoTT, by contrast, adopts a more ‘top-down’ strategy: taking the objects of mathematics as given, and seeking to describe their structural features in terms of how they map to and from one another. These computational and algebraic motivations combine to produce an interesting new approach to foundational questions.

To sum up, HoTT/UF has the expressive resources to capture a great deal of mathematics. It facilitates automatic verification of proofs, and provides a synthetic ‘top-down’ approach to mathematics. The language is subtle enough to make a number of fine-grained distinctions employing the flexible algebraic character of homotopy theory, and unifies the mathematical language with a strongly proof-theoretic orientation to logic via constructive type theory. Taken together this seems to significantly distinguish the motivations of this school from other foundational programmes, and indeed shows a different orientation toward foundational disputes. To put this more succinctly: advocates of HoTT/UF are not seeking reform, but revolution in the foundations of mathematics.

c. Questions and Debate

HoTT/UF raises a number of interesting issues both for mathematical practice and for the philosophy of mathematics. In this final subsection, we will consider some of the criticisms that might be leveled against this proposal. Given that this proposal builds off of material covered in the previous section, certain criticisms of constructive type theory may also be levelled against HoTT/UF (for example the use of a non-classical logic). Despite this, we will focus on issues and concerns with a direct bearing upon HoTT/UF. As with other sections, we will also consider a more direct comparison with set theory. Again, as previously emphasised, this article presents ideas for the reader to consider, and it is not intended to adjudicate the issues.

i. Relationship with Other Computational Proposals

Although homotopy type theory has certainly stimulated a great deal of discussion it is still a relatively minor player in the foundational literature. One reason for this is that despite the promise of the computational properties of the system, at the time of writing no large-scale formalisation project has been completed in a homotopical proof assistant. Indeed, extant high-profile cases of computer formalisation such as the proof of the four-colour theorem and the Kepler Conjecture have utilised proof assistant technologies which do not include any homotopical features. Although these particular results were established prior to the development of HoTT they nevertheless underline that as far as research involving proof assistant software has actually been conducted, the majority of significant cases have not involved any homotopy theory. Moreover, the current fastest growing functional programming language for mathematics (Lean) in its current incarnation is incompatible with the homotopical interpretation. As far as the development of computational foundations goes, HoTT remains something of a minor thread.

ii. Simplicity

A second reason for HoTT’s minority status is that comparatively, relatively little is known about it. While set theory extends back to the late nineteenth century, and category theory to the mid-twentieth, HoTT/UF has only emerged in the last two decades. This has led some people to express reservation towards the HoTT/UF proposal until more is known. This by itself should not be viewed as a serious criticism. Presumably, with time, further investigation will occur and a greater body of results will be established giving us a better idea of how mathematics plays out on this picture.

Nevertheless, there is a more substantial criticism in this vicinity. The relative lack of information regarding HoTT/UF is of course due to the fact that relatively few people have investigated it. However, it seems to be the case that relatively few people are capable of investigating it. Herein lies the potential problem: compared to alternative proposals, this theory appears to have a rather high barrier for entry.

To contribute to the HoTT/UF programme requires a substantial understanding not only of type-theory and mathematical logic, but also detailed knowledge of homotopy theory and algebraic topology more generally. Even the basic concepts and theorems of HoTT/UF involve a relatively high degree of conceptual complexity making it difficult for people understand what is going on in this area. This is particularly problematic when contrasted with other proposals. While many working mathematicians outside of foundations display a more than adequate grasp of the fundamental concepts of sets or categories, the subject matter of HoTT/UF is far less intuitive. The fact that HoTT/UF requires such a great deal of background knowledge prior to its study might be seen as an impediment for the program. The criticism, in essence then, is somewhat familiar from general considerations of theoretical virtues; all things being equal, we tend to prefer a more simple theory over a more complex one. According to this view, the fundamental ideas and concepts underlying set theory and category theory are comparatively simple and natural for the mathematician, and given that each of these can equally well reconstruct mathematical practice they ought to be preferred on grounds of simplicity.

There are a few things that one might say to this. Firstly, it is perhaps to be expected that in such a young field only a small number of people can engage with the ideas invovled, since it is very much cutting-edge mathematics. However, this does not mean that it will always be so. As the field develops over time the ideas may become more widespread and familiar in a way which could lead to them seeming equally conceptually simple or natural. This response then views the criticism as simply another iteration of the idea that HoTT/UF is to be rejected because it is relatively new. Secondly, the advocate of HoTT/UF might agree that all things being equal we should prefer a more simple theory over a more complex one (pending a suitable elaboration of the relevant notion of simplicity). However, they would deny that all things are indeed equal, and point to the fact that HoTT lends itself to proof-checking procedures that more traditional proposals (that is, set theory and category theory) do not (or at least do not appear to). Therefore, the increase in conceptual complexity is a small price to pay. Finally, there is the question of why one should expect the very foundations of mathematics to be conceptually simple at all. Perhaps if one has a robustly metaphysical or epistemological conception of ‘foundation’ in mind, this might follow; but as we have seen many contemporary foundationalists reject such a conception. Therefore, one might think that the demand for simplicity is unjustified.

iii. Autonomy

The previous considerations of simplicity raise a related question of conceptual autonomy (and therefore considerations of autonomy more generally). Recall that a theory is conceptually autonomous if it is possible to understand the concepts involved in that theory without prior grasp of some concepts from another theory. Quite clearly, since HoTT is a homotopical interpretation of dependent type theory, it requires the conceptual apparatus of homotopy theory. Indeed, using the framework of Linnebo & Pettigrew(2011) from sections 2cb and 4cb, it is not clear that HoTT can be regarded as logically autonomous or as having justificatory autonomy either.

The autonomy of HoTT is a central problem for any advocate who holds autonomy as an important foundational desideratum. Whether or not it is possible to articulate HoTT in a way which does not presuppose a prior grasp of other areas of mathematics is unclear. Ladyman & Presnell (2018) take this as a central challenge for HoTT’s foundational status, and try to provide an autonomous rendering of the central ideas. Their approach is to interpret both types and tokens as concepts, in order to give an autonomous intensional theory of HoTT (see section 7 of their paper). Of course, whether this is the correct or even an appropriate way of interpreting the theory is highly contentious.

Ultimately, whether an autonomous interpretation of HoTT/UF can be given is still very much a matter of dispute.

The previous considerations of simplicity raise a related question of conceptual autonomy (and therefore considerations of autonomy more generally). Recall that a theory is conceptually autonomous if it is possible to understand the concepts involved in that theory without prior grasp of some concepts from another theory. Quite clearly, since HoTT is a homotopical interpretation of dependent type theory, it requires the conceptual apparatus of homotopy theory. Indeed, using the framework of Linnebo & Pettigrew(2011) from sections 2cii and 4cii, it is not clear that HoTT can be regarded as logically autonomous or as having justificatory autonomy either.

Ultimately, whether an autonomous interpretation of HoTT/UF can be given is still very much a matter of dispute.

iv. Assertion

As we saw when considering category theory, there is a question of whether the axioms of a proposed foundation are suitably assertory. Generally, the standard axiomatisation of set theory is seen as strongly assertory, in that the existence of certain sets follows immediately from the axioms. This may naturally lead one to wonder about the entities postulated by HoTT/UF. We’ve seen that types are the primitive objects of the theory. At a low level, HoTT/UF includes a small number of very simple unit and zero types. From there, one moves through inductive types forming products, co-products, a type of natural numbers, and so on to produce a theory of roughly equivalent strength to ETCS. Most of the objects used in everyday mathematics can be constructed in the type of sets. One can then further augment the system with principles which yield higher algebraic structures (Buchholtz (2019)). In general, anything that can be captured in ETCS can also be captured in HoTT/UF.

Nevertheless, the top-down approach of HoTT has lead some authors to worry about the assertory capabilities of the theory (for example Ladyman & Presnell (2018)). HoTT/UF as a theory is capable of describing the behaviour of certain mathematical entities in homotopical terms, but without supplementation by other type forming operators it does not dictate one way or the other whether there are such entities. Philosophers sympathetic to this criticism view HoTT as providing a version of ‘if thenism’: if there are any structures of a given kind, then they can be characterised homotopically. In response to this, advocates of HoTT/UF have claimed that this is a feature of the system rather than a bug, and that making no existential assertions allows the theory to remain ontologically neutral compared to alternatives like ZFC which are often criticised for having Platonistic overtones (see Ladyman & Presnell (2018) p.391). Ultimately however, this is an instance of a more general philosophical question of whether mathematical axioms need to have an assertory character (again, the reader is referred to Hellman (2003), Feferman (1980) , Maddy (Maddy, 2011) for more).

v. Constructivity

As seen in 5ci, the type theory upon which HoTT/UF is based is cast in a non-classical logic. Many of the remarks made in that section will apply mutatis mutandis to the discussion of this section, particularly with regards to indirect methods of proof such as classical proof by contradiction or double negation elimination. As such, we will try to keep the discussion of this section pertinent to HoTT/UF, but with the acknowledgment that these issues are much more general.

The constructive logic used in HoTT is a proper subtheory of full classical logic, so once again anything derivable in this system will also be a result of classical logic (though not necessarily vice versa), and the system can be augmented with strictly classical principles taken as non-logical axioms. One method for doing this involves noting that the homotopy types are stratified and restricting attention to only types of a certain strata. In particular, one notices that the so-called homotopy(-1) types (otherwise called ‘mere propositions’) are always either empty or contractible. One may then interpret these possibilities in terms of bivalent truth values, and add to the theory the law of excluded middle as an axiom governing the behaviour of the types at this level of stratification (for details see Univalent Foundations Program (2013) p.9). Given these sorts of processes, HoTT/UF may be seen as more friendly to classical mathematics than the purely constructive type theory upon which it is based. Indeed, according to Awodey (2019), the homotopy interpretation allows the mathematician to justify the addition of non-constructive principles to the system on the basis of homotopical intuitions, thus allowing the system to formalise various classical spaces and constructions (p.14). These classical versions inevitably forego some of the computational properties of the system (in the sense that not every proof is executable as a program) but they do maintain the usability of HoTT/UF as a formalization of mathematics utilisable by proof assistants. The key point is that principles of classical reasoning can be consistently added to HoTT/UF so as to yield a formalisation of classical mathematics (see also Shulman (2018) p.46).

One thing worth noting with regards to the choice of logic, is that as discussed in 4.1, the type theory which underlies HoTT/UF has been often been justified in terms of Martin-Löf’s ‘meaning explanation’ (for example Martin-Löf (1996)). Such an explanation is not compatible with a classical understanding of logical rules and can only justify the more direct methods found in a constructive theory. As such, given that HoTT/UF appears more amenable to classical logic, it remains an open question whether it admits of a similar ‘meaning explanation’ (this question is discussed in Bentzen(2020) ). However, given that the semantic interpretation of the theory is homotopical, it is unclear whether such a ‘meaning explanation’ needs to be sought out.

Ultimately, the question of whether or not HoTT/UF should be interpreted constructively or classically turns on the much broader question of which (if any) is the correct logic for mathematical reasoning.

vi. Comparison with Set Theory

As with other sections, it is worth briefly considering a direct comparison with set theory. To reiterate some of the ideas espoused in favour of set theory, we saw that a shared standard, generous arena, relative consistency strength, and consistency strength hierarchy have been put forth. If we are correct in identifying these features as important foundational desiderata, it’s worth pausing to consider how they play out under HoTT/UF.

The idea of a shared standard is an especially interesting case to begin with. As we saw in 2ciii, and 6b, many HoTT/UF theorists (following Voevodsky) have placed a strong emphasis on the potential of HoTT as a working foundation for the verification of mathematical proofs. Were this to be accepted as the preferred foundational theory, it would arguably lead to a more widely implementable shared standard of proof for mathematics. Given at least some of the claims made by the researchers in this area, it would seem that HoTT/UF scores rather highly on the desideratum of a shared standard of proof.

The idea of a generous arena is somewhat less clear. As noted, the types in HoTT/UF can yield a theory equivalent to ETCS (and given that ETCS is equivalent to ZFC-replacement) it would therefore seem that HoTT/UF can deliver a great deal of mathematics. Moreover, given the fact that HoTT can be ‘classicised’ it would seem that it provides a potentially flexible foundation for large swathes of both classical and constructive mathematics. So, if one is insistent that the unaugmented base theory serve as a foundation, this proposal will fare less well on the standard of generous arena, but given the strengthenings available, it’s unclear how or why one might justifiably insist upon the base theory being the only legitimate foundation.

As far as measure of consistency/risk is concerned, HoTT is in an interesting position. It is unclear whether something like a large cardinal hierarchy can be captured directly in the system, although given the type-theoretic analogues studied in Rathjen et al. (1998) there seems to be no in-principle barrier if these results can be given a homotopical interpretation (perhaps also certain large toposes available within HoTT can serve as a surrogate for particular large cardinals). So, if measure of risk is understood in terms of an external standard against which our theories can be compared, it’s not yet clear how to judge HoTT.

However, it is possible that this criterion be inverted. Rather than rely on a hierarchy external to the theory as the preferred measure of risk, one might argue instead that the more appropriate notion is to stick to only claims that are strongly verifiable. If this were accepted as the relevant notion, perhaps HoTT/UF would fare better than traditional set-theoretic proposals, given that HoTT/UF has strong verifiability properties.

This brings us once again to the ‘top-down’ vs ‘bottom-up’ conception of a foundation. On the set-theoretic proposal one seeks an ever-increasing hierarchy of theories, each one capable of deriving facts about the theories below it in the hierarchy. In contrast, one possible proposal for HoTT/UF is to start with a theory which is more epistemically secure (given the methods of verification) and understand the measure of risk as concerning how ‘far away’ each further theory strays from this base. Ultimately this debate is yet to be conducted.

d. A Brief Appraisal

In sum, the HoTT/UF program offers yet another radically different perspective on foundational issues in mathematics. It draws together insights from both logic and algebraic topology to elucidate surprising connections which call into question certain assumptions implicit in traditional foundational debates. Given the relative youth of the theory, and the rate at which work is being conducted, it is likely that in the future much of the present discussion may seem dated. Nevertheless, as things currently stand, there is much more to be established, both in terms of the mathematical consequences of the theory as well as their philosophical implications.

7. Conclusion

To condense the main themes of discussion in this article, we have seen that the foundations of mathematics remains a vibrant and dynamic area of interdisciplinary research bringing together mathematicians, philosophers, and computer scientists with no signs of slowing down. Although different candidate foundations have been put forth, there are longstanding conceptual questions which remain to be settled. Articulating exactly what is required of a foundation philosophically is a tricky task, and the question of what features a foundational theory ought to possess remain unresolved. We’ve seen that advocates of differing proposals often emphasise different features a foundation for mathematics might have, and this can shape resultant theory quite drastically. Although some of the philosophical considerations are longstanding, ongoing technical developments serve to further highlight the variety and importance of contemporary debate. As foundational proposals evolve, opportunities for new insights and new ideas continue to emerge. Thus, the subject offers great opportunity for a wide range of contributions from many different perspectives.

8. References and Further Reading

Aczel, P. (1999). On Relating Type Theories and Set Theories. In Thorsten Altenkirch, Bernhard Reus, Wolfgang Naraschewski (Eds.), Types for Proofs and Programs (pp. 1–18). Springer Berlin Heidelberg.
Altenkirch, T. (2019). Naive Type Theory. In Stefania Centrone, Deborah Kant, Deniz Sarikaya (Eds.), Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts. Springer International Publishing.
Andrews, P. (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof (Applied Logic Series). (second ed.). Springer Dordrecht.
Antos, C., Friedman, S., Honzik, R., & Ternullo, C. (2015). Multiverse Conceptions in Set Theory. Synthese, 192(8), 2463–2488.
Avigad, J., & Feferman, S. (1998). {G\. In Samuel R. Buss (Ed.), Handbook of Proof Theory (pp. 338–400). Elsevier Science Publishing.
Awodey, S. (1996). Structure in Mathematics and Logic: A Categorical Perspective. Philosophia Mathematica, 4(3), 209–237. https://doi.org/10.1093/philmat/4.3.209
Awodey, S. (2004). An Answer to Hellman’s Question: Does Category Theory Provide a Framework for Mathematical Structuralism?. Philosophia Mathematica, 12(1), 54–64.
Awodey, S. (2006). Category Theory. Oxford, England: Oxford University Press.
Awodey, S., & Warren, M. (2009). Homotopy Theoretic Models of Identity Types. Mathematical Proceedings of the Cambridge Philosophical Society, 146(45), 45–55.
Awodey, S. (2011). From Sets to Types, to Categories, to Sets. In Giovanni Sommaruga (Ed.), Foundational Theories of Classical and Constructive Mathematics (pp. 113–125). Springer Netherlands.
Awodey, S. (2012). Type Theory and Homotopy. In P. Dybjer, Sten Lindström, Erik Palmgren, G. Sundholm (Eds.), Epistemology versus Ontology: Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf (pp. 183–201). Dordrecht: Springer Netherlands.
Awodey, S., Pelayo, A., & Warren, M. (2013). Voevodsky’s Univalence Axiom in Homotopy Type Theory. Notices of the American Mathematical Society, 60(9), 1164–1167.
Awodey, S. (2014). Structuralism, Invariance, and Univalence. Philosophia Mathematica, 22(1), 1–11.
Awodey, S. (2019). Mathesis Universalis and Homotopy Type Theory. In Stefania Centrone, Sara Negri, Deniz Sarikaya, Peter M. Schuster (Eds.), Mathesis Universalis, Computability and Proof. Springer Verlag.
Bagaria, J. (2023). Set Theory. In Edward N. Zalta, Uri Nodelman (Eds.), The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University.
Bagaria, J., & Ternullo, C. (2023). Steel’s Programme: Evidential Framework, The Core and Ultimate-L. The Review of Symbolic Logic, 16(3), 788–812.
Baldwin, J. T. (2018). Model Theory and the Philosophy of Mathematical Practice: Formalization Without Foundationalism. Cambridge University Press.
Barton, N. (2021). Indeterminateness and `The’ Universe of Sets: Multiversism, Potentialism, and Pluralism. In Melvin Fitting (Ed.), Research Trends in Contemporary Logic (pp. 105–182). College Publications.
Benacerraf, P. (1965). What Numbers Could not Be. The Philosophical Review, 74(1), 47–73.
Benacerraf, P. (1973). Mathematical Truth. Journal of Philosophy, 70(19), 661–679.
Benacerraf, P., & Putnam, H. (1984). Philosophy of Mathematics: Selected Readings. Englewood Cliffs, NJ, USA: Cambridge University Press.
Bentzen, B. (2020). What Types Should Not Be. Philosophia Mathematica, 28(1), 60–76.
Bishop, E. (1967). Foundations of Constructive Analysis. New York, NY, USA: McGraw-Hill.
Bishop, E. (1985). Schizophrenia in Contemporary Mathematics. Contemporary Mathematics, 39, 1–32.
Boole, G. (1847). The Mathematical Analysis of Logic. Oxford: Cambridge University Press.
Bridges, D., & Richman, F. (1987). Varieties of Constructive Mathematics. New York: Cambridge University Press.
Buchholtz, U. (2019). Higher Structures in Homotopy Type Theory. In Stefania Centrone, Deborah Kant, Deniz Sarikaya (Eds.), Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts. Springer International Publishing.
Burgess, J. P. (2015). Rigor and Structure. Oxford, England: Oxford University Press UK.
Burgess, J. (2018). Putnam on Foundations: Models, Modals, Muddles. In Geoffrey Hellman, Roy Cook (Eds.), Hilary Putnam on Logic and Mathematics. Springer International Publishing.
Button, T., & Walsh, S. P. (2018). Philosophy and Model Theory. Oxford, UK: Oxford University Press.
Buzzard, K. (2024). Mathematical Reasoning and the Computer. Bulletin of the American Mathematical Society, 61(2), 251–268.
Cantor, G. (1891). Über eine elementare Frage der Mannigfaltigskeitslehre. Jahresbericht der Deutschen Mathematiker-Vereinigung, .
Centrone, S., Kant, D., & Sarikaya, D. (2019). Introduction. In Stefania Centrone, Deborah Kant, Deniz Sarikaya (Eds.), Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts. Springer International Publishing.
Church, A. (1936). A Note on the Entscheidungsproblem. Journal of Symbolic Logic, 1(1), 40–41. https://doi.org/10.2307/2269326
Church, A. (1940). A Formulation of the Simple Theory of Types. The Journal of Symbolic Logic, 5(2), 56–68.
Cohen, P. (1963). The Independence of the Continuum Hypothesis. Proceedings of the National Academy of Sciences USA, 50(6), 1143–1148.
Cohen, P. (1964). The Independence of the Continuum Hypothesis II. Proceedings of the National Academy of Sciences USA, 51(1), 105–110.
Cohen, C., Coquand, T., Huber, S., & Mörtberg, A. (2016). Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. https://arxiv.org/abs/1611.02108
Constable, R. L. (1998). Types in Logic, Mathematics and Programming. In Samuel R. Buss (Ed.), Handbook of Proof Theory (pp. 683–786). Elsevier Science Publishing.
Constable, R. L. (2017). Formal Systems, Logics, and Programs. In Melvin Fitting, Brian Rayman (Eds.), Raymond Smullyan on Self Reference (pp. 23–38). Cham: Springer International Publishing.
Crosilla, L. (2024). Bishop’s Mathematics: A Philosophical Perspective. In Laura Crosilla (Ed.), Handbook of Bishop’s Mathematics. Cambridge University Press.
Cunningham, D. (2024). Set Theory. In The Internet Encyclopedia of Philosophy.
Curry, H. B. (1934). Functionality in Combinatory Logic. Proceedings of the National Academy of Sciences of the United States of America, 20(11), 584–590.
Dedekind, R. (1872). Stetigkeit und irrationale Zahlen. In R. Fricke, E. Noether, Ö. Ore (Eds.), Gesammelte Mathematische Werke. Braunschweig: Vieweg; reprinted by New York: Chelsea Publishing Company, 1969.
Detlefsen, M., & Arana, A. (2011). Purity of Methods. Philosophers’ Imprint, 11.
Dybjer, P., & Palmgren, E. (2024). Intuitionistic Type Theory. In Edward N. Zalta, Uri Nodelman (Eds.), The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University.
Dzamonja, M. (2019). A New Foundational Crisis in Mathematics, Is It Really Happening?. In Stefania Centrone, Deborah Kant, Deniz Sarikaya (Eds.), Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts (pp. 255–269). Springer International Publishing.
Enderton, H. (1977). Elements of Set Theory. New York: Academic Press.
Ernst, M. (2015). The Prospects of Unlimited Category Theory: Doing What Remains to Be Done. Review of Symbolic Logic, 8(2), 306–327.
Ernst, M. (2017). Category Theory and Foundations. In Elaine Landry (Ed.), Categories for the Working Philosopher. Oxford University Press.
Escardó, M. H. (2019). Introduction to Univalent Foundations of Mathematics with Agda. CoRR, abs/1911.00580. http://arxiv.org/abs/1911.00580
Feferman, S. (1980). Categorical Foundations and Foundations of Category Theory. In R. E. Butts, J. Hintikka (Eds.), Logic, Foundations of Mathematics, and Computability Theory (pp. 149–169). Springer.
Feferman, S. (2011). Enriched Stratified Systems for the Foundations of Category Theory. In Giovanni Sommaruga (Ed.), Foundational Theories of Classical and Constructive Mathematics (pp. 127–143). Springer Netherlands.
Florio, S. (2023). On Type Distinctions and Expressivity. Proceedings of the Aristotelian Society, 123(2), 150–172.
Frege, G. (1879). Begriffsschrift. In Jean Van Heijenoort (Ed.), From Frege to Gödel (pp. 1–83). Cambridge: Harvard University Press.
Gambino, N., & Garner, R. (2008). The Identity Type Weak Factorisation System. Theoretical Computer Science, 409(1), 94–109.
Gödel, K. (1931). On Formally Undecidable Propositions of Principia Mathematica and Related Systems. New York, NY, USA: Basic Books.
Gödel, K. (1947). What is Cantor’s Continuum Problem?. The American Mathematical Monthly, 54(9), 515–525.
Gödel, K. (1986). Collected Works, Volume 1: Publications 1929-1936. Oxford, England: Clarendon Press.
Gentzen, G. (1969). The Collected Papers of Gerhard Gentzen. Amsterdam: North-Holland Pub. Co.
Griffin, O. (2024). The Problem of Isomorphic Structures. Thought\: A Journal of Philosophy, 13(1), 45–58.
Hamkins, J. D. (2012). The Set-Theoretic Multiverse. Review of Symbolic Logic, 5(3), 416–449.
Heijenoort, J. V. (1967). {From Frege to G\. Cambridge: Harvard University Press.
Hellman, G. (2003). Does Category Theory Provide a Framework for Mathematical Structuralism?. Philosophia Mathematica, 11(2), 129–157.
Hellman, G. (2011). Foundational Frameworks. In Giovanni Sommaruga (Ed.), Foundational Theories of Classical and Constructive Mathematics (pp. 53–69). Springer Netherlands.
Hellman, G., & Shapiro, S. (2017). Varieties of Continua: From Regions to Points and Back. Oxford, England: Oxford University Press.
Henkin, L. (1950). Completeness in the Theory of Types. Journal of Symbolic Logic, 15(2), 81–91.
Holmes, M. R. (2025). Alternative Axiomatic Set Theories. In Edward N. Zalta, Uri Nodelman (Eds.), The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University.
Howard, W. A. (1980). The Formulae-as-Types Notion of Construction. In Haskell Curry, J. Roger Hindley, Jonathan P. Seldin (Eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press.
Kamareddine, F., Laan, T., & Nederpelt, R. (2005). A Modern Perspective on Type Theory: From its Origins until Today (Applied Logic Series). Springer Dordrecht.
Kanamori, A. (2003). The Higher Infinite Large Cardinals in Set Theory from Their Beginnings (Springer monographs in mathematics). (second ed.). Springer Berlin, Heidelberg.
Klement, K. (2024). Russell’s Paradox. In The Internet Encyclopedia of Philosophy.
Koellner, P. (2010). Independence and Large Cardinals. In Stanford Encyclopedia of Philosophy.
Kunen, K. (1980). Set Theory: An Introduction to Independence Proofs. Amsterdam: North Holland.
Kunen, K. (2009). The Foundations of Mathematics (Studies in Logic). College Publications.
Ladyman, J., & Presnell, S. (2014). A Primer on Homotopy Type Theory Part 1: The Formal Type Theory. https://philsci-archive.pitt.edu/11157/
Ladyman, J., & Presnell, S. (2015). Identity in Homotopy Type Theory, Part I: The Justification of Path Induction. Philosophia Mathematica, 23(3), 386–406.
Ladyman, J., & Presnell, S. (2016). Identity in Homotopy Type Theory: Part II, the Conceptual and Philosophical Status of Identity in Hott. Philosophia Mathematica, 24(2), 199–228.
Ladyman, J., & Presnell, S. (2018). Does Homotopy Type Theory Provide a Foundation for Mathematics?. British Journal for the Philosophy of Science, 69(2), 377–420.
Ladyman, J., & Presnell, S. (2019). Universes and Univalence in Homotopy Type Theory. Review of Symbolic Logic, 12(3), 426–455.
Lambek, J., & Scott, P. J. (1986). Introduction to Higher Order Categorical Logic. Cambridge University Press.
Lambek, J., & Scott, P. (2011). Reflections on the Categorical Foundations of Mathematics. In Giovanni Sommaruga (Ed.), Foundational Theories of Classical and Constructive Mathematics (pp. 171–186). Springer Netherlands.
Landry, E. M. (2017). Categories for the Working Philosopher. Oxford, England: Oxford University Press.
Lane, S. M., & Eilenberg, S. (1945). General Theory of Natural Equivalences. Transactions of the American Mathematical Society, 58, 231–294.
Lane, S. M. (1971). Categories for the Working Mathematician. Springer.
Lane, S. M. (1971). Categorical Algebra and Set-Theoretic Foundations. In Dana Scott, Thomas Jech (Eds.), Axiomatic Set Theory, Proceedings of the Symposium in Pure Mathematics of the AMS UCLA 1967 (pp. 231–240). Providence: AMS.
Lane, S. M., & Moerdijk, I. (1994). Sheaves in Geometry and Logic: A First Introduction to Topos Theory (Universitext). Springer.
Lawvere, F. W. (1964). An Elementary Theory of the Category of Sets. Proceedings of the National Academy of Sciences of the United States of America, 52(6), 1506–1511.
Lawvere, F. W. (1966). The Category of Categories as a Foundation for Mathematics. In S. Eilenberg, D. K. Harrison, S. MacLane, H. Röhrl (Eds.), Proceedings of the Conference on Categorical Algebra (pp. 1–20). Berlin, Heidelberg: Springer Berlin Heidelberg.
Leinster, T. (2014). Basic Category Theory (Cambridge Studies in Advanced Mathematics). Cambridge University Press.
Levy, A. (1979). Basic Set Theory. Berlin: Springer.
Linnebo, O., & Pettigrew, R. (2011). Category Theory as an Autonomous Foundation. Philosophia Mathematica, 19(3), 227–254. https://doi.org/10.1093/philmat/nkr024
Linsky, B., & Irvine, A. D. (2026). Principia Mathematica. In Edward N. Zalta, Uri Nodelman (Eds.), The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University.
Maddy, P. (2011). Set Theory as a Foundation. In Giovanni Sommaruga (Ed.), Foundational Theories of Classical and Constructive Mathematics (pp. 85–96). Springer Netherlands.
Maddy, P. (2011). Defending the Axioms: On the Philosophical Foundations of Set Theory. Oxford, England: Oxford University Press.
Maddy, P. (2016). Set-Theoretic Foundations. In Andrés Eduardo Caicedo, James Cummings, Peter Koellner, Paul B. Larson (Eds.), Foundations of Mathematics. American Mathematical Society.
Maddy, P. (2019). What Do We Want a Foundation to Do?. In Stefania Centrone, Deborah Kant, Deniz Sarikaya (Eds.), Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts (pp. 293–311). Cham: Springer International Publishing.
Maddy, P., & Meadows, T. (2020). A Reconstruction of Steel’s Multiverse Project. Bulletin of Symbolic Logic, 26(2), 118–169.
Martin-Löf, P. (1973). An Intuitionistic Theory of Types: Predicative Part. In Logic Colloquium ’73, Proceedings of the Logic Colloquium. North Holland.
Martin-Löf, P. (1980). Intuitionistic Type Theory. Bibliopolis.
Martin-Löf, P. (1982). Constructive Mathematics and Computer Programming. In Laurence Jonathan Cohen (Ed.), Logic, Methodology, and Philosophy of Science VI: Proceedings of the Sixth International Congress of Logic, Methodology, and Philosophy of Science, Hannover, 1979 (pp. 153–175). Elsevier North-Holland.
Martin-Löf, P. (1984). Intuitionistic Type Theory: Notes by Giovanni Sambin of a series of lectures given in Padova, June 1980. Bibliopolis, .
Martin-Löf, P. (1996). On the Meanings of the Logical Constants and the Justifications of the Logical Laws. Nordic Journal of Philosophical Logic, 1(1), 11–60.
Mathias, A. R. D. (1992). What is MacLane Missing?. In H. Judah, W. Just, H. Woodin (Eds.), Set Theory of The Continuum. Springer New York.
Mathias, A. R. D. (2000). Strong Statements of Analysis. Bulletin of the London Mathematical Society, 32(5).
Mathias, A. R. D. (2001). The Strength of Mac Lane Set Theory. Annals of Pure and Applied Logic, 110(1-3), 107–234.
Mayberry, J. (1994). What is Required of a Foundation for Mathematics?. Philosophia Mathematica, 2(1), 16–35.
McLarty, C. (1991). Axiomatizing a Category of Categories. The Journal of Symbolic Logic, 56(4), 1243–1260.
McLarty, C. (1991). Elementary Categories, Elementary Toposes. Oxford, England: Oxford University Press.
McLarty, C. (2004). Exploring Categorical Structuralism. Philosophia Mathematica, 12(1), 37–53.
McLarty, C. (2011). Recent Debate over Categorical Foundations. In Giovanni Sommaruga (Ed.), Foundational Theories of Classical and Constructive Mathematics (pp. 145–154). Springer Netherlands.
Moore, G. (1982). Zermelo’s Axiom of Choice: Its Origins, Development, and Influence (Studies in the History of Mathematics and Physical Sciences). Springer.
Moschovakis, Y. N. (1994). Are Sets All There is?. In Notes on Set Theory (pp. 33–51). New York, NY: Springer New York.
Mostowski, A. (1965). Thirty Years of Foundational Studies Lectures on the Development of Mathematical Logic and the Study of the Foundations of Mathematics in 1930-1964. New York, NY, USA: Blackwell.
Osius, G. (1974). Categorical Set Theory: A Characterization of the Category of Sets. Journal of Pure and Applied Algebra, 4(1), 79–119.
Potter, M. D. (2004). Set Theory and its Philosophy: A Critical Introduction. Oxford, England: Oxford University Press.
Prawitz, D. (1974). On the Idea of a General Proof Theory. Synthese, 27(1/2), 63–77.
Program, T. U. F. (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study: https://homotopytypetheory.org/book.
Putnam, H. (1967). Mathematics Without Foundations. Journal of Philosophy, 64(1), 5–22.
Quine, W. V. (1956). Unification of Universes in Set Theory. Journal of Symbolic Logic, 21(3), 267–279.
Rathjen, M., Griffor, E. R., & Palmgren, E. (1998). Inaccessibility in Constructive Set Theory and Type Theory. Annals of Pure and Applied Logic, 94(1-3), 181–200. https://doi.org/10.1016/s0168-0072(97)00072-9
Riehl, E. (2017). Category Theory in Context. Aurora: Dover Modern Math Originals.
Russell, B. (1908). Mathematical Logic as Based on the Theory of Types. American Journal of Mathematics, 30(3), 222–262.
Schroeder-Heister, P. (2024). Proof-Theoretic Semantics: An Autobiographical Survey. In Thomas Piecha, Kai F. Wehmeier (Eds.), Peter Schroeder-Heister on Proof-Theoretic Semantics (pp. 1–51). Cham: Springer Nature Switzerland.
Shapiro, S. (1991). Foundations Without Foundationalism: A Case for Second-Order Logic. New York: Oxford University Press.
Shapiro, S. (2001). Thinking About Mathematics. Oxford University Press.
Shapiro, S. (2004). Foundations of Mathematics: Metaphysics, Epistemology, Structure. Philosophical Quarterly, 54(214), 16–37.
Shapiro, S. (2005). Categories, Structures, and the Frege-Hilbert Controversy: The Status of Meta-Mathematics. Philosophia Mathematica, 13(1), 61–77.
Shapiro, S. (2011). Foundations: Structures, Sets, and Categories. In Giovanni Sommaruga (Ed.), Foundational Theories of Classical and Constructive Mathematics (pp. 97–110). Netherlands: Springer.
Shulman, M. (2018). Homotopy Type Theory: A Synthetic Approach to Higher Equalities. In Elaine Landry (Ed.), Categories for the Working Philosopher. Oxford University Press.
Simpson, S. (2009). Subsystems of Second Order Arithmetic (Perspectives in Logic). (second ed.). Cambridge University Press.
Sommaruga, G. (2011). Foundational Theories of Classical and Constructive Mathematics (The Western Ontario Series in Philosophy of Science). (first ed.). Springer Dordrecht.
Steel, J. (2014). Godel’s Program. In Juliette Kennedy (Ed.), Interpreting Godel: Critical Essays. Cambridge University Press.
Streicher, T. (1991). Semantics of Type Theory: Correctness, Completeness and Independence Results (Progress in Theoretical Computer Science). (first ed.). Springer Birkhäuser Boston, MA.
Tarski, A. (1931). The Concept of Truth in Formalized Languages. In A. Tarski (Ed.), Logic, Semantics, Metamathematics (pp. 152–278). Oxford University Press.
Troelstra, A. S., & Dalen, D. V. (1988). Constructivism in Mathematics: An Introduction. Amsterdam: North Holland.
Turing, A. (1936). On Computable Numbers, with an Application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, 42(1), 230–265.
Väänänen, J. (2001). Second-Order Logic and Foundations of Mathematics. Bulletin of Symbolic Logic, 7(4), 504–520. https://doi.org/10.2307/2687796
Väänänen, J. (2012). Second Order Logic or Set Theory?. The Bulletin of Symbolic Logic, 18(1), 91–121.
Väänänen, J. (2014). Multiverse Set Theory and Absolutely Undecidable Propositions. In Juliette Kennedy (Ed.), Interpreting Gödel: Critical Essays. Cambridge University Press.
Väänänen, J. (2024). Second-order and Higher-order Logic. In Edward N. Zalta, Uri Nodelman (Eds.), The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University.
Voevodsky, V. (2006). A Very Short Note on Homotopy λ-calculus. Unpublished, 1–7. http://www.math.ias.edu/vladimir/files/2006_09_Hlambda.pdf
Voevodsky, V. (2014). The Origins and Motivations of Univalent Foundations. Princeton Institute for Advanced Study Newsletter, .
Wadler, P. (2015). Propositions as Types. Communications of the ACM, 58(12), 75–84.
Wang, H. (1958). Eighty Years of Foundational Studies. Dialectica, 12(3/4), 466–497.
Welch, P. D. (2015). Large Cardinals, Inner Models, and Determinacy: An Introductory Overview. Notre Dame Journal of Formal Logic, 56(1), 213–242.
Whitehead, A. N., & Russell, B. (1910). Principia Mathematica. Cambridge: Cambridge University Press.
Woodin, W. H. (2011). The Realm of the Infinite. In Micha\l Heller, W. Hugh Woodin (Eds.), Infinity: New Research Frontiers. Cambridge University Press.
Zermelo, E. (1908). Investigations in the Foundations of Set Theory I. In Jean Van Heijenoort (Ed.), From Frege to Gödel (pp. 199–215). Cambridge: Harvard University Press.

Author Information

Owain Griffin
Email: griffin.862@buckeyemail.osu.edu
The Ohio State University
U. S. A.

The Foundations of Mathematics

Table of Contents

1. Introduction

2. What is a Foundation?

a. Metaphysics?

i. Ontology?

b. Epistemology?

i. Mathematical

ii. Logico-Cartesian

iii. Knowledge of Sources

c. Criteria or Desiderata?

i. A Mathematico-Linguistic Phenomena?

ii. Frameworks

iii. Independence and Autonomy

iv. A Standard of Proof?

v. Foundational Desiderata

d. Do We Even Need a Foundation?

e. Can There Be More Than One Foundation?

f. Concluding Remarks

3. Set Theory

a. The Case for Set Theory

b. Questions and Debate

i. Independence and Axioms

ii. Universes and Multiverses

4. Category Theory

a. ETCS and CCAF

i. ETCS

ii. CCAF

b. Motivating Categorical Foundations

c. Questions and Debate

i. Adequacy

ii. Autonomy

iii. Assertion

iv. Comparison with Set Theory

d. Some Final Remarks

5. Type Theory

a. Interpreting the Syntax of Constructive Type Theory

i. Propositions as Types

b. Mathematics in Constructive Type Theory

i. Arithmetic

ii. Interpreting Set theory

c. Questions and Debate

i. Constructive vs Classical Logic

ii. Simplicity

iii. Separation of Mathematics and Logic

iv. Comparison with Sets

6. Univalence and Homotopy

a. What is HoTT/UF?

i. Homotopy Theory

ii. Homotopy Type Theory

iii. The Univalence Axiom

b. A Unique Foundational Perspective

c. Questions and Debate

i. Relationship with Other Computational Proposals

ii. Simplicity

iii. Autonomy

iv. Assertion

v. Constructivity

vi. Comparison with Set Theory

d. A Brief Appraisal

7. Conclusion

8. References and Further Reading

Author Information

An encyclopedia of philosophy articles written by professional philosophers.