Formulation of the Successor Function as an Endofunction in First-Order Logic

Question

The Peano axioms are often listed (among other ways) as a set of 5 axioms in an informal language or 3 axioms in a formal language. For example:

Informal (see, e.g., http://mathworld.wolfram.com/PeanosAxioms.html):

1. 1 is a natural number.
2. The successor function $S$ is an endofunction (i.e., the domain and codomain of $S$ are equal such that if $n\in\mathbb{N}$, then $S(n)\in\mathbb{N}$).
3. The image of $S$ does not contain 1 (i.e., 1 is not the successor $S(x)$ of any $x\in\mathbb{N}$).
4. The successor function $S$ is injective.
5. Induction Axiom: If $A$ is a set of natural numbers such that $1\in A$, and $k\in A$ implies $k+1\in A$ for any $k$, then $A=\mathbb{N}$.

Formal First-Order Logic (see, e.g., wikipedia:Peano_Axioms):

3. $\forall x[S(x)\neq1]$.
4. $\forall x\forall y[x\!\neq\!y\rightarrow S(x)\!\neq\!S(y)]$.
5. As an axiom schema: $\varphi(1/x)\wedge\forall x[\varphi\rightarrow\varphi(S(x)/x)])\rightarrow\forall x\varphi.\ $ (In a second-order logic, this can be written as a single axiom).

(Note: in this presentation, the equality axioms are considered to be part of the underlying logical system of axioms, and not part of the "Peano axioms".)

A prior question considered whether axioms 1 and 2 from the informal list can be considered axioms from the context of a formal logic. The answer given there was, in part, as follows:

Today ... the fact that function symbols are interpreted by total functions are taken as part of the underlying "logic", apart from the "theory" that is being studied. So axioms 1 and 2 are not needed as axioms. ...

My Question: It seems clear that even if axioms 1 and 2 are not required in a first-order presentation, axiom 1 could still be presented as: $$ \exists x[x=1]. $$ However, it is not clear to me how one could present axiom 2. The prior answer suggests that all functions provided in the signature of a first-order logic are "total functions", which could (?) be written as: $$ \forall x\forall y[x\!=\!y\rightarrow S(x)\!=\!S(y)]. $$ But how would one state in first-order that a function is an endofunction (or is that, too, implicitly given by the construct of a first-order logic)?

Answer 1

This does not answer your quesrion as to how you would formalize that $s$ is an endo-function (I suspect that maybe you'd need second-orer logic to do this, but I'm not any good at that ...), but I'd like to point out that both of your your suggested axioms are first-order logic tautologies:

$\exists x x =1$ is a necessarily true statement in FOL, and can be proven from nothing as follows:

$1. 1=1 \quad = \ Intro$

$2. \exists x \ x =1 \quad \exists \ Intro 1$

$\forall x \forall y (x=y \rightarrow s(x) = s(y))$ is also a nessarily true statement in FOL, and can be proven as follows:

$1. x=y \quad Assumption$

$2. s(x) =s(x) \quad = \ Intro$

$3. s(x) =s(y) \quad = \ Elim 1,2$

$4. \forall x \forall y (x=y \rightarrow s(x) =s(y)) \quad \forall \ Intro 1-3$

So I guess this is why they do not need to be axiomatized and are inherently part of FOL ...

Answer 2

In your "formal" system here, the domain of discourse is implicitly assumed to be the natural numbers, i.e. everything is assumed to be a natural number. So, $1$ is a natural number. So is, $S(x)$ for all $x$, i.e. for all natural numbers $x$.

BTW, your "informal" axioms can be easily formalized as follows using the notation of set theory:

1. $1 \in N$
2. $\forall x\in N: S(x)\in N$
3. $\forall x\in N: S(x)\neq 1$
4. $\forall x, y\in N: [S(x)=S(y) \implies x=y]$
5. $\forall A\subset N:[1\in A \land \forall x\in A: S(x)\in A \implies A=N]$

Note that that nothing but $1$ is explicitly assumed here to be a natural number. $N$ itself is not assumed to be a natural number. With set theory available, we an construct any number of things that are not themselves natural numbers, e.g. the set of even numbers, and various functions on $N$ such as addition and multiplication.