The First-Order axiomatisation of PA is:
- $\forall x. x = x$
- $\forall x, y. x = y \rightarrow y = x$
- $\forall x, y, z. x = y \land y = z \rightarrow x = z$
- $\forall x. 0 \ne S(x)$
- $\forall x, y. S(x) = S(y) \rightarrow x = y$
- $\forall x. x + 0 = x$
- $\forall x, y. x + S(y) = S(x + y)$
- $\forall x. x * 0 = 0$
- $\forall x, y. x * S(y) = x*y + x$
- Axiom schema
Now a thing is eating at me. Why is it that a model where $0$ is the only natural number and $S(x)$ is defined nowhere isn't a model of PA? If $S(0)$ doesn't exist, and furthermore $S(x)$ doesn't exist for any x, wouldn't that be also a nonstandard model?
This is a particular feature of axiomatizations in first-order logic. First-order logic proves $$ (\forall x)(\exists y)[S(x) = y] $$ as part of a general pattern of proving $$ (\forall x)(\exists y)[t(x) = y] $$ whenever $t$ is a term whose only free variable is $x$. To avoid this you would have to work in what is known as "free logic".
But there is little interest in that for the specific case of PA, because of course we do want the successor function to be total, so the fact that the logic ensures this is convenient.