I hope I am not going to drive people buggy by what most might consider obvious but I must ask.

Peano’s axioms define the basic properties of the set of natural numbers but does not attempt to enumerate them because they are the “given” and can be expressed many different ways, slash marks, Arabic numbers, Roman numerals etc.

But I take it that:

given x e N, x = 501, I am allowed to write,

x’ = 501’ = 502 because we are familiar with the system of Arabic numbers and know what symbol follows 501.

Theorem 3 establishes that every natural number except 1 has a precursor.

If Peano’s axioms allow 501’ -> 502. It does it also allow writing 502 -> 501’?

If not, does Theorem 3 allow writing 502 -> 501’.

Hmmm, going out on a limb here but in thinking about it I guess I am pondering whether the successor function, though injective and surjective on N-{1} is also bijective. I am torn because I was thinking that any injective function that is also surjective must also be bijective but that would mean the the successor function would automatically define a precursor function, I think ... and that does not seem right, otherwise I would have run across it in the literature.

Does Theorem 3 establish that the successor function is a bijection?

My question is prompted by considering how to prove Theorem #4 which establish addition as an operation.

Well, once again I feel like a curious fly brain again caught in a spider web, ah well ...