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

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):

1. $\forall x[S(x)\neq1]$.
2. $\forall x\forall y[x\!\neq\!y\rightarrow S(x)\!\neq\!S(y)]$.
3. 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)?

• The "standard" semantics of FOL assumes that every constant symbol has a denotation; thus (as shown by @Bram28's answer) the simple fact that we have the term $1$ in the language allows us to prove $\exists x (x=1)$. What we can do is avoid $1$ and add the axiom $\exists x \forall y (x \ne S(y))$ and then expand the language adding the new symbol $1$. – Mauro ALLEGRANZA Oct 29 '17 at 8:36

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 ...

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.