Can we replace these two Peano axioms with this single axiom?

Question

Peano Axioms from Mathworld:

1. Zero is a number.

2. If $a$ is a number, the successor of $a$ is a number.

3. zero is not the successor of a number.

4. Two numbers of which the successors are equal are themselves equal.

5. (induction axiom.) If a set $S$ of numbers contains zero and also the successor of every number in $S$, then every number is in $S$.

Q: After defining $1$ to be the successor of $0$, $2$ to be the successor of $1$, etc, can we replace Axioms 3 and 4 with

Axiom 6. $0$, $1$, $2$, etc. are (pairwise) distinct.

Answer 1

Working in second-order logic, consider a language with a constant $0$ and a unary function symbol $S$. Let $\Bbb{N}$ be the set of natural numbers in the meta-theory. Looking at the following axiom systems.

System 1

1. $\neg\exists x \,Sx = 0$
2. $\forall x\forall y \,(Sx=Sy\rightarrow x=y)$
3. $\forall U(0\in U\land (\forall x\, (x\in U\rightarrow Sx\in U)))\rightarrow (\forall x\,x\in U)$, where $U$ quantifies over subsets the universe.

System 2

• $(An,m)$ an axiom schema. For all $n,m\in\Bbb{N}$ such that $n\ne m$, $S^n 0\ne S^m 0$, where $S^n$ is a term applying $S$ $n$ times (and $S^0 0=0)$.
• $(B)$ an axiom same as axiom 3 above.

Assume System 1. To establish the axioms of System 2, we just need to prove $(An,m)$ for all $n,m\in\Bbb{N}$ such that $n\ne m$. Let $n$ be the least natural number such there exists an $m>n$ such that $S^n 0 = S^m 0$.

• If $n=0$ then $0 = S^m 0$, so $0$ is a succesor - in contradiction to axiom 1.
• Otherwise, $S(S^{n-1} 0) = S^n 0 = S^m 0 = S(S^{m-1} 0)$, so by axiom 2, $S^{n-1} 0 = S^{m-1} 0$ in contradiction to $n$ being minimal.

Notice I didn't even have to use the induction axiom 3 to prove this, just that $\Bbb{N}$ is well-ordered in the meta-theory.

Now assume System 2. To establish the axioms of System 1, we need to prove axioms 1 and 2. Let $U=\{S^n 0:n\in\Bbb{N}\}$ in the meta-theory. Since this is second-order logic, $U$ satisfies the assumption of axiom B/axiom 3, so $U$ is the whole universe of the model.

If $0=Sx$ for some $x$ in the universe then there is some $n\in\Bbb{N}$ such that $x=S^n 0$ and then $0=S^{n+1} 0$ which contradicts the axiom $(A0,(n+1))$.

If $x\ne y$ for some $x,y$ in the universe, there are $n,m\in\Bbb{N}$ such that $x=S^n 0, y=S^m 0$ and necessarily $n\ne m$. But then $s^{n+1} 0\ne S^{m+1} 0$ by axiom $(A(n+1),(m+1))$, so $Sx\ne Sy$.

The above proof shows that System 1 and System 2 are equivalent in the sense of $\models$. I'm not sure whether they're equivalent in the sense of $\vdash$, as I'm unfamiliar with deductive systems for second-order logic and they're not complete anyway.

Addendum: System 1 ($S1$) is finite while System 2 ($S2$) is an infinite schema. Any finite subset $S2'\subseteq S2$ has a finite model of a circular buffer. Since any model of $S1$ is isomorphic to $\Bbb{N}$, it follows $S2'\not\models S1$. Assuming that a deductive system of second-order logic allows a proof to only use finitely many axioms - it follows that $S2\not\vdash S1$. On the other hand, the proof that $S1\models S2$ does not use the second-order induction axiom, so it's valid in first-order logic. Since first-order logic has a complete deductive system, $S1\vdash S2$ in first-order logic. Assuming a deductive system of second-order logic can do everything a deductive system of first-order logic can do then $S1\vdash S2$ is second-order logic.

---

Here's a summary if you don't know formal logic

• Axiom $6$ is actually a set of infinitely many axioms.
• Axioms $1+2+3+4+5$ together have only one model up to isomorphism which is $\Bbb{N}$.
• Axiom set $1+2+5+6$ together has only one model up to isomorphism which is $\Bbb{N}$.
• Each and every axiom in $6$ is provable (with a separate finite proof for each) from axioms $1+2+3+4$ together.
• No finite subset of axioms from $1+2+5+6$ can prove either $3$ or $4$ in a finite proof.

So the system consisting of $1+2+3+4+5$ is stronger than $1+2+5+6$ in terms of what you can prove using finite proofs. However, they both categorically model the natural numbers.