You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Peva Blanchard (Sep 29 2025 at 11:56):I read the thread set theoretic and categorical foundations, hoping to understand a bit more various aspects of foundations of mathematics. But now, I am more confused than before.
Is there a good reference that gives a historical account of the problem of foundations of mathematics?
I am interested in knowing how this problem has been formulated, why set theory has this prominent role, and what the alternatives are (including reformulations of the problem). So, more about the genealogy of ideas than the actual mathematical content.
John Baez (Sep 29 2025 at 13:59):Just as a start, are you familiar with all the material here, including the timeline of discoveries?
John Baez (Sep 29 2025 at 14:04):There's a slightly more advanced overview here:
All this is standard stuff that people interested in foundations of mathematics would expect others to know when discussing this subject.
Peva Blanchard (Sep 29 2025 at 15:19):Thank you John. I am remotely familiar with the content of the wikipedia page (but clearly not enough).
My understanding, very briefly, is:
I am not sure I understand what the "problem of founding mathematics" is about. At first, I thought it was the point 2: find a framework (e.g. ZFC), reduce all mathematics to it, and prove it is consistent and complete. But Gödel's theorems just show this is a dead end.
A more relaxed formulation would be: find a framework (e.g. ZFC) and reduce all mathematics to it. But then ... why would we want to do that? And why ZFC specifically?
Ryan Wisnesky (Sep 29 2025 at 15:33):another reason to reduce all math to a foundational formal system is to help mechanize proof checking using a computer. proof assistants such as mizar use set theory, although type theory is popular too.
Peva Blanchard (Sep 29 2025 at 15:55):Oh interesting, thank you. So a goal more modest than "proving consistency and completeness" is "checking proofs are valid", which in practice is already a big deal.
Morgan Rogers (he/him) (Sep 29 2025 at 16:00):I think there's a more at stake too from a philosophical perspective:
Alex Kreitzberg (Sep 29 2025 at 16:05):I believe a very important touch stone was Cantor discovering that "completed infinites" seemed necessary to do mathematics.
You could pretend actually completing a limit wasn't really possible, those are "potential infinites".
But Cantor established the continuum was "bigger than" the natural numbers. so now you can't easily pretend infinite math doesn't exist anymore.
If you do like this, or don't like this, how do you decide either way since we can only prove with a finite amount of stuff?
A second aspect is geometry, as Euclid did it, was a sort of science of space. As understanding of space and mathematics improved, if Euclid's work was understood as a science, it was essentially falsified. However there seemed to be good reason to believe all of Euclid's work was still "true". In what sense is this possible? Defining this would establish the sense in which mathematics wasn't physics.
Attempting to answer these, and other, questions leads to its own hornets nest of issues.
I understand Sets to be important because, in addition to packaging in infinity, if you decide their axiom system is okay, along with a first order logic (which I believe can prove its own consistency without set theory) - it's surprisingly easy to build all the major structural math constructions. Building specialized applications with geometry is comparatively more difficult for example, we don't make databases with straight edges and compasses. The philosophical advantage of this, is we're at least as confident in everything else as we are in sets.
One way to think about that previous thread was asking whether Set Theory is alone in this. A modern popular competitor "Type Theory" is still basically a sort of Set Theory (actually, it's a set theory which doesn't even need a logic slapped on). Are logicians collectively running off of the founders ideas, but there are other choices? Or if your goal is to prove all of math relative to one axiom system (so we're making a general purpose language, not a domain specific language), are Sets the only game in town?
(As always I'm open to comments on my understanding of this stuff)
Damiano Mazza (Sep 29 2025 at 16:14):Peva Blanchard said:
A more relaxed formulation would be: find a framework (e.g. ZFC) and reduce all mathematics to it. But then ... why would we want to do that?
In order to increase our confidence that what we do is not contradictory. As you said, people started being scared that we would end up deriving a contradiction using what seemed to be perfectly valid logical steps from perfectly valid axioms. If you reduce all mathematics to some formal system S that you trust, then you feel safe.
In this respect, Gödel's second incompleteness theorem only "killed" Hilbert's original goal, which was to reduce all of mathematics to an especially trust-worthy S, whose consistency would be self-evident (according to him). Like I said in the other thread, today we happily trust systems that Hilbert would have never trusted, maybe because we've been using them for almost a century and got used to them. Also, the fact that we can implement these systems on a computer probably makes us feel even safer, because it helps reduce human error.
Damiano Mazza (Sep 29 2025 at 16:23):It is important to stress, however (as I already did in the other thread), that even if Hilbert's program had worked, we still would not be completely safe from an unexpected contradiction. This is because a proof of consistency of a system T using a system S is only as good as the trust you have in S: if S is inconsistent, then it can prove anything, including the consistency of T. In particular, if a system proves its own consistency, it is basically proving nothing at all. So, in the end, even in Hilbert's "dream world" we would have had to accept the consistency of his "finitistic" system (and, therefore, the consistency of mathematics) by faith.
Mike Shulman (Sep 29 2025 at 16:31):That's a point that I think isn't stressed enough: since an inconsistent theory proves anything, it also proves its own consistency, so even a priori a proof of consistency of a system in itself can't tell us that the system is consistent. Godel's theorem only strengthens that to say that a proof of consistency of a system in itself actually tells us the system is inconsistent.
Mike Shulman (Sep 29 2025 at 16:32):Ryan Wisnesky said:
proof assistants such as mizar use set theory
Are you sure the plural is justified there? Mizar is the only proof assistant I know of that uses set theory (and even it also has a type-theoretic layer on top, because bare set theory is so inappropriate for a proof assistant).
Mike Shulman (Sep 29 2025 at 16:34):Consistency-wise, I think this is the main point:
Alex Kreitzberg said:
we're at least as confident in everything else as we are in sets.
If the foundational theory is more "self-evidently" consistent, or we can at least develop an intuition for it that convinces us of its consistency, then anything we build on top of it is at least as consistent, without our having to go through a parallel process of convincing ourselves that we believe in its consistency.
Mike Shulman (Sep 29 2025 at 16:35):But another very important benefit of a foundational theory is interoperability. If algebra and geometry are both defined in terms of sets, then a geometer can easily make use of algebra and vice versa.
John Baez (Sep 29 2025 at 17:21):Peva Blanchard said:
A more relaxed formulation would be: find a framework (e.g. ZFC) and reduce all mathematics to it. But then ... why would we want to do that? And why ZFC specifically?
The first question has been adequately answered, but in brief: by putting everything under one umbrella, we both increase the unity of mathematics (always a good thing) and reduce the chance of inconsistencies as compared with a patchwork approach where people keep making up new formalisms as they go.
As for the second, it's important to study history, because ZFC was certainly not "inevitable"; it arose for some historically contingent reasons.
Alex pointed to a key step in the history:
Alex Kreitzberg said:
I believe a very important touch stone was Cantor discovering that "completed infinites" seemed necessary to do mathematics.
You could pretend actually completing a limit wasn't really possible, those are "potential infinites".
But Cantor established the continuum was "bigger than" the natural numbers. so now you can't easily pretend infinite math doesn't exist anymore.
Cantor delved into the theory of infinite sets, showing some were bigger than others, and discovering many marvelous things about them, some very useful. But his work also led to contradictions like the Burali-Forti paradox:
In set theory, a field of mathematics, the Burali-Forti paradox demonstrates that constructing "the set of all ordinal numbers" leads to a contradiction and therefore shows an antinomy in a system that allows its construction. It is named after Cesare Burali-Forti, who, in 1897, published a paper proving a theorem which, unknown to him, contradicted a previously proved result by Georg Cantor. Bertrand Russell subsequently noticed the contradiction, and when he published it in his 1903 book Principles of Mathematics, he stated that it had been suggested to him by Burali-Forti's paper, with the result that it came to be known by Burali-Forti's name.
Frege's approach to set theory was also inconsistent: the problem was noticed by Russell and is thus called Russell's paradox:
Russell discovered the paradox in May or June 1901. By his own account in his 1919 Introduction to Mathematical Philosophy, he "attempted to discover some flaw in Cantor's proof that there is no greatest cardinal". In a 1902 letter, he announced the discovery to Gottlob Frege of the paradox in Frege's 1879 Begriffsschrift and framed the problem in terms of both logic and set theory, and in particular in terms of Frege's definition of function.
Russell wrote to Frege about the paradox just as Frege was preparing the second volume of his Grundgesetze der Arithmetik. Frege responded to Russell very quickly; his letter dated 22 June 1902 appeared, with van Heijenoort's commentary in Heijenoort 1967:126–127. Frege then wrote an appendix admitting to the paradox, and proposed a solution that Russell would endorse in his Principles of Mathematics, but was later considered by some to be unsatisfactory....
John Baez (Sep 29 2025 at 17:32):Russell wrote an enormous 3-volume book with Whitehead trying to lay out a system that dodged these paradoxes: the Principia Mathematica, with the 3 volumes coming out in 1910, 1912 and 1913.
PM, according to its introduction, had three aims: (1) to analyse to the greatest possible extent the ideas and methods of mathematical logic and to minimise the number of primitive notions, axioms, and inference rules; (2) to precisely express mathematical propositions in symbolic logic using the most convenient notation that precise expression allows; (3) to solve the paradoxes that plagued logic and set theory at the turn of the 20th century, like Russell's paradox.[3]
This third aim motivated the adoption of the theory of types in PM. The theory of types adopts grammatical restrictions on formulas that rule out the unrestricted comprehension of classes, properties, and functions. The effect of this is that formulas such as would allow the comprehension of objects like the Russell set turn out to be ill-formed: they violate the grammatical restrictions of the system of PM.
But the type theory introduced in Principia Mathematica (somewhat different from what people now call type theory) was very burdensome.
Further developments and problems led to ZFC... rather slowly, and not without difficulties:
In 1908, Ernst Zermelo proposed the first axiomatic set theory, Zermelo set theory. However, as first pointed out by Abraham Fraenkel in a 1921 letter to Zermelo, this theory was incapable of proving the existence of certain sets and cardinal numbers whose existence was taken for granted by most set theorists of the time, notably the cardinal number aleph-omega and the set {Z, P(Z), P(P(Z)), P(P(P(Z))) , . . . }, where Z is any infinite set and P is the power set operation.
Moreover, one of Zermelo's axioms invoked a concept, that of a "definite" property, whose operational meaning was not clear. In 1922, Fraenkel and Thoralf Skolem independently proposed operationalizing a "definite" property as one that could be formulated as a well-formed formula in a first-order logic whose atomic formulas were limited to set membership and identity. They also independently proposed replacing the axiom schema of specification with the axiom schema of replacement. Appending this schema, as well as the axiom of regularity (first proposed by John von Neumann), to Zermelo set theory yields the theory ZFC.
John Baez (Sep 29 2025 at 17:37):(This passage doesn't make it clear where the axiom of choice, the "C" in ZFC, came in.)
Ryan Wisnesky (Sep 29 2025 at 20:24):mike: I'm only familiar with Mizar and metamath as set-theory based proof assistants (and even metamath is agnostic; it's the largest library for metamath that uses set theory)
Kenji Maillard (Sep 29 2025 at 20:45):Concerning Set-theory based proof assistants, there are also Isabelle/ZF and PVS. I seem to remember that there was also another one being developed recently at ETH Zurich but I don't remember the name of the project or their authors.
Mike Shulman (Sep 29 2025 at 21:28):Ok, I suppose I should include metamath and Isabelle/ZF although the set theory isn't built into the ground system. I don't know anything about PVS but a brief persual of it looks type-theoretic rather than set-theoretic?
David Michael Roberts (Sep 30 2025 at 03:27):Also, ZFC wasn't dominant, in my understanding, until around the time of Cohen's proof that not AC and not CH are relatively consistent with ZF and ZFC resp. before then you had the class-set theories NBG (used by Gödel for the relative consistency of CGH and AC with ZF) and MK as contenders.
David Michael Roberts (Sep 30 2025 at 03:30):@Mike Shulman yes, I was going to say Metamath, though really just the subset of that based on zfc https://us.metamath.org/mpeuni/mmset.html#zfcaxioms
Peva Blanchard (Sep 30 2025 at 07:07):Thank you all for your answers.
So let me try to summarize. The problem of founding mathematics consists in reducing mathematics to a specific framework. We can broadly separate the motivations in:
logical. We want to avoid inconsistencies crawling up everywhere. We cannot hope to absolutely prevent any inconsistency, but we can at least reduce the perceived risk. Strategies to reduce this risk include, on the pragmatic side, proof-checking but also designing the founding framework to be as self-evident as possible, or convincing oneself that this framework is self-evident. I guess this self-evidency also relates to the philosophical aspect.
philosophical. The specific framework chosen to found math upon comes with an ontological commitment (what mathematical entities are) and epistemological organization (e.g. what and how we can know, or unifying mathematical knowledge).
The fact that Set theory specifically, in the form of ZFC (which, I learn now, was not as dominant as I thought), has played, and is still playing (I guess), the role of this founding framework is a combination of mathematical reasons, but also contingent historical conditions.
David Michael Roberts (Sep 30 2025 at 07:22):I think Penelope Maddy's work describing the differing purposes of foundations should be mentioned. https://sites.socsci.uci.edu/~pjmaddy/bio/STF%20printed%20version.pdf
It should be noted that her arguments against structural foundations may not be the best, nor aimed at even then-current ideas (eg CCAF, which is really not taken as a foundation by anyone). She even takes shots at the material multiverse view, which feels like a kind of set-theorist (mild) civil war
Peva Blanchard (Sep 30 2025 at 11:59):David Michael Roberts said:
I think Penelope Maddy's work describing the differing purposes of foundations should be mentioned. https://sites.socsci.uci.edu/~pjmaddy/bio/STF%20printed%20version.pdf
Thank you! I just started reading, but she pins exactly the question that troubles me (and which has been partially answered above)
The question for us is: what's the point of this exercise? What 'goal', properly thought as 'foundational', is served by this 'embedding'?
Mike Shulman (Sep 30 2025 at 16:01):You omitted the "practical" motivation of interoperability.
Peva Blanchard (Oct 04 2025 at 08:34):I spent a bit of time reading Maddy's paper, and she provides nice names for the various aspects we usually expect from a "foundational framework".
Peva Blanchard (Oct 04 2025 at 08:35):Mike Shulman said:
You omitted the "practical" motivation of interoperability.
I guess "interoperability" falls under Generous arena, and possibly Shared standard.
Peva Blanchard (Oct 04 2025 at 08:35):She also mentions three more problematic aspects
John Baez (Oct 04 2025 at 13:22):All this is very nice. I think that the "risk assessment" feature of ZFC has worked so well that few people worry in practice about inconsistencies showing up in ZFC. But as you add axioms imposing the existences of larger and larger cardinals, you eventually hit the Reinhardt cardinals which have been proved inconsistent with ZFC (though not (yet) with ZF). So there's a range going from "very likely to be fine" to "not good at all". But very very few mathematicians make use of the upper end of this range: it's really only a few professional set theorists, who enjoy exploring the boundaries.
John Baez (Oct 04 2025 at 13:25):There's also a lot of interesting axioms for mathematics that are weaker than ZFC, and thus more likely to be consistent. Their strength is often measured by countable ordinals in the field of ordinal analysis.
Mike Shulman (Oct 04 2025 at 15:41):Arguably, very very few mathematicians even make use of the full strength of ZFC.
Mike Shulman (Oct 04 2025 at 15:46):Peva Blanchard said:
- Elucidation: It is the ability to replace an imprecise notion with a precise one, e.g. "the real line" and Dedekind cuts.
I think it's worth mentioning that while a foundational framework can be used for this purpose, it's not the only way to replace an imprecise notion with a precise one. Domain-specific axiomatic theories can do just as well. For instance, we can make informal notions of plane geometry precise by encoding points as ordered pairs of real numbers, but we can make them equally precise by working with a formal axiomatic system for geometry such as Hilbert's refinement of Euclid's axioms. These two approaches, sometimes called "analytic" and "synthetic", each have strengths and complement each other, but neither is more precise than the other in principle.
Peva Blanchard (Oct 04 2025 at 22:02):Mike Shulman said:
I think it's worth mentioning that while a foundational framework can be used for this purpose, it's not the only way to replace an imprecise notion with a precise one. Domain-specific axiomatic theories can do just as well.
In her paper, the presentation of the various aspects is intertwined with references to Set theory. This makes, e.g., "Elucidation" look like an aspect of Set theory specifically. But I guess we can understand each aspect as an expected trait of any kind of "foundational work".
I guess we could say that building a domain-specific axiomatic theory is also "partly a foundational work". Because, for instance, it sometimes helps replacing imprecise notions with precise ones, i.e. this work shares the Elucidation trait.
However, building a domain-specific axiomatic theory does not share the other traits (e.g. meta-mathematical corral, and generous arena). So this work is less "foundational" than Set theory.
Peva Blanchard (Oct 04 2025 at 22:03):A good test of Maddy's perspective would be to check which aspects Type Theory share. (But I would need to learn more about type theory)
Mike Shulman (Oct 04 2025 at 22:20):All of them.