16
$\begingroup$

Using Grothendieck universes as the foundations of (higher) category theory is problematic:

  • The existence of Grothendieck universes relies on the existence of inaccessible cardinals. However, one can not prove that the existence of inaccessible cardinals is independent from ZFC: see e.g. this question on SE.
  • So whenever one proves a claim which is formulated in ZFC, but where the proof uses (higher) category theory, it is absolutely valid to question whether or not the existence of inaccessible cardinals is fundamentally needed, or just a gadget to justify category theoretic arguments. This happened e.g. with Wiles' proof of Fermat's last theorem, see this post on MO.

Intuitively and naively one wants to be able to form e.g. the category of all small categories without having to worry about any of this. Essentially, I am looking for some axiomatic class theory that allows one to do higher category theory, but which is a conservative extension of ZFC (i.e. every claim that can be formulated in ZFC and that can be proven using this hypothetical theory of classes can also be proven in ZFC).

So my first question is:

  1. Is there an axiomatic set/class theory that allows one to work with higher categories (in particular, stacks) seamlessly, but which is a conservative extension of ZFC? (I believe the answer is 'no', since otherwise people would use this theory instead of Grothendieck universes - but maybe such a theory is just not well-known to the mainstream algebraists)
  2. Is question 1 completely hopeless? I.e. is there a fundamental reason why working with higher categories necessitates the assumption of the existence of inaccessible cardinals?

My completely naive proposal to question 1 is the following: based on how one forms 2-categories from 1-categories, one could consider a typed axiom system as follows:

  • For every ZFC-ordinal $\mu$, we have $\mu$-sets. ZFC sets are '0-sets'.
  • The collection of all $\mu$-sets forms a $\mu+1$-set. Moreover, the collection $$\{S \; : \; S \text{ is a }\nu \text{-set for some } \nu < \mu\}$$ forms a $\mu$-set.
  • $\mu$-sets satisfy ZFC-type axioms, with the restriction that one can only take a $\mu$-set sized union of $\mu$-sets to obtain a $\mu$-set, and only a $0$-set (ZFC-set) sized formula in the axiom schema of specification.

My questions about this construction:

  1. People must have worked with such axioms before. Could you provide some references?
  2. Inspired by the proof of the fact that the Von Neumann-Bernays-Gödel (NBG) set/class theory is a conservative extension of ZFC: could such a theory be a conservative extension of ZFC?
Improve this question
$\endgroup$
21
  • 6
    $\begingroup$ A provocative answer is that we should drop set theory all together as foundations. We could decide to work with other foundations than set theory. A very good and robust alternative is dependent type theory. Having a hierarchy of universes in dependent type theory has the same strength than having Peano arithmetic. Type theory is as old as set theory (Russell in the 1910's) and has many ramifications used in computer science (lambda-calculus, calculus of constructors) for more than a century. And we can construct models of set theory within dependent type theory. $\endgroup$ Commented Dec 10, 2025 at 15:31
  • 13
    $\begingroup$ @D.-C.Cisinski "Having a hierarchy of universes in dependent type theory has the same strength than having Peano arithmetic." This is not true. $\endgroup$ Commented Dec 10, 2025 at 19:19
  • 8
    $\begingroup$ @D.-C.Cisinski " And we can construct models of set theory within dependent type theory." And we can construct models of dependent type theory within set theory, so why are you bringing this up? $\endgroup$ Commented Dec 10, 2025 at 20:23
  • 8
    $\begingroup$ Speaking as a PhD student in type theory, I will also say tangentially that I do not believe at all that type theory is “strictly better” in an absolute sense than set theory. I think the most productive mindset is to (1) embrace the fact that there are many possible foundations and we don't need to choose a “canonical” one, and (2) take the things achievable with one foundation and not another, which are plenty on both sides (e.g., inner models vs. reasoning internally in Grothendieck $(∞, 1)$-toposes) as an intriguing phenomenon inviting further investigation. $\endgroup$ Commented Dec 10, 2025 at 21:44
  • 7
    $\begingroup$ @D.-C.Cisinski Sure, MLTT + universes without LEM, choice, or W-types is predicative. It's still well above Peano and way too little to build set theoretic models. $\endgroup$ Commented Dec 11, 2025 at 0:04

1 Answer 1

Reset to default
25
$\begingroup$

The answer to question 1 is actually positive, accomplished by Feferman set theory. I have learned of (a variant of) it from Cantor's Attic.

We define the theory FST by taking ZFC, adjoining a new predicate symbol $C$ to its language, and adding the following axioms concerning it:

  • $C$ defines a closed and unbounded class of cardinals,
  • For any formula $\varphi$ in the language of ZFC (i.e. not involving $C$) with one parameter, we have an axiom $$\forall\kappa\in C\forall x\in V_\kappa\big(\phi(x)\iff (V_\kappa\models\phi(x))\big).$$

That is, any element $\kappa\in C$ is a correct cardinal, so that $V_\kappa$ is an elementary substructure of $V$.

The reason this extension is conservative is the reflection theorem, which asserts that for any finite collection $\varphi=(\varphi_1,\dots,\varphi_n)$ of predicates, there is a closed unbounded class of cardinals $C_\varphi$ satisfying the axioms above for all $\varphi_i$. Since any proof in FST can only invoke finitely many instances of this axiom schema, we can repeat this proof in ZFC using the class $C_\varphi$ in place of $C$.

It is not hard to see that cardinals in $C$ are strong limit cardinals. However, they may fail to be regular - the axiom schema merely guarantees that any $\kappa\in C$ is regular "from within $V_\kappa$", that is, any subset of $\kappa$ which is definable in $V_\kappa$ (as a class) must have length $\kappa$. This shortcoming is I imagine why this theory has not gained much traction, since although you are unlikely to run into such undefinable classes inside $V_\kappa$, in principle it requires some bookkeeping to make sure things do not go wrong. See this MO post for a similar discussion.

On the other hand, correctness of these cardinals has its advantages - we can work with all of $V$ or internally to some $V_\kappa,\kappa\in C$, and the results we prove will be equally valid by the above axiom schema.

Improve this answer
$\endgroup$
1
  • 4
    $\begingroup$ Particularly relevant is Peter Scholze's answer to the MO post you cite. $\endgroup$ Commented Dec 11, 2025 at 18:42

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.