What is the proof of Replacement in iterating functions over the empty set?

Question

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?

Answer 1

If ZF is consistent, replacement does not hold here. In ZFC all the axioms hold in $V_{\omega_1}$.

Answer 2

After Kirmayer's answer, I've figured out the answer to my revised question (which copies the original intention behind this posting).

We seek to prove well ordered replacement, that is for any well ordered set $x$ and a definable function $f$ there exists a set $\{f(y) \mid y \in x\}$.

Proof: from axiom of Height we take an initial ordinal that is bijective to $x$, that is $|x|$, now we take a bijection $g$ from the set $\text{Successors}|x|=\{\alpha+1 \mid \alpha \in |x| \}$ to $x$. Now let $G$ send every element $\alpha$ of the domain of $g$ to the rank of $f(g(\alpha))$.

Define another function $H$ from $\text{Limits}|x|=\{\lambda \in |x| : \not \exists \alpha (\lambda=\alpha+1) \}$, as:

$$H(\lambda) = \bigcup_{\alpha< \lambda} G(\alpha)$$

We define a successor function $G^+$ as the function from the $range(G) \cup range(H)$ to range($G$), defined as: $$ G^+(G(\alpha))=G(\alpha+1) \\ G^+(H(\lambda))= G(\lambda+1) $$. Define $$F_\emptyset= \emptyset \\ F_{\alpha+1}= G^+(F_\alpha) \\ F_\lambda = H(\lambda)$$ Accordingly we have $F_{|x|}$ as a set and it will contain among its elements all images of elements of $x$ under $f$, and the axiom would follow from specification.

Answer 3

None. This theory is much weaker than ZFC.

If $\alpha = \beth(\alpha), V_\alpha$ satisfies this theory.