Define (ordinal): $\begin {align} ordinal(x) \iff & trs(x) \land \forall y \in x (trs(y)) \,\land \\& x \, \text {is} \in \text{-well-founded}
\end{align}$
Where $trs(x)$ means $x$ is transitive, that is: $\forall y \in x \, (y \subset x)$
Ordinals shall be denoted by Greek term symbols.
Specification: $\forall x \, \exists! s: s=\{y \in x \mid \phi\}; \text{ if } s \text{ not in formula } \phi$
Define $F_\alpha$ recusively as:
$F_\emptyset = \emptyset \\ F_{\alpha+1} = f (F_\alpha) \\ F_\lambda = \bigcup F_{\gamma<\lambda}; \text{ for} \lim \lambda $
Iteration: if $f$ is a definable function symbol, then$$ \forall \alpha \exists x: x=F_\alpha$$
Hierarchy $\forall x \exists \alpha: x \in \mathcal P_\alpha$
Where $\mathcal P$ is the powerset operator.
Infinity: $\exists \alpha: \lim \, \alpha$
[EDIT] up to here was the axioms of the original question. However, to remedy that the following axiom is added:
Height: $\text{well-ordered}(x) \to \exists \alpha: x \text{ injects to } \alpha$
I'm always under the impression that this theory is equaivalent to $
\sf ZF$, i.e. have the same deductive closure!
The proofs of Extensionality, Foundation, empty set, pairing, power, and set unions, are straighforward.
What is the proof that Replacement holds here?
Best Answer
If ZF is consistent, replacement does not hold here. In ZFC all the axioms hold in $V_{\omega_1}$.