Is this theory as strong as ZFC?

Question

Let $T$ be a theory with a binary relation $\in$, a constant $U$, and the following axioms: \begin{align} \text{axiom of transitivity} &\quad \forall x \forall y (x \in y \in U \rightarrow x \in U) \\ \text{axiom of supertransitivity} &\quad \forall x \forall y (x \subseteq y \in U \rightarrow x \in U) \\ \text{axiom schema of comprehension} &\quad \forall \bar{a}_{\in U}(\forall x (\phi(x, \bar{a}) \rightarrow x \in U) \rightarrow \exists y_{\in U} \forall x (x \in y \leftrightarrow \phi(x, \bar{a}))) \end{align} where $\phi$ does not contain $U$ and $\bar{a}$ denotes a sequence of parameters. Then $T$ proves \begin{align} \text{empty set} &\quad \exists y_{\in U} \forall x (x \not\in y) \\ \text{powerset} &\quad \forall a_{\in U} \exists y_{\in U} \forall x (x \in y \leftrightarrow x \subseteq a) \\ \text{union} &\quad \forall a_{\in U} \exists y_{\in U} \forall x (x \in y \leftrightarrow \exists z (x \in z \in a)) \\ \text{specification} &\quad \forall a_{\in U} \exists y_{\in U} \forall x (x \in y \leftrightarrow \phi \land x \in a) \\ \text{pairing} &\quad \forall a_{\in U} \forall b_{\in U} \exists y_{\in U} \forall x (x \in y \leftrightarrow x = a \lor x = b) \\ \text{infinity} &\quad \exists y_{\in U} (\varnothing \in y \land \forall x_{\in y} (x \cup \{x\} \in y)) \end{align} Does this theory interpret ZFC? Proving a form of collection or replacement, as Reinhardt did for Ackermann set theory, seems sufficient.

Answer 1

I've asked before if class construction of Ackermann's is really needed for its equi-interpretability with ZFC [see here] But here your question dropped Extensionality, and it also has a problem with its formulation, although I think that was intended and not a typo, that is the parameters of $\phi$ in comprehension are unrestricted in $U$, but this would render the theory inconsistent! Take the formula $x \in A \land x \notin x$, now substitute that formula in comprehension, since $A$ can be any class, substitute it by $U$, then $y$ would be the Russell set.

So you must add the restriction that all parameters of $\phi$ must be bounded in $U$. Now if that's done, then you'll get a fragment of Ackermann's set theory, which is of course consistent relative to Ackermann's. Now in this fragment it is a theorem that for every element $x$ of $U$ all of co-extensionals of $x$ are also elements of $U$ and also proves the existence of a set of all of those that is an element of $U$, and I think this would be enough to interpret Extensionality (that if class construction schema of Ackermann's set theory is not needed for the equi-interpretability of ZFC with Ackermann's). But as its stands for now, your theory is inconsistent.

Answer 2

We can build the cumulative hierarchy up to $V_{<ω^ω}$, if we have extensionality. Even without extensionality, we still can get to the same height but I do not know how to prove a linear hierarchy. I will use the term "set" synonymously with "member of $U$".

~ ~ ~

Let $C(A,S) ≡ A∈S ∧ ∀x{∈}S\ ∃y{∈}S\ ∀t\ ( t∈y ⇔ ∀z{∈}t\ ( z∈x ) )$.
[$C(A,S)$ says that $S$ includes $A$ and is closed under powerclass.]

Let $I(A,T) ≡ ∀x\ ( x∈T ⇔ ∀S\ ( C(A,S) ⇒ x∈S ) )$.
[$I(A,T)$ says that $T$ is the intersection of all $S$ satisfying $C(A,S)$.]

Then $∀A{∈}U\ ( C(A,U) )$ [by powerset] and hence $∀A{∈}U\ ∀x\ ( ∀S\ ( C(A,S) ⇒ x∈S ) ⇒ x∈U )$.

Thus $∀A{∈}U\ ∃B{∈}U\ ( I(A,B) )$ [by comprehension].

Thus $∀A{∈}U\ ∃!B{∈}U\ ( I(A,B) )$ [by extensionality].
[This will not be used later, but I included it to show what extensionality gains.]

~ ~ ~

We have reached $V_ω$ because $∃B{∈}U\ ( I(\varnothing,B) )$. In general, we can construct the set of finite powersets of any given set. We can capture this process and iterate it internally as follows.

~ ~ ~

Let $C'(A,S) ≡ A∈S ∧ ∀x{∈}S\ ∃y{∈}S\ ( I(x,y) )$.
[$C'(A,S)$ says that $S$ includes $A$ and is closed under $I$.]

Let $I'(A,T) ≡ ∀x\ ( x∈T ⇔ ∀S\ ( C'(A,S) ⇒ x∈S ) )$.
[$I'(A,T)$ says that $T$ is the intersection of all $S$ satisfying $C'(A,S)$.]

Then $∀A{∈}U\ ( C'(A,U) )$ [by above] and hence $∀A{∈}U\ ∀x\ ( ∀S\ ( C'(A,S) ⇒ x∈S ) ⇒ x∈U )$.

Thus $∀A{∈}U\ ∃B{∈}U\ ( I'(A,B) )$ [by comprehension].

~ ~ ~

We now have essentially reached $V_{ω·ω}$, because we essentially have $I(V_0,V_ω)$ and $I(V_ω,V_{ω·2})$ and in general $I(V_{ω·k},V_{ω·(k+1)})$ for any $k∈ω$. I say "essentially" since without extensionality it seems impossible to define $V_{ω·k}$ even though there is some $B$ satisfying $I'(\varnothing,B)$ and so this $B$ includes all the sets that are candidates for being $V_{ω·k}$.

We can clearly repeat this any finite number of times. The first time gave closure of levels (of the hierarchy) under ${}+1$. The second gave closure under ${}+ω$. The third gives closure under ${}+ω·ω$. The $n$-th gives closure under ${}+ω^n$.

Iterating this (externally) all the way gives $V_{<ω^ω}$. I do not see how to construct anything like $V_{ω^ω}$, even with extensionality, so this theory seems weaker than Z plus countable replacement. I would be very intrigued if someone goes beyond that. My intuition is not that good, but it feels like this theory is as strong as Z plus inductive construction (IC), where IC is the schema:

$∀A\ ∃S{⊇}A\ ( ∀x{∈}S\ ( f(x)∈S ) ∧ ∀T{⊇}A\ ( ∀x{∈}T\ ( f(x)∈T ) ⇒ S⊆T ) )$, for every definable function $f$.

Answer 3

Not a full answer to the question, but some thoughts:

For any relation $R$, say \begin{align} \text{$S$ is $R$-closed} \longleftrightarrow \forall x_{\in S} \exists y_{\in S} R(x,y) \end{align}

Define the following relations: \begin{align} F(a, b) &\longleftrightarrow \forall x (x \in b \leftrightarrow x \in a \lor x \subseteq a) \\ F^\omega(a, b) &\longleftrightarrow \text{$b$ is the minimal $F$-closed set containing $a$} \\ F^{\omega \cdot \omega}(a, b) &\longleftrightarrow \text{$b$ is the minimal $F^\omega$-closed set containing $a$} \\ F^{\omega \cdot \omega \cdot \omega}(a, b) &\longleftrightarrow \text{$b$ is the minimal $F^{\omega \cdot \omega}$-closed set containing $a$} \\ & \dots \\ F^{\omega^{n+1}}(a, b) &\longleftrightarrow \text{$b$ is the minimal $F^{\omega^n}$-closed set containing $a$} \end{align}

This can be interpreted as $b$ containing $a$ and being closed under transfinitely-long chains of $F$. Then \begin{align} &\exists x F(\varnothing, x) && (V_1) \\ &\exists x F^\omega(\varnothing, x) && (V_\omega) \\ &\exists x F^{\omega \cdot \omega}(\varnothing, x) && (V_{\omega \cdot \omega}) \\ & \dots \\ &\exists x F^{\omega^n}(\varnothing, x) && (V_{\omega^n}) \end{align}

Thus it looks like we have at least $V_{< \omega^\omega}$, as the other answer pointed out.

---

More concisely, we can do the following for the ordinals: For notational convenience, assume extensionality. For a functional relation $f$, say \begin{align} \text{$x$ is $f$-closed} \leftrightarrow \forall y (y \in x \rightarrow f(y) \in x) \end{align} Let \begin{align} s(x) &= x \cup \{x\} \\ s^{\omega^{n+1}}(x) &= \text{intersection of all $s^{\omega^n}$-closed classes containing $x$} \end{align} These can be viewed as transfinite compositions of $s$. Then \begin{align} \varnothing \neq s^{\omega^n}(\varnothing) \in U \end{align}

Answer 4

I don't agree with the answers given above! So I'll pose this answer as a partial answer to show that such approaches are invalid here.

I'll assume Extensionality throughout.

This theory proves that for any ordinal $\alpha \in U$, i.e. any set ordinal, the stage $V_\alpha$ of the cumulative hierarchy is a set!

The reason is because this theory proves transfinite induction scheme over set ordinals for properties definable after formulae eligible in comprehension.

Let take the property: $\exists x: x = P^\alpha(\emptyset)$ which is exactly $\exists x: x=V_\alpha$, now this doesn't use $U$ in it, and when $\alpha \in U$ then it qualifies for comprehension.

Now clearly for any limit set ordinal $\alpha$ if for every $\beta \in \alpha$ we have $\exists x \in U: x=V_\beta$, then by comprehension schema there exists a union of all $V_\beta$ stages! But this is $V_\alpha$, if $\alpha$ was a successor, then clearly $V_\alpha$ is the power set of $\bigcup V_{\beta < \alpha}$.

So by transfinite induction for any set ordinal $\alpha$, there exists $V_\alpha$.

Now to see that every $V_\alpha$ must be a set, is clear, since either $\alpha$ is a limit ordinal, and since it is a set, then we can use the formula $ x \in V_{\beta \in \alpha}$ and by comprehension $V_\alpha$ would be a set. If $\alpha$ was a successor, then clearly $V_\alpha$ is the power set of the union of the prior stages, and since that union is a set, then it must be a set.

Therefor this theory proves: that for every ordinal $\alpha$: $$\alpha \in U \to V_\alpha \in U$$. Now this theory clearly proves infinity, and power, so it proves existence of all countable ordinals, and of course existence of uncountable ones as well.

Since this theory proves $\omega ^ \omega \in U$, then of course it proves that $V_{\omega^\omega}$ is a set.

Now to see how $\omega^\omega$ is a set, we need to define recursive tiers of succession:

Define $S_i$ as

$S_1(\alpha) = \alpha \cup \{\alpha\}$

$S_{i+1} (\alpha) = \bigcup (\bigcap x :\alpha \in x \land x \text{ closed under } S_i)$

Now each $S_i(\omega)=\omega^{i-1}$ when $i \geq 3$.

Now this theory proves that: for every natural number $n$: $$S_n(\omega) \in U \to S_{n+1} (\omega) \in U$$, so we simply construct the set $K=\{S_3(\omega), S_4 (\omega),...\}$, this is simply the intersection of all classes I such that: $$S_3(\omega) \in I \land \forall n (S_n(\omega) \in I \to S_{n+1}(\omega) \in I)$$; then $\omega^\omega = \bigcup K$.