Principle of Recursive Definition for Minimal Infinite Successor Set

From ProofWiki
Jump to navigation Jump to search


Let $\omega$ be the minimal infinite successor set.

Let $T$ be a set.

Let $a \in T$.

Let $g: T \to T$ be a mapping.

Then there exists exactly one mapping $f: \omega \to T$ such that:

$\forall x \in \omega: \map f x = \begin {cases} a & : x = \O \\ \map g {\map f n} & : x = n^+ \end {cases}$

where $n^+$ is the successor set of $n$.


Take the function $F$ generated in the second principle of transfinite recursion.

Set $f = F {\restriction_\omega}$.

\(\displaystyle \map f \O\) \(=\) \(\displaystyle \map F \O\) $\O \in \omega$
\(\displaystyle \map f {n^+}\) \(=\) \(\displaystyle \map F {n^+}\) $n^+ \in \omega$
\(\displaystyle \) \(=\) \(\displaystyle \map g {\map F n}\) Second Principle of Transfinite Recursion
\(\displaystyle \) \(=\) \(\displaystyle \map g {\map f n}\) $n \in \omega$ and the definition of $f$

Therefore, such a function exists.

Now, suppose there are two functions $f$ and $f'$ that satisfy this:

$\map f \O = \map {f'} \O$


\(\displaystyle \map f {n^+}\) \(=\) \(\displaystyle \map g {\map f n}\) By Hypothesis
\(\displaystyle \) \(=\) \(\displaystyle \map g {\map {f'} n}\) Inductive Hypothesis
\(\displaystyle \) \(=\) \(\displaystyle \map {f'} {n^+}\) By Hypothesis

This completes the proof.