Peano Axioms from Mathworld:

  1. Zero is a number.
  1. If $a$ is a number, the successor of $a$ is a number.
  1. zero is not the successor of a number.
  1. Two numbers of which the successors are equal are themselves equal.
  1. (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.

  • 1
    $\begingroup$ "etc." is a meta-formulation that we cannot use in a formal mathematical language. This is why formal logic is so cumbersome and proofs are usually not formulated in such a language , although they could be formalized. $\endgroup$
    – Peter
    Jul 5, 2023 at 6:18
  • $\begingroup$ @Peter: But then how does one define $1$, $2$, $3$, "etc."? In this context, Tao does use "etc." and so did Peano $\endgroup$
    – user986614
    Jul 5, 2023 at 6:21
  • 1
    $\begingroup$ [1] Authors can & will use "ETC" in Discussions , not in Axioms. Hence Axiom 6 is not valid. [2] More-over , that Axiom 6 will allow Natural numbers to be like 1,2,3,4,1,2,3,4,1,2,3,4,3,4,3,4,.... , where we have Pair-wise Distinct Elements. $\endgroup$
    – Prem
    Jul 5, 2023 at 6:39
  • 1
    $\begingroup$ My Point [1] , you say "ETC" is there in Axioms , It might be good to include that Part in your Post. My Point [2] still stands , though ! $\endgroup$
    – Prem
    Jul 5, 2023 at 6:53

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


You must log in to answer this question.