In Peano's Axioms are the uniqueness of the successor and the property $x^{\prime}=y^{\prime}\implies{x=y}$ redundant?

This seems obvious to me, but I may be missing something. In the various forms of the axioms used as the basis of natural number arithmetic that I have seen, the successor of a number is, in the axiom stating its existence, defined to be a unique number. That appears to require that $x^{\prime}=y^{\prime}\implies{x=y}$. So stating this result as an additional axiom is redundant.

On the other hand, $x^{\prime}=y^{\prime}\implies{x=y}$ seems insufficient to show that the successor of a number is unique.

From my perspective, such a redundancy is not particularly offensive if it aids in the applicability of the set of axioms. But such a feature should be explained, perhaps in a footnote. Since I have seen no such footnote, I am motivated to ask if others agree with my understanding.

  • 8
    $\begingroup$ No, it is not redundant. Consider the set $\{0,1\}$ with successor function $0’=1$, $1’=1$. It satisfies the “other” axioms: $0$ is in the set; if $x$ is in the set then $x’$ is in the set. There is no $y$ in the set with $y’=0$. And if $S$ is a collection of elements of the set that includes $0$ and such that if $x\in S$ then $x’\in S$; then $S$ is the whole set. But this set does not satisfy that $x’=y’$ implies $x=y$. That means that this axiom is not redundant: it cannot be derived from the other four. $\endgroup$ Commented Apr 16, 2019 at 15:32
  • $\begingroup$ In my book, the successor function is one-to-one. $\endgroup$
    – Wuestenfux
    Commented Apr 16, 2019 at 15:34
  • 7
    $\begingroup$ @Wuestenfux: That’s exactly equivalent to the statement that $x’=y’$ implies $x=y$. $\endgroup$ Commented Apr 16, 2019 at 15:36
  • $\begingroup$ @Wuestenfux The statement of Axiom II which motivated my question is: "To every number $a$ there corresponds a unique number $a^{\prime}$, called the successor of $a$." Today I was reading "unique" to apply to $a^\prime$ among all numbers, and not merely relative to $a.$ The axiom intends the correspondence to be unique. On other days, I read the axiom as it was intended. $\endgroup$ Commented Apr 16, 2019 at 16:01
  • 4
    $\begingroup$ The statement: $x^\prime=y^\prime\implies x=y$ isn’t about uniqueness of successor, it’s about uniqueness of predecessor. Uniqueness of successor is: $x=y\implies x^\prime=y^\prime$. $\endgroup$ Commented Apr 16, 2019 at 16:32

4 Answers 4



We state that the successor relation $s(n)$ is defined by a function, in order to guarantee that there are no multiple values for the same argument.

But a function can map two arguments to the same value.

This is why we rquire that :

$\text { if } s(n)=s(m), \text { then } n=m$.

I.e., by contraposition, if the two arguments $n$ and $m$ are distinct, also their successors must be.

This is why Peano (1889) original formulation stated :

$\text { for all natural numbers } m \text { and } n ( m = n \text { if and only if } s(m) = s(n))$.

In the modern formulation in the language of first-order logic, the successor relation is expressed with a function symbol $s(n)$. Thus, the "functionality" is built-in into the rules of the language and thus the corresponding axiom amounts to :

$\text { for every } n, m (\text { if } s(n) = s(m), \text { then } n=m )$.

This axioms is necessary to ensure the infinity of the number sequence; withou it, we may have some sort of "circularity", like e.g. $s(10)=2$. In this case, we have that both $1$ and $10$ have the same successor.

  • $\begingroup$ Indeed. In terms of functions as ordered pairs, the first element must be unique, so each pair is unique. But that does not require the second elements to be mutually unique. $\endgroup$ Commented Apr 16, 2019 at 15:40
  • $\begingroup$ I should add. BBFSK do not explicitly define a successor function. If the axiom were stated in terms of a function, then the word unique could be omitted and there would be no ambiguity. IIRC, Stoll (among most others) explicitly state that the successor of $n$ is the value of a successor function. $\endgroup$ Commented Apr 24, 2019 at 19:14
  • 1
    $\begingroup$ @StevenHatton - see BBFSK, page 93 The Peano System of Axioms : "The number formed by writing a vertical stroke to the right of the number $a$ is called the successor [emphasis added] of $a$". $\endgroup$ Commented Apr 25, 2019 at 9:24
  • $\begingroup$ I take the entire discussion prior to the statement of Peano's axioms as informal, and motivational; not definitive. But my point is that they do not explicitly call it a function. In most contexts function means for each element of the domain, there is exactly one image element. That is, to each $a$ there corresponds a unique number called the successor of $a$. Which I contend is an ambiguous statement without further clarification. $\endgroup$ Commented Apr 26, 2019 at 13:27

This is not redundat. Consider only the sentence $\phi\equiv\forall x\exists !y(y=S(x))$. Where $S$ is the succesor function. Now, consider the structure $\mathfrak{A}:=(M,S)$ where $M=\{0,1,2\}$, $S(i)=i+1$ if $i<2$ and $S(2)=2$. Here you see that $\mathfrak{A}\models\phi$ but $\mathfrak{A}\models\exists x, y(S(x)=S(y)\wedge x\neq y)$.


Let's say that S is the relation : the natural number y is a successor of the natural number x. That is to say , the relation S is a subset of the cartesian product " N cross N" such that:

S = { (x,y) | the nat.number y is a successor of the nat. number x }

Remark. Here I say " a successor" since S being only defined at this stage as a relation, nothing prevents a natural number x to have more that more than one successor. Things will change at the next stage.

The fact that the relation S is furthermore defined as a function guarantees that (1) each natural number has a successor and (2) not more than 1: briefly it guarantees each natural number has a unique successor.

Adding to this that " S(x) is equal to S(y)" implies that " x is equal to y" ( by contraposition, that " x is different from y" implies that " S(x) is different from S(y) " ) guarantees that no two different natural numbers have the same successor, in other words it guarantees that each natural number has its own/ proper successor . It means technically that the successor function is " one-one" ( injective).

Let us notice that although the function S from N to N is injective ( one-one) it is not surjective ( " onto"). This is because the natural number 0 is not the image of any natural number under the function S : there is no natural number x such that S(x) = 0


Visually, the successor relation on $N$ (from Peano's Axioms) should look like this:

enter image description here

We don't want anything like this:

enter image description here

Every number must be mapped to a unique successor. So, we require that the successor relation be a function.

We also don't want anything like this:

enter image description here

The predecessor of any number, if it exists, must also be unique. So, we require that the successor function be injective (to answer your question).

More on this topic at my blog posting here.

  • 1
    $\begingroup$ @StevenHatton Your question is really about the uniqueness of predecessors on N. If you dropped this requirement of the natural numbers, you could have as few two numbers in your system (0 and 1), as expressed by so well by Arturo in his comment to your question. In his example, 1 has two different predecessors, namely 0 and 1 itself. (I would write it as S(0)=S(1)=1.) As he points out, the other four of Peano's Axioms would be satisfied by such a structure. $\endgroup$ Commented Apr 18, 2019 at 3:35
  • 1
    $\begingroup$ @StevenHatton That just says the successor relation is a function. Arturo's example would still not be avoided. If you have $N = \{ 0, 1\}$ then you could still have a function $S: N \to N$ such that $S(0)=S(1)=0$ and that would satisfy the other 4 of Peano's Axioms. $1$ would still have two different pre-images (or predecessors) under $S$. It would be a many-to-one function, which you don't want.. $\endgroup$ Commented Apr 18, 2019 at 17:34
  • 1
    $\begingroup$ @StevenHatton No. The successor function in Peano's Axioms is NOT bijective since the "first number" (whether you call it $0$ or $1$) has no pre-image in $N$ under that function. $\endgroup$ Commented Apr 19, 2019 at 17:56
  • 1
    $\begingroup$ @StevenHatton Read my previous comment carefully. $\endgroup$ Commented Apr 19, 2019 at 18:52
  • 1

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .