[Ackermann](https://en.wikipedia.org/wiki/Ackermann_set_theory) in 1956 proposed an axiomatic set theory.


Reinhardt proved that [Ackermann's set theory equals ZF](https://www.sciencedirect.com/science/article/pii/0003484370900112)


It's clear that Zermelo set theory can be interpreted in Ackermann's set theory minus class comprehension.



> 
> Is Ackermann's set theory minus class comprehension also equal to ZF?
> 
> 
> 


In other words: did Reinhardt's proof made an essential use of the class comprehension schema in proving the equivalence between Ackermann's set theory and ZF?



Is Ackermann's set theory minus class comprehension equal to ZF?
Let $V$ be the $V$ from $A$. It is clear $V$ satisfies exstensionality, seperation, and regularity. Pairing follows from reflection ($x=a\lor x=b$). Inductively, we can prove each $n\in V$, and so we have $\omega\in V$. If $X\in V$, then $\cup X\subseteq V$. Then define $\phi(x)\leftrightarrow \exists y(y\in X\land x\in y)$. By reflection $\cup X=\{x|\phi(x)\}$, and so $\cup X\in V$. A similar argument goes for powerset. For replacement, let $F=\{(x,y)|\phi(x,y)\}$ be a function. Then $F(X)\subseteq V$ (By definition). Then we can find some $V\_\alpha$ that reflects $\phi(x,y)$ relative to $V$, and $x\in F(X)\leftrightarrow \exists y(y\in X\land\phi(x,y)^{V\_\alpha})$, and so $F(X)\in V$. Therefore $V\vDash \phi$ for each axiom $\phi$ of $ZFC$. Now suppose an axiom of $ZFC\,\phi$, satisfies $\phi\vdash\psi$. Then every model of $\phi$ satisfies $\psi$, and so $V\vDash\psi$.


**Proof the $V$ satisfies the reflection theorem:** Note that the statement $x\in V\_\alpha$ is $\Delta\_1$, and so $V\_\alpha^V=V\_\alpha$. In addition, the mapping $\phi(x,\alpha)\leftrightarrow rank(x)<\alpha$ is $\Delta\_1$, and so $\phi(x,\alpha)^V\leftrightarrow\phi(x,\alpha)$. Then for any $\alpha\in V$, $V\_\alpha=\{x|rank(x)<\alpha\}$, and so $V\vDash Replacement\,for\,\alpha\mapsto V\_\alpha$. As a consequence, for any $C\subseteq V$, the set $\hat C=\{x\in C|\forall y\in C(rank(x)\leq rank(y))\}$ is in $V$.


Let $H(u\_0...u\_n)=\hat C$ and $C=\{x|\phi^V(x\_0...x\_n)\}$. Then, for any set $M\_0\in V$, define a sequence starting at $M\_0$ with $M\_{i+1}=M\_i\cup(\cup\{H(u\_0...u\_n)|u\_0...u\_n\in M\_i\})$. The function $F^V:{i\mapsto V\_{ran(M\_i)+1}}$ can be defined inductively, and it is easy to see that if $F(i)\in V$, $F(i+1)\in V$. Then $D=\cup \{H(u\_0...u\_n)|u\_0...u\_n\in\cup F(\omega)\}$ is in $V$. Then $x\in F(i)\leftrightarrow (i=0\land x\in M\_0)\lor (\exists j(j+1=i\land x\in F(i)\cup ((D'\restriction F(i))(F(i))))$, where $D'$ is the union of the class of all sets such that each $x\in D'$ is $\hat C$ for some $C$ and $\cup D'=D$. What I mean by $(D'\restriction F(i))(F(i))$, is really $(G\restriction F(i))(F(i))$, where $G=\{(x,u\_0...u\_n)|x=H(u\_0...u\_n)\land u\_0...u\_n\in F(i)\}$. And so $V\_\alpha=\cup F(\omega)$ is in $V$ and $V\_\alpha\vDash\phi\leftrightarrow V\vDash\phi$ (By induction on formula complexity).


