Transfinite Recursion Theorem/Formulation 3

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\On$ denote the class of all ordinals.

Let $h$ and $f$ be mappings defined for all sets.

Let $c$ be a set.


Then there exists a unique mapping $F$ on $\On$ such that:

\((1)\)   $:$      \(\ds \map F 0 \)   \(\ds = \)   \(\ds c \)      
\((2)\)   $:$     \(\ds \forall \alpha \in \On:\)    \(\ds \map F {\alpha^+} \)   \(\ds = \)   \(\ds \map h {\map F \alpha} \)      
\((3)\)   $:$     \(\ds \forall \lambda \in K_{II}:\)    \(\ds \map F \lambda \)   \(\ds = \)   \(\ds \map f {F \sqbrk \lambda} \)      

where $K_{II}$ denotes the class of all limit ordinals.


Proof

For an arbitrary ordinal sequence $\theta$, let us define $\map g \theta$ by the following conditions:

\((1)\)   $:$   If the length of $\theta$ is $0$:       \(\ds \map g \theta \)   \(\ds = \)   \(\ds c \)      
\((2)\)   $:$   If the length of $\theta$ is $\alpha^+$:       \(\ds \map g \theta \)   \(\ds = \)   \(\ds \map h {\map \theta \alpha} \)      
\((3)\)   $:$   If the length of $\theta$ is $\lambda$:       \(\ds \map g \theta \)   \(\ds = \)   \(\ds \map f {\Img \theta} \)      


By the Transfinite Recursion Theorem: Formulation 2, there exists a unique mapping $F$ on $\On$ such that:

$\forall \alpha \in \On: \map F \alpha = \map g {F \restriction \alpha}$


Hence we have:

\(\text {(1)}: \quad\) \(\ds \map F 0\) \(=\) \(\ds \map g {F \restriction 0}\)
\(\ds \) \(=\) \(\ds c\) as $F \restriction 0$ has length $0$
\(\text {(2)}: \quad\) \(\ds \map F {\alpha^+}\) \(=\) \(\ds \map g {F \restriction {\alpha^+} }\)
\(\ds \) \(=\) \(\ds \map h {\map {\paren {F \restriction {\alpha^+} } } \alpha}\) as $F \restriction {\alpha^+}$ has length $\alpha^+$
\(\ds \) \(=\) \(\ds \map h {\map F \alpha}\)
\(\text {(3)}: \quad\) \(\ds \map F \lambda\) \(=\) \(\ds \map g {F \restriction \lambda}\) where $\lambda$ is a limit ordinal
\(\ds \) \(=\) \(\ds \map f {\Img {F \restriction \lambda} }\) as $F \restriction \lambda$ has length $\lambda$
\(\ds \) \(=\) \(\ds \map f {F \sqbrk \lambda}\)

$\blacksquare$


Sources