Questions about Peano axioms and second-order logic

Question

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.

Answer 1

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.

Answer 2

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