In Peano arithmetic (first order), we first define natural numbers using a successor function and Peano axioms, then we define addition (and multiplication), and then, we define inequality, as:

$a\leq b\leftrightarrow\exists c\left(a+c=b\right)$

Is there any way to define inequality first, directly from the successor function and Peano axioms? (I mean, if I don't need addition for my purpose, why define it?).


4 Answers 4


In a precise sense, the answer is no. Namely, let $PA_{succ}$ be the set of PA-theorems in the language containing only the symbol for the successor function; then we can show:

There are models of $PA_{succ}$ with no definable linear ordering.

In particular, this means that there is no first-order formula using only successor which PA proves defines a linear ordering.

Specifically, consider the structure (in the language of successor only) $\mathbb{N}+\mathbb{Z}+\mathbb{Z}$. This is a model of $PA_{succ}$ (this takes a bit of work, but isn't hard), but has no definable linear ordering: consider any automorphism swapping the two $\mathbb{Z}$-parts.

(A bit more thought also shows that there is no formula in the language of successor alone which defines a linear ordering in the standard model $\mathbb{N}$; the key ingredient is the proof that $PA_{succ}$ is complete. And in fact thinking along these lines ultimately shows that no model of $PA_{succ}$ has a definable linear ordering.)

  • $\begingroup$ For the asker's benefit, I'll note that this answer addresses the technical notion of first-order definability; "$\le$" is not first-order definable over PA[succ], just as neither are $+$ or $·$. However, if the asker wants a 'recursive definition' of "$\le$" in a way that allows one to recover the usual properties of the ordering based on the other axioms of PA[succ], then my answer or Bram28's answer provide possible ways. $\endgroup$
    – user21820
    Commented Nov 16, 2019 at 19:06
  • $\begingroup$ @user21820 Note that I explicitly mentioned first-order logic in my answer. $\endgroup$ Commented Nov 16, 2019 at 19:06
  • $\begingroup$ Yup; it's just to eliminate the usual confusion that a lot of people have due to having been told that one can recursively define $+$ and $·$ over PA[succ]. It could be due to a misinterpretation of the phrase "recursive definition". $\endgroup$
    – user21820
    Commented Nov 16, 2019 at 19:08
  • $\begingroup$ @user21820 That's a good point. $\endgroup$ Commented Nov 16, 2019 at 19:08
  • $\begingroup$ I upvoted anyway, and I realize that the asker may have been confused and thought the definition of "$\le$" over the usual PA is like the 'definition' of $+,·$ over PA[succ], which it certainly is not. $\endgroup$
    – user21820
    Commented Nov 16, 2019 at 19:17

Let's assume you have the typical axioms for Successor:

$$\forall x \ s(x) \neq 0$$

$$\forall x \forall y \ (s(x) = s(y) \to x = y)$$

and the Axiom Scheme of Induction, which states that for any formula $\varphi(x)$, we have:

$$(\varphi(0) \land \forall x (\varphi(x) \to \varphi(s(x))) \to \forall x \ \varphi(x)$$

Then, if you add:

$$\forall x \forall y (x < y \leftrightarrow (s(x) = y \lor \exists z (y = s(z) \land x < z))) \tag{*}$$

you can prove all of the following:

$$\forall x \ x < s(x)$$

$$\forall x \ \neg x < 0$$

$$\forall x \neg \exists y (x < y \land y < s(x))$$

$$\forall x \ \neg x < x \text{ (irreflexivity)}$$

$$\forall x \forall y (s(x) < s(y) \to x < y)$$

$$\forall x \forall y \forall z ((x < y \land y < z) \to x < z) \text{ (transitivity)}$$

$$\forall x \forall y (x < y \to \neg y < x) \text{ (asymmetry)}$$

$$\forall x \forall y (x = y \lor x < y \lor y < x) \text{ (trichotomy)}$$

So, you can prove all kinds of important and elementary facts about $<$ by adding that one statement to the basic axioms about $s$.

Of course, you would define $x \leq y$ simply as $x < y \lor x = y$ to get results regarding $\leq$, including:

$$\forall x \ x \leq x \text{ (reflexivity)}$$

$$\forall x \forall y \forall z ((x \leq y \land y \leq z) \to x \leq z) \text{ (transitivity)}$$

$$\forall x \forall y (x \leq y \lor y \leq x) \text{ (totality)}$$

Also, once you do add the typical axioms for addition:

$$\forall x \ x+0=x$$

$$\forall x \forall y \ x + s(y) = s(x+y)$$

then you can derive the 'standard' definition of inequality in terms of addition:

$$\forall x \forall y (x \leq y \leftrightarrow \exists z \ x + z = y)$$

In sum: Yes, we can have an alternative definition of smaller than or inequality that allow you to prove important things about it without using the axioms of addition.

  • $\begingroup$ Nice and detailed. I didn't check, but I trust you did so I upvoted. =) $\endgroup$
    – user21820
    Commented Nov 16, 2019 at 19:06
  • 1
    $\begingroup$ @user21820 Thanks, and yes, I have the fully checked proofs :) $\endgroup$
    – Bram28
    Commented Nov 16, 2019 at 19:13
  • $\begingroup$ Wouldn't ∀x∀y(x<y↔s(x)=y∨s(x)<y) work as well? If not, why? $\endgroup$
    – ByteEater
    Commented Aug 12, 2022 at 11:46
  • 1
    $\begingroup$ @ByteEater That wouldn’t work. Note that your statement would be true if we interpret $<$ as a total relationship, i.e. if $x<y$ for any $x$ and $y$ … meaning that it doesn’t capture much of interest at all … certainly not many of the things we want to be true of $<$ $\endgroup$
    – Bram28
    Commented Aug 15, 2022 at 0:42

One way to axiomatize "$\le$" (better not to call it "defining $\le$") that plays very nicely with induction is:

$a≤b ⇔ a=0 ∨ ∃c,d ( c≤d ∧ S(c) = a ∧ S(d) = b )$.

Do not forget that, whether you have addition or not, you must be able to prove that $≤$ is a strict total order. That is what truly matters.

  • $\begingroup$ @NoahSchweber: This is obviously not a definition in the usual sense, and you know that I know it. I took it as granted that the asker meant it in the sense of axiomatizing "$\le$". $\endgroup$
    – user21820
    Commented Nov 16, 2019 at 19:00
  • $\begingroup$ Fair, I suppose I was being uncharitable. $\endgroup$ Commented Nov 16, 2019 at 19:00
  • $\begingroup$ @NoahSchweber: I'll edit anyway to clarify the terminology just in case someone else gets confused (I admit your concern has some validity). $\endgroup$
    – user21820
    Commented Nov 16, 2019 at 19:01
  • $\begingroup$ I've added an answer explaining my concern, and how that can lead to a negative answer to the question. $\endgroup$ Commented Nov 16, 2019 at 19:03

You could try something like$$a\le b\iff Sb\not\leq a\land Sa=b\lor Sa\le b.$$


You must log in to answer this question.

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