Questions about Peano axioms and second-order logic

I have what I hope are some simple questions regarding the Peano axioms. I am reading Terence Tao's book "Analysis 1" where he constructs the natural numbers using the Peano axioms, but the axioms are written in plain English. I want to convert these axioms into FOL sentences (and SOL sentence for the axiom of induction).

However, I can't find a complete and consistent list of these axioms in this form, so I have pieced together from various sources how I think they should be:

Signature: $\mathcal{L} = \{\mathbb{N}, 0, S\}$

1. $\exists x(x = 0 \wedge x \in \mathbb{N})$
2. $\forall n(n \in \mathbb{N} \to S(n) \in \mathbb{N})$
3. $\forall n(S(n) \ne 0)$
4. $\forall m \forall n(S(m) = S(n) \to m = n)$
5. $\forall P(P(0) \wedge (P(n) \to P(S(n))) \to \forall n P(n))$

First question: Is this a correct way of writing the axioms in logic?

Second question: The signature for the Peano axioms doesn't include the $\in$ symbol as a non-logical symbol in any of the treatments I've encountered on the web. Does this mean that the membership predicate is in some way "built-in" to second-order logic so that you don't need to declare it in the signature? To me this makes sense, since SOL can quantify over sets of objects, so therefore the notion of what a set is and what membership is, is integral to SOL.

See First-order theory of arithmetic for the "standard" first-order translation.

Definition 2.1.1 (Informal) of natural number. Not applicable: the set $\mathbb N$ will be "characterized" by the axioms as the domain of the relevant interpretation.

Axiom 2.1: $0$ is a natural number. Not needed: the language has an individual constant $0$ that "names" the number zero.

Axiom 2.2: If $n$ is a natural number, then $n++$ is also a natural number. Not needed: the function symbol $++$ (more usually: $S$) is interpreted as the successor function from the domain $\mathbb N$ to $\mathbb N$ (like every function symbols in first-order language).

And so on...

Axiom 2.5 (Principle of mathematical induction). Your SOL translation is correct.

Regarding $\in$, it is not a "logical" symbol in first order logic; thus, we have it only in the mathematical heories that need it.

Mathematical theories are obtained from the logical machinery (e.g. the language of first-order logic with equality) adding specific non-logical symbols (and the relevant axioms):

• first order arithemetic is obtained adding to the logical language an individual constant: $0$, and three function symbols: $S, +, \times$;

• first order set theory is obtained adding a single non-logical symbol: the (binary) predicate symbol $\in$.

For second-order arithmetic, a usual axiomatisation is:

$\forall x (Sx \ne 0) \land \forall x \ \forall y (Sx = Sy \to x = y)$ --- (successor axiom)

$\forall x (x+0=x) \land \forall x \ \forall y (x+sy=s(x+y))$ --- (addition axiom)

$\forall x (x \times 0=0) \land \forall x \ \forall y (x \times sy=x \times y +x))$ --- (multiplication axiom)

$\forall X ((X0 \land \forall x (Xx \to XSx)) \to \forall x Xx)$ --- (induction axiom).

For more details, see Second-order arithmetic.

• So are you saying that axioms 1 and 2 in my formulation are unnecessary, as they are asserted in the signature? Therefore 3, 4 and 5 are the only axioms required? – esotechnica Jul 18 '17 at 10:34
• @esotechnica - exactly; In FOL you cannot have a "name" (individual constant) for a subset of the domain $\mathbb N$. Individual constant are interpreted as names for elements of the domain, like $0$ for the number zero. – Mauro ALLEGRANZA Jul 18 '17 at 11:06
• If so, the purported axiom $\exists x (x=0)$is unnecessary: from $0=0$ (derivable from equality axiom: $\forall x (x=x)$ we can derive $\exists x (x=0)$. – Mauro ALLEGRANZA Jul 18 '17 at 11:07
• If you are working in FOL, and thus 5 must be expressed as an axiom schema, with $\varphi$ in place of $P$, you have to add also the recursive axioms for $+$ and $\times$, because in FOL we cannot define them. – Mauro ALLEGRANZA Jul 18 '17 at 11:09
• One final question, if I'm working in SOL rather than FOL, is it possible to define $+$ and $\times$ in terms of S? That is, there is no need to add $+$ and $\times$ to the signature? – esotechnica Jul 18 '17 at 11:25

Stated in the language of set theory:

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

Using these axioms, the required addition, multiplication and exponentiation functions can be constructed, i.e. they can be proven to exist on $N$.