Correct, I *haven't* defined the successor function. There are various variants of the Peano axioms, which take different basic assumptions as starting points. This is *my* version:

We start with a set K, such that 0 ∈ K. We also start with an INJECTIVE function S:K→K (we have no idea as yet what the function might do, or what its values specifically are).

First limiting property of (K,S):

0 is not an element of S(K) (in other words, S is not surjective in a specific way). Although we will not use this property much, it prevents K from being some sort of "cyclical" structure.

Second limiting property of (K,S):

If, for a subset T of K, we have: 0 is in T, and S(t) is in T whenever t is in T, then T = K (this means we can do induction on K by using S). (*)

Clearly, we obviously have: {0,S(0),S(S(0)),.....} ⊆ K. But by (*) we have something much more: {0,S(0),S(S(0)),....} = K.

We would like to say, of course, S(k) = k+1, but we haven't even said what "+" means, yet. Let's fix this:

DEFINITION:

We define a+b, for a,b in K as follows:

a+0 = a

a+S(k) = S(a+k). For example:

S(S(S(0))) + S(S(0)) = S[S(S(S(0))) + S(0)] = S[S{S(S(S(0))) + 0}] = S(S(S(S(S(0))))).

Let's take a moment to be sure we can actually evaluate this for any a,b in K. Since b is in K, we have either:

1)b = 0, in which case we have a+0 = a, or:

2)b = S(k), for some k, in which case we have a+b = a+S(k) = S(a+k).

Of course, to evaluate THIS, we either have:

1A) k = 0, in which case S(a+k) = S(a) in K

2A) k = S(k'), in which case S(a+k) = S(a+S(k')) = S(S(a+k')).

It seems "obvious" this process should terminate in a finite number of steps. Let's try to avoid this by using (*):

Theorem: Let f_{a}, for a given a in K be defined by: f_{a}(b) = a+b. Then f_{a}(b) is in K for all b in K.

Proof: If b = 0, we have f_{a}(b) = a+0 = a, which is in K. Suppose then f_{a}(k) is in K.

We have: f_{a}(S(k)) = a+S(k) = S(a+k) = S(f_{a}(k)), which is in K, since S is a function on K with S(K) ⊆ K. Thus by (*), f_{a}is defined on all of K, and f_{a}(b) ∈ K for all b in K.

DEFINITION:

1 = S(0).

Now we can PROVE S(k) = k+1:

k+1 = k+S(0) = S(k+0) = S(k).

If we make the subsequent definitions:

S(1) = 2, S(2) = 3, etc. we have:

K = {0,S(0),S(S(0)),S(S(S(0))),...} = {0,1,S(1),S(S(1)),....} = {0,1,2,S(2),....} = {0,1,2,3,.....} =.....= N

*****

this "roundabout" way of explicitly defining S:N→N as S(n) = n+1 has the advantage of logically placing the functional concepts before the "operational" concepts (we really need functions before we can even say what a binary operation IS).

The property (*) is KEY: and there is no point in trying to "prove" it, it's not provable (although it is "justifiable" by an appeal to ordinary objects, and our experience with counting things).

(This treatment is based on a development given by Jacobson in Basic Algebra I, and the Wikipedia page on the Peano axioms).