Definition of Successor function in Peano Axioms

Question

Dedekind-Peano axioms characterize (in first-order logic) the natural numbers ($\mathbb{N}$) as follows:

A1. $0 \in \mathbb{N}$.

A2. $\forall n \in \mathbb{N}: n' \in \mathbb{N}$.

A3. $\forall n \in \mathbb{N}: n' \not= 0$.

A4. $\forall n,m \in \mathbb{N}: n' = m' \rightarrow n = m$.

A5. $[(0) \land \forall n \in \mathbb{N}: \varphi(n) \rightarrow \varphi(S(n))] \rightarrow \forall n \in \mathbb{N}: \varphi(n)$.†

My question is about the implicit definition of the successor function $(\cdot)'$. It seems to me that we need to define it (which means, at least, that we need to specify its domain and codomain) in order for A1-5 to be meaningful. But can we even say so little as that it is a mapping from $\mathbb{N}$ to $\mathbb{N}$ when A1-A5 are what define $\mathbb{N}$? Is there not a circularity there? If 'no', might it be that $(\cdot)'$ is given all of its relevant meaning by A1-A5?

---

† A5 is not really an axiom but a schema for generating an infinity of actual axioms for each $\phi$.

Answer 1

Your line 2 is equivalent to $': N\to N$.

It's would be a little more clear if you used the notation $S: N\to N$. Then $n'$ becomes $S(n)$.

Answer 2

As said by Dan, Axiom 2 says that the successor $S$ is a mapping from $\mathbb{N}$ into $\mathbb{N}$.

Axiom 4 says that it is injective, i.e. two different numbers cannot have the same successor.

But you must take into account that the "proper" context for the translation of the original Dedekind-Peano axioms must be second-order logic.

If we are working with first-order logic, things are slightly different.

See S.C.Kleene, Mathematical Logic (1967, Dover reprint), pag.209 :

" Axiom 14 [i.e. $ a' = b' \rightarrow a = b$] and Axiom 15 [i.e. $\lnot a = 0$] and Axiom Schema 13 [i.e. f-o induction schema] formalize the third, fourth and fifth of Peano's list of five axioms for the natural numbers, 1889. Peano's first axiom, that $0$ is a natural number, and his second axiom, that if $n$ is a natural number so is $n+1$, are taken care of instead by the formation rules [of the f-o language] which make $0$ a term and whenever $r$ is a term make $(r)'$ a term, since all the terms in the system are interpreted as expressing natural numbers."

Answer 3

In the definition of an interpretation of first-order logic we require that if $M$ is an interpretation to a language, and $F$ is an $n$-ary symbol function, then the interpretation $F^M$ is a function from $M^n$ to $M$.

The syntax does not concern itself with such issues, and axioms are part of the syntax, rather than the semantics.