Principle of Recursive Definition for Peano Structure

From ProofWiki
Jump to navigation Jump to search


Let $\left({P, 0, s}\right)$ 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: f \left({x}\right) = \begin{cases} a & : x = 0 \\ g \left({f \left({n}\right)}\right) & : x = s \left({n}\right) \end{cases}$


For each $n \in P$, define $A \left({n}\right)$ as:

$A \left({n}\right) = \left\{{h: P \to T}\,\middle\vert\,{h \left({0}\right) = a \land \forall m < n: h \left({s \left({m}\right)}\right) = g \left({h \left({m}\right)}\right)}\right\}$

First, we prove for all $n \in P$ that $A \left({n}\right)$ is not empty.

More formally, we prove that $A = \left\{{n \in P: A \left({n}\right) \ne \varnothing}\right\} = P$.

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

Since the constant mapping $h \left({n}\right) = a$ satisfies this condition, it follows that $0 \in A$.

Now suppose that $n \in A$, and let $h \in A \left({n}\right)$.

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

$h' \left({n'}\right) = \begin{cases} h \left({n'}\right) & : n' \le n \\ g \left({h \left({n}\right)}\right) & : n' > n \end{cases}$

To check that $h' \in A \left({s \left({n}\right)}\right)$, we have to verify that:

$\forall m < s \left({n}\right): h' \left({s \left({m}\right)}\right) = g \left({h' \left({m}\right)}\right)$

Since $h \in A \left({n}\right)$, only the case $m = n$ needs to be verified:

\(\displaystyle h' \left({s \left({n}\right)}\right)\) \(=\) \(\displaystyle g \left({h \left({n}\right)}\right)\) Since $s \left({n}\right) > n$
\(\displaystyle \) \(=\) \(\displaystyle g \left({h' \left({n}\right)}\right)\) Definition of $h'$

Therefore $h' \in A \left({s \left({n}\right)}\right)$, and so $A \left({s \left({n}\right)}\right) \ne \varnothing$.

That means $s \left({n}\right) \in A$, and by Axiom $(P5)$, we conclude $A = P$.

Now let $A' = \left\{{n \in P: \forall h, h' \in A \left({n}\right): h \left({n}\right) = h' \left({n}\right)}\right\}$.

Then by definition of $A \left({0}\right)$, it follows that $0 \in A'$.

Suppose now that $n \in A'$, and let $h, h' \in A \left({s \left({n}\right)}\right)$.


\(\displaystyle h \left({s \left({n}\right)}\right)\) \(=\) \(\displaystyle g \left({h \left({n}\right)}\right)\) Since $h \in A \left({s \left({n}\right)}\right)$
\(\displaystyle \) \(=\) \(\displaystyle g \left({h' \left({n}\right)}\right)\) Since $h, h' \in A \left({n}\right)$
\(\displaystyle \) \(=\) \(\displaystyle h' \left({s \left({n}\right)}\right)\) Since $h \in A \left({s \left({n}\right)}\right)$

Hence $s \left({n}\right) \in A'$, and by Axiom $(P5)$, we conclude $A' = P$.

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

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

$f \left({n}\right) = h_n \left({n}\right)$

where $h_n \in A \left({n}\right)$.

It is immediate from the definition of the $A \left({n}\right)$ that:

$\forall m, n, m < n: A \left({n}\right) \subseteq A \left({m}\right)$

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

$h_m \left({m}\right) = h_n \left({n}\right)$

Thus, for all $m < n$:

$f \left({m}\right) = h_n \left({m}\right)$

Since $h_n \in A \left({n}\right)$, it follows that also:

$f \in A \left({n}\right)$

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

$f \left({s \left({n}\right)}\right) = g \left({f \left({n}\right)}\right)$

as desired.