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$.
Best Answer
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)$.