Transfinite Recursion/Theorem 2

From ProofWiki
Jump to navigation Jump to search


Let $\operatorname{Dom} \left({x}\right)$ denote the domain of $x$.

Let $\operatorname{Im} \left({x}\right)$ denote the image of the mapping $x$.

Let $G$ be a class of ordered pairs $\left({x, y}\right)$ satisfying at least one of the following conditions:

$(1): \quad x = \varnothing$ and $y = a$

$(2): \quad \exists \beta: \operatorname{Dom} \left({x}\right) = \beta^+$ and $y = H \left({x \left({\bigcup \operatorname{Dom} \left({x}\right)}\right)}\right)$

$(3): \quad \operatorname{Dom} \left({x}\right)$ is a limit ordinal and $y = \bigcup \operatorname{Rng} \left({x}\right)$.

Let $F \left({\alpha}\right) = G \left({F \restriction \alpha}\right)$ for all ordinals $\alpha$.


$F$ is a mapping and the domain of $F$ is the ordinals, $\operatorname{On}$.
$F \left({\varnothing}\right) = a$
$F \left({\beta^+}\right) = H \left({F \left({\beta}\right)}\right)$
For limit ordinals $\beta$, $\displaystyle F \left({\beta}\right) = \bigcup_{\gamma \mathop \in \beta} F \left({\gamma}\right)$
$F$ is unique.
That is, if there is another function $A$ satisfying the above three properties, then $A = F$.


\(\displaystyle F \left({\varnothing}\right)\) \(=\) \(\displaystyle G \left({F \restriction \varnothing}\right)\) Hypothesis
\(\displaystyle \) \(=\) \(\displaystyle G \left({\varnothing}\right)\) Restriction of $\varnothing$
\(\displaystyle \) \(=\) \(\displaystyle a\) Definition of $G$


\(\displaystyle F \left({\beta^+}\right)\) \(=\) \(\displaystyle G \left({F \restriction \beta^+}\right)\) Hypothesis
\(\displaystyle \) \(=\) \(\displaystyle H \left({F \restriction \beta^+ \left({\bigcup \beta^+}\right)}\right)\) Definition of $G$
\(\displaystyle \) \(=\) \(\displaystyle H \left({F \left({\beta}\right)}\right)\) Union of successor set is the original set by Union of Ordinals is Least Upper Bound


\(\displaystyle F \left({\beta}\right)\) \(=\) \(\displaystyle G \left({F \restriction \beta}\right)\) Hypothesis
\(\displaystyle \) \(=\) \(\displaystyle \bigcup \operatorname{Im} \left({F \restriction \beta}\right)\) Definition of $G$
\(\displaystyle \) \(=\) \(\displaystyle \bigcup_{\gamma \mathop \in \beta} F \left({\gamma}\right)\)


We can proceed in the fourth part by Transfinite Induction.

Basis for the Induction

\(\displaystyle F \left({\varnothing}\right)\) \(=\) \(\displaystyle a\) First part
\(\displaystyle \) \(=\) \(\displaystyle A \left({\varnothing}\right)\) Hypothesis

This proves the basis for the induction.


Induction Step

\(\displaystyle F \left({\beta}\right) = A \left({\beta}\right)\) \(\implies\) \(\displaystyle H \left({F \left({\beta}\right)}\right) = H \left({A \left({\beta}\right)}\right)\) Substitutivity of equality
\(\displaystyle \) \(\implies\) \(\displaystyle F \left({\beta^+}\right) = A \left({\beta^+}\right)\) Second part

This proves the induction step.


Limit Case

\(\displaystyle \forall \gamma \in \beta: F \left({\gamma}\right) = A \left({\gamma}\right)\) \(\implies\) \(\displaystyle \bigcup_{\gamma \mathop \in \beta} F \left({\gamma}\right) = \bigcup_{\gamma \mathop \in \beta} A \left({\gamma}\right)\) Substitutivity of equality
\(\displaystyle \) \(\implies\) \(\displaystyle F \left({\beta}\right) = A \left({\beta}\right)\) Third part

This proves the limit case.