Ackermann in 1956 proposed an axiomatic set theory.
Reinhardt proved that Ackermann's set theory equals ZF
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?
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).
