Definition S.AN.1Let N be a set. We define that (N,s,0) satisfies the axioms of natural numbers if and only if A.S.AN.1 0:-N, A.S.AN.2 s:N-1-1->N\{0}, A.S.AN.3 /\(A:-P(N)) [(0:-A and /\(n:-A) s(n):-A) => A = N].Remark:We will often write (N,s,0) satisfies ANN.Theorem S.AN.2If (N,s,0) satisfies ANN then s:N-onto->N\{0}.ProofLet A = {n:-N\{0}|\/(k:-N) s(k)=n} u {0}. We will show that A = N. It is obvious that 0:-A. Take any n:-A. If n=0 then s(n)=s(0):-A. Assume that n != 0. Then there exists k:-N such that s(k)=n. Since s(s(k)) = s(n), s(n):-A. Thus by A.S.AN.3 A = N. It shows that s:N-onto->N\{0}.Theorem S.AN.3If (N,s,0) satisfies ANN, Y is a set, y:-Y and g:NxY->Y then there exists a unique function f:N->Y such that f(0)=y and /\(n:-N) f(s(n)) = g(n,f(n)).ProofLet D(h) denote the domain of an arbitrary function h. Let K = { h:-P(NxY) | h is a function and (0,y):-h and /\(n:-N) s(n):-D(h) => n:-D(h) and h(s(n)) = g(n,h(n)) }. Let f = u(K). We will later show that f is a function. Let A = {n:-N | \/(z:-Y) (n,z):-f}. Notice that if f is a function then A is the domain of f. We will show that A = N. Since {(0,y)}:-K, 0:-A. Take any n:-A. There exists z:-Y such that (n,z):-f. Hence there exists h:-K such that h(n) = z. If s(n):-D(h) then s(n):-A. Assume that !(s(n):-D(h)). We construct function h1. Let D(h1) = D(h) u {s(n)} and / h(k) for k:-D(h), h1(k) = { \ g(n,z) for k = s(n). It is easy to show that h1:-K. Hence (s(n),g(n,z)):-h1 c f. So s(n):-A. Now by A.S.AN.3 A = N. Let D = {n:-N | /\(y1,y2:-Y) (n,y1),(n,y2):-f => y1 = y2}. We will show that D = N. It is easy to show that 0:-D. Take any n:-D. There exists a unique z:-Y such that (n,z):-f. Take any h:-K such that s(n):-D(h). Then h(s(n)) = g(n,h(n)). Since n:-D and (n,h(n)):-f, h(n) = z. Hence h(s(n)) = g(n,z). But h:-K was arbitralily chosen. Hence /\(h:-K) h(s(n)) = g(n,z). So s(n):-D. Now by A.S.AN.3 D = N. Since A = D = N, f:N->Y. It is obvious that f(0) = y. We will show that /\(n:-N) f(s(n)) = g(n,f(n)). Take any n:-N. There exists h:-K such that h(s(n)) = g(n,h(n)). Since h c f, f(s(n)) = g(n,s(n)). Notice that f:-K. Since f:-K, f is unique.Theorem S.AN.4If (N,s,0) and (N',s',0') satisfy ANN then there exists a unique function f:N->N' such that f(0)=0' and /\(n:-N) f(s(n)) = s'(f(n)). Moreover f:N-1-1-onto->N'.Proof(N,s,0) satisfies ANN. By Theorem S.AN.3 there exists an unique f:N->N' such that f(0) = 0' and /\(n:-N) f(s(n)) = s'(f(n)). We have to show that f:N-1-1-onto->N'. We will show that f:N-onto->N'. Let D = {n':-N'|\/(n:-N) f(n)=n'} It is obvious that 0':-D. Take any n':-D. There exists n:-N such that f(n) = n'. Then f(s(n)) = s'(f(n)) = s'(n'). Hence s'(n'):-D. Since (N',s',0') satisfies ANN, D = N'. Thus f:N-onto->N' We will show that f:N-1-1->N'. Let A = {n':-N | /\(n1,n2:-N) f(n1)=f(n2)=n' => n1=n2} We will show that 0':-A. Assume to the contrary that there exists n!=0 such that f(n)=0'. By Theorem S.AN.2, there exists k:-N such that s(k) = n. Hence 0'=f(n)=f(s(k))=s'(f(k)). Contradiction with A.S.AN.2. Thus 0':-A. Take any n':-A. Take any n1,n2:-N such that f(n1)=f(n2)=s'(n'). Since f(0)=0', n1!=0 and n2!=0. Hence there exists k1,k2:-N such that s(k1)=n1, s(k2)=n2. So f(s(k1))=f(s(k2))=s'(n'). Then s'(f(k1))=s'(f(k2))=s'(n'). Since s:N'-1-1->N', f(k1)=f(k2)=n'. Since n':-A, k1=k2. Hence n1 = n2. Thus s(n'):-A. By A.S.AN 3 A = N. Thus f:N-1-1->N'. This completes the proof.