Axiomatic strength of the cumulative hierarchy

Question

In the 2021 paper Level Theory Part I: Axiomatizing the Bare Idea of a Cumulative Hierarchy of Sets by Tim Button, a first order theory of the cumulative hierarchy is explored. Initially no axioms regarding the height of this hierarchy are added, resulting in a relatively weak theory referred to as ${\bf LT}$ for level theory. He then considers three more putative axioms regarding the height of this hierarchy, referred to as ${\bf Endless,\ Infinity}$ and ${\bf Unbounded}$. Towards the end of his paper we have

Proposition 7.1.

1. ${\bf LT}$ proves separation, union and foundation.
2. ${\bf LT + Endless}$ proves pairing and powersets.
3. ${\bf LT+Endless+Infinity}$ proves Zermelo's axiom of infinity.
4. ${\bf LT+Endless+\neg Infinity}$ is equivalent to ${\bf ZF_{fin}}$.
5. ${\bf LT+Infinity+Unbounded}$ proves ${\bf Endless}$.
6. ${\bf LT+Infinity+Unbounded}$ is equivalent to $ZF$.

These results are fascinating, but make me wonder if there is some elegant axiomatization of $ZF$ where remove the axioms of separation, union, and foundation (and perhaps pairing/powersets/more) and add some 'cumulative hierarchy' axiom and get the other axioms for free.

Is anyone here aware of such an axiomatization, or able to cook one up on the spot?

Another question that comes to mind, but which is slightly more ambiguous:

What is the axiomatic strength of the cumulative hierarchy over the rest of the set theory axioms, minus the ones we use to construct it?

Any pointers are appreciated.

Answer 1

This is an edited and improved answer; see edit details at the end.

We can obtain the whole of ZF using a single, natural, scheme.

I will keep the definition of level from Button 2021, as cited above. (The definition needs a slight tweak, because Button 2021 assumes extensionality, but that assumption is easily removed.) Intuitively, our scheme is as follows, for any definable partial function $\tau$. For any $a$, there is a level $s \ni a$ such that: for any $b \in s$, exactly one set in $s$ comprises the $\tau$-images of $b$'s members.

Here is the scheme precisely, with $Lev$ as in Button 2021:

The Main Scheme. Where $\tau$ is any definable partial function, this is an axiom: $$\forall a (\exists s \ni a)\big(Lev(s) \wedge (\forall b \in s)(\exists ! c \in s)\forall z(z \in c \leftrightarrow (\exists x \in b)\tau(x) = z)\big)$$

To avoid mis-understandings, here is how we might re-state the Main Scheme, in terms of arbitrary formulas. If $\forall x \forall y \forall z\big((\phi(x,y) \wedge \phi(x,z)) \rightarrow y = z\big)$, then $\forall a (\exists s \ni a)\big(Lev(s) \wedge (\forall b \in s)(\exists ! c\in s)\forall z(z \in c \leftrightarrow (\exists x \in b)\phi(x,z))\big)$.

---

Theorem. The theory whose only axioms are all the instances of the Main Scheme is a re-axiomatization of ZF.

To prove the Theorem, I will prove a few lemmas.

Lemma 1. The Main Scheme entails Separation. Proof. Fix $a$ and any formula $\psi(x)$. Let $\tau(x)$ be $x$ when $x \in a \wedge \psi(x)$, and be undefined otherwise. By the Main Scheme, there is a level $s$ with $a \in s$ and some (unique) $c \in s$ such that $\forall x\big(x \in c \leftrightarrow (x \in a \wedge \psi(x))\big)$. So $c$ is the result of Separation on an arbitrary set $a$.

Lemma 2. The Main Scheme gives Extensionality. Proof. Reason exactly as before, but letting $\psi(x)$ be trivial. So there is a level $s$ with $a \in s$ and a unique $c \in s$ which is co-extensive with $a$, i.e. $\forall x(x \in c \leftrightarrow x \in a)$. Moreover, if $d$ is co-extensive with $a$, then also $d \in s$, since $s$ is a level and hence is closed under subsets of members (see Button 2021 section 3). So all sets co-extensive with $a$ are in $s$, and hence are identical.

Note: having obtained Extensionality, we can re-write the Main Scheme like this, where $\tau$ is any definable partial function, and where we write $\tau[b]$ for $\{\tau(x) : x \in b\}$: $$\forall a (\exists s \ni a)\big(Lev(s) \wedge (\forall b \in s)\tau[b] \in s\big)$$ It's worth noting how this resembles Replacement.

Lemma 3. The Main Scheme gives Stratification and Endless. Proof. Let $\tau(x)$ just be $x$. By the Main Scheme, for any $c$ there is a level $s$ with $c \in s$. Now $c \subseteq s$ (as levels are transitive; see Button 2021 section 3) establishing Stratification. And also every level $c$ has a successor, establishing Endless.

Lemma 4. The Main Scheme gives Infinity. Proof. Let $\tau(x)$ be $\{x\}$. Using everything we have established so far, $\text{rank}(\tau(x)) = \text{rank}(x) + 1$ for every $x$. By Endless and the Main Scheme, there is some level $s$ with $\{\emptyset\} \in s$ such that: for any $b \in s$, also $\tau[b] \in s$. Since $\text{rank}(\tau[b]) = \text{lsub}_{x \in b}\text{rank}(x)$, it follows that $s$ is a limit level.

Lemma 5. The Main Scheme gives Unbounded. Proof. Let $\tau$ be any total definable function, i.e. $\tau(x)$ exists for any $x$. Fix $a$; by the Main Scheme, there is a level $s$ with $\tau[a] \in s$; now just note that levels are transitive, so $\tau(x) \in s$ whenever $x \in a$.

Combining Lemmas 1-5: the Main Scheme yields LT + Infinity + Unbounded, which is equivalent to ZF (as in Button 2021; the key to that equivalence is to prove, in ZF, that the $V_\alpha$'s are the levels). This final result completes the proof of our Theorem:

Lemma 6. ZF proves the Main Scheme. Proof. Fix $\tau$. Replacement tells us that $\tau(x)$ exists for any $x$. Using recursion, we can show that, for any $a$, there is a level $s$ with $a \in s$ and closed under $\tau[\cdot]$, i.e. if $b \in s$ then $\tau[b] \in s$.

---

Explanation of edits. In my original answer, I offered a simpler scheme: $$\forall b \exists c \phi(b, c) \rightarrow \forall a (\exists s \ni a)(Lev(s) \wedge (\forall b \in s)(\exists c \in s)\phi(b, c))$$ This a slight variation of a scheme suggested by Dana Scott (1960, "The notion of rank in set-theory"). The variation is suitable, given my definition of level.

Using arguments like those above (but simpler!), I showed that Extensionality + Separation + the Scott-like Scheme is just ZF under a different axiomatization.

Then @ZuhairAl-Johar suggested the improvement (in discussion below), tweaking the above to what I've now called the Main Scheme.

Answer 2

Now, I think the bare idea of a Hierarchy is this:

if $F$ is a total unary function, then we can build a function $V$, such that:

$V^F_\emptyset = \emptyset \\ V^F_{\alpha+1} = F(V^F_\alpha) \\ V^F_\lambda = \bigcup V^F_{\alpha < \lambda}$

In the usual setting we take $F$ to be the powerset operator $\mathcal P$, but this is not the bare glimpse of a hierarchy. It is an instance of it.

However, since we want to capture $\sf ZFC$, then we can modify this to:

$V^F_\emptyset = \emptyset \\ V^F_{\alpha+1} = \mathcal P (F(V^F_\alpha)) \\ V^F_\lambda = \bigcup V^F_{\alpha < \lambda}; \text { for limit }\lambda$

When $F$ is the identity function, we'll simply omit $F$ from the notation.

Now, I think $\sf ZFC$ can be captured by defining all of the above and also defining the cardinality function, all in first order logic with equality and membership, then have axioms of

Extensionality: $x \subset y \land y \subset x \to x=y$

Levels: $\forall x \exists \alpha: |V^F_\alpha|=\alpha \land x \in V^F_\alpha$

Level-Separation: $\forall \alpha \forall \vec{k} \in V_\alpha \exists x: x=\{y \in V_\alpha \mid \phi^{V_\alpha}\}$

Where $\phi^X$ means all quantifiers in $\phi$ are bounded by $X$.

Lots of technical definitional details I didn't give here but they can be easily done. The point is that one can easily cook some hierarchy motivated principles from the outset, and get the resulting theory equivalent to $\sf ZFC$, but they would appear complex and in some sense contrived.