Principle of Recursive Definition for Peano Structure

Theorem

Let $\struct {P, 0, s}$ be a Peano structure.

Let $T$ be a set.

Let $a \in T$.

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

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

$\forall x \in P: \map f x = \begin{cases} a & : x = 0 \\ \map g {\map f n} & : x = \map s n \end{cases}$

Proof

For each $n \in P$, define $\map A n$ as:

$\map A n = \set {h: P \to T \mid \map h 0 = a \land \forall m < n: \map h {\map s n} = \map g {\map h m} }$

This article needs to be linked to other articles. In particular: Ordering $<$ on Peano Structure You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding these links. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{MissingLinks}} from the code.

First, we prove for all $n \in P$ that $\map A n$ is not empty.

More formally, we prove that $A = \set {n \in P: \map A n \ne \O} = P$.

For $n = 0$, there are no $m < n$, so any mapping $h: P \to T$ with $\map h 0 = a$ is an element of $\map A 0$.

Since the constant mapping $\map h n = a$ satisfies this condition, it follows that $0 \in A$.

Now suppose that $n \in A$, and let $h \in \map A n$.

Define $h': P \to T$ by, for all $n' \in P$:

$\map {h'} {n'} = \begin {cases} \map h {n'} & : n' \le n \\ \map g {\map h n} & : n' > n \end {cases}$

To check that $h' \in \map A {\map s n}$, we have to verify that:

$\forall m < \map s n: \map {h'} {\map s m} = \map g {\map {h'} m}$

Since $h \in \map A n$, only the case $m = n$ needs to be verified:

\(\ds \map {h'} {\map s n}\)

\(=\)

\(\ds \map g {\map h n}\)

as $\map s n > n$

\(\ds \)

\(=\)

\(\ds \map g {\map {h'} n}\)

Definition of $h'$

Therefore $h' \in \map A {\map s n}$, and so $\map A {\map s n} \ne \O$.

That means $\map s n \in A$, and by Axiom $(\text P 5)$, we conclude $A = P$.

Now let $A' = \set {n \in P: \forall h, h' \in \map A n: \map h n = \map {h'} n}$.

Then by definition of $\map A )$, it follows that $0 \in A'$.

Suppose now that $n \in A'$, and let $h, h' \in \map A {\map s n}$.

Then:

\(\ds \map h {\map s n}\)

\(=\)

\(\ds \map g {\map h n}\)

as $h \in \map A {\map s n}$

\(\ds \)

\(=\)

\(\ds \map g {\map {h'} n}\)

as $h, h' \in \map A n$

\(\ds \)

\(=\)

\(\ds \map {h'} {\map s n}\)

as $h \in \map A {\map s n}$

Hence $\map s n \in A'$, and by Axiom $(\text P 5)$, we conclude $A' = P$.

Because any $f: \N \to T$ as in the theorem statement needs to be in all $\map A n$, it follows that such an $f$ is necessarily unique.

Finally, we can define $f: P \to T$ by:

$\map f n = \map {h_n} n$

where $h_n \in \map A n$.

It is immediate from the definition of the $\map A n$ that:

$\forall m, n, m < n: \map A n \subseteq \map A m$

Hence, for every $m, n$ such that $m < n$:

$\map {h_m} m = \map {h_n} m$

Thus, for all $m < n$:

$\map f m = \map {h_n} m$

Since $h_n \in \map A n$, it follows that also:

$f \in \map A n$

Thus, since $n$ was arbitrary, it follows that for all $n \in P$:

$\map f {\map s n} = \map g {\map f n}$

as desired.

$\blacksquare$