Let $SC$ (sets and classes) denote the modification of Ackermann set theory laid out in F. A. Muller's Sets, Classes and Categories (denoted there by ARC -- a brief summary of the theory is given below, see the reference for a more detailed discussion).
Let $ZMC/\mathbb{S}$ be $ZFC$ plus a constant symbol $\mathbb{S}$ and an axiom stating that $\mathbb{S}$ is a Grothendieck universe, together with a reflection axiom schema stating that $$\forall x_1\in\mathbb{S}\cdots\forall x_n\in\mathbb{S}\big(\phi(x_1,\dots,x_n)\iff\phi^\mathbb{S}(x_1,\dots,x_n)\big)$$ as laid out in Mike Shulman's paper Set Theory for Category Theory.
How does $SC$ compare to $ZMC/\mathbb{S}$ as a foundation for category theory? Do we run into any issues that the latter handles 'better' than the former?
Muller's paper lays out how we can handle all of standard $1$-category theory in this modified theory (summarized below), and further points out that $SC$ is not conservative over $ZFC$ but that $ZFC^+$ ($ZFC$ plus the existence of the first uncountable strictly inaccessible cardinal) is sufficient to prove its consistency, whereas MacLane's set theory requires $ZFC^{++}$ to establish consistency and Grothendieck's theory with universes requires $ZFC^{++\cdots}$.
Similarly, Shulman's paper lays out how $ZMC/\mathbb{S}$ can handle all of $1$-category theory and points out that it is equivalent to $ZFC+"Ord$ is Mahlo" (thusly also equivalent to $ZFC^{++\cdots}$) and consequently much stronger in consistency strength than $SC$.
The theory $SC$ is given as follows (for a more detailed exposition see Muller's paper above, where this theory is referred to as $ARC$). We work in a language where the primitives are classes and class membership, and we have a constant symbol $\mathbb{V}$ denoting the 'universe of sets'. A set is a class that is a member of $\mathbb{V}$.
We have axioms as follows:
- Extensionality, in the usual sense applied to classes.
- Completeness, asserting that $\mathbb{V}$ is closed under member’s members and member’s subsets.
- Class Separation, asserting that for any predicate $\phi(\cdot,Y)$ where $Y$ stands for any finite number of class parameters, and for every class $Z$, there exists a class $A$ whose members are exactly those members of $Z$ satisfying $\phi(\cdot,Y)$.
- Regularity, but only for sets.
- Choice, again for sets only.
For the final axiom, say that a predicate $\psi$ is safe iff $\psi$ only contains set-parameters and $\mathbb{V}$ does not occur in it. Then we have
- Set Existence, asserting that for any safe predicate $\phi(\cdot,Y)$ where $Y$ stands for any finite number of set parameters, if the only classes for which $\phi(\cdot,Y)$ holds are sets, then the class of these sets is a set.
Working in this theory, call a class $X$ good iff there exists some $n\in\omega$ such that $X\in\mathcal{P}^n(\mathbb{V})$, so good classes are obtained through finitely many applications of the powerset operation applied to the universe of sets. Call a class $X$ good of rank $n$ iff $X$ is good and $n$ is the smallest natural number such that $X\in\mathcal{P}^n(\mathbb{V})$. We then have the following
Theorem for Good Classes. The following classes are good:
- The powerclass and union class of a good class.
- The union, intersection, complement, (un)ordered pair, and Cartesian product of any finite number of members of one good class.
This theorem doesn't exist in Ackermann set theory, since it isn't provable without class separation. We also have the
Lévy-Vaught Theorem. All good classes exist.
From these theorems we immediately deduce that we can combine good classes of the same rank in all the same ways we can sets, and a slight modification of the definition of a tuple (laid out in a 1998 paper by Muller) yields that we can form all constructions we would like to using good classes of arbitrary rank. This is Muller's primary justification for saying that category theory can be founded in $SC$, since functor categories between large categories etc. are all (collections of) good classes (of potentially varying rank) in this theory.
Are there any constructions in standard category theory that can't be carried out in $SC$? How about higher category theory?
Any relevant input is appreciated, and I am open to broad interpretations of the word 'better' in the first highlighted question.
