Proof of transfinite induction from well-foundedness

Proof

We argue by contradiction, using a minimal counterexample.

1. Let $R$ be a well-founded relation on a set $A$ and let $P(x)$ be a predicate on $A$.
2. Assume the hypothesis: for each $x \in A$, if $P(y)$ holds for each $y \in A$ with $y \mathrel{R} x$, then $P(x)$ holds.
3. Let $S = \set{x \in A \mid P(x) \text{ is false}}$. Suppose, for a contradiction, that $S$ is nonempty.
4. Since $R$ is well-founded and $S$ is a nonempty subset of $A$, there is $m \in S$ such that no $s \in S$ satisfies $s \mathrel{R} m$.
5. Let $y \in A$ with $y \mathrel{R} m$. By step 4, $y \notin S$. By the definition of $S$, $P(y)$ is not false. By the law of excluded middle, $P(y)$ holds.
6. By step 5, $P(y)$ holds for each $y \in A$ with $y \mathrel{R} m$. By step 2 with $x = m$, $P(m)$ holds.
7. But $m \in S$ by step 4, so $P(m)$ is false. This contradicts step 6.
8. Hence $S$ is empty. So for each $x \in A$, $P(x)$ is not false. By the law of excluded middle again, $P(x)$ holds.