Fake proof of the Axiom of Specification I came up with a fake proof of the axiom of specification, but can't pinpoint exactly what's wrong with the proof.
Let $P$ be some logical formula which evaluates sets to true or false, and let $X$ be some set. I claim that there exists a set $S=\{x\in X\mid P(x)\}$.
By choice, we can well-order $X$. Thus, WLOG we can assume that $X$ is an ordinal. We now conduct transfinite induction to construct a function $\phi_X:X\to X+1$.
Base case: $\phi_0:0\to X+1$ is a function.
Successor Case: Given $\phi_\alpha:\alpha\to X+1$, let $\phi_{\alpha+1}$ be as follows:$$\phi_{\alpha+1}(x)=\begin{cases}\phi_\alpha(x)&x\in\alpha\\X&x=\alpha\wedge\lnot P(\alpha)\\\alpha&x=\alpha\wedge P(\alpha)\end{cases}$$Inductive Case: Given $\phi_\alpha$ for all $\alpha<\gamma$, let $\phi_\gamma(x)$ equal $\phi_\alpha(x)$ for any $x<\alpha<\gamma$.
Thus, we have a map $X\to X+1$ whose image is $S\cup\{X\}$.
Now, we extend this map to a binary relation $R$ on Set by sending any set not in $X$ to itself. Thus, by the axiom schema of replacement, $R[X]=S\cup\{X\}$ is a set, and thus, so is $S$.
 A: There are numerous problems here, but one of the most fundamental is in your use of transfinite induction and in your definition of $\phi$.
I will assume you're attempting to work without the axiom schemes of specification and replacement, since (over classical logic) replacement implies specification. I assume you're working instead with $\Delta_0$ specification (which states that if $\phi(x)$ is a formula where all quantifiers are of the form $\exists w \in a$ or $\forall w \in a$, then the set $\{x \in X | \phi(x)\}$ exists).
The problem is that well-order induction is dramatically weaker without full specification. In fact, well-order induction can only be used on $\Delta_0$ formulas.
For let us recall the principle of well-ordering induction(or, more generally, well-founded induction), which states that given a well-ordered set $(A, <)$, $\forall Q \subseteq A (\forall x \in A [(\forall y \in A (y < x \implies y \in A)) \implies x \in A]) \implies \forall x \in A (x \in Q)$.
The issue here is that we can only use well-ordering induction to show that $\forall x \in A, x \in Q$ for some subset $Q \subseteq A$. In other words, we must actually be able to define the subset $Q$ corresponding to the relevant property in order to be able to use well-founded induction.
Let's say we have some well-ordering $(A, <)$ and we want to show $\forall x \in A, Q(x)$. With full specification, we can pass to the set $Q = \{x \in A | Q(x)\}$ and use well-ordering induction on this set. But with only $\Delta_0$ specification, we require first that $Q(x)$ be a $\Delta_0$-formula in order to construct $Q = \{x \in A | Q(x)\}$ using specification.
The issue here is that the statement $Q(\alpha) :\equiv $ "$\phi_\alpha$ exists" is not a $\Delta_0$ statement, because saying whether a function satisfies the definition of $\phi_\alpha$ invokes $P(\alpha)$, which is not necessarily a $\Delta_0$ statement. Thus, you cannot apply well-founded induction here.
