[090] Trace of proof. Note that the proof only uses Peano’s axioms and induction. Given \(m∈ℕ,m≠ 0\) we recall that \(S^{-1}(m)\) is the predecessor, see 131 (using the arithmetic we may write

but this theorem is needed to define the arithmetic...) For any given \(R⊆ ℕ× A\) we define the projection on the first component

Consider the family \({\mathcal F}\) of relations \(R⊆ ℕ× A\) that satisfy

We show that under these conditions \(𝜋(R)=ℕ\); we know that \(0∈ 𝜋(R)\); if \(m\in 𝜋(R)\), then there exists \(x∈ A\) for which \((m,x)∈ R\) from which for ** follows \((S(m),g_{m}(x))∈ R\), and we obtain \(S(m)∈ 𝜋(R)\).

The family \({\mathcal F}\) is not empty because \(ℕ× A∈ {\mathcal F}\). Let then \(T\) be the intersection of all relations in \({\mathcal F}\). \(T\) is therefore the least relation in \({\mathcal F}\).

It is possible to verify that \(T\) satisfies the previous * and ** properties. In particular \(𝜋(T)=ℕ\).

We must now show that \(T\) is the graph of a function (which is the desired \(f\) function), that is, that for every \(n\) there is a single \(x∈ A\) for which \((n,x)∈ T\).

Let \(A_ n=\{ x∈ A, (n,x)∈ T \} \); we write \(|A_ n|\) to denote the number of elements in \(A_ n\); since \(𝜋(T)=ℕ\) then \(|A_ n|≥ 1\) for every \(n\). We will show that \(|A_ n|=1\) for each \(n\). We will prove it by induction. Let

Let’s see the induction step.

Suppose by contradiction that \(|A_{m}|=1\) but \(|A_{Sm}|≥ 2\); morally at \(m\) the graph of the function \(f\) ”forks” and the function becomes ”multivalued”. We define for convenience \(w=g_{m}(x),k=Sm\); we may remove some elements to \(T\) (those that do not have a ”predecessor” according to the relation **) defining

it is possible to show that \(\tilde T\) satisfies * and **, but \(\tilde T\) would be smaller than \(T\), against the minimality of \(T\). To prove that \(P(0)\) holds, we define \(k=0,w=a\) and proceed in the same way.

The previous reasoning also shows that the function is unique, because if the graph \(G\) of any function satisfying to * and ** must contain \(T\), then \(T=G\).