0
$\begingroup$

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?).

$\endgroup$
2
$\begingroup$

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

$\endgroup$
  • $\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 Nov 16 '19 at 19:06
  • $\begingroup$ @user21820 Note that I explicitly mentioned first-order logic in my answer. $\endgroup$ – Noah Schweber Nov 16 '19 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 Nov 16 '19 at 19:08
  • $\begingroup$ @user21820 That's a good point. $\endgroup$ – Noah Schweber Nov 16 '19 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 Nov 16 '19 at 19:17
2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Nice and detailed. I didn't check, but I trust you did so I upvoted. =) $\endgroup$ – user21820 Nov 16 '19 at 19:06
  • 1
    $\begingroup$ @user21820 Thanks, and yes, I have the fully checked proofs :) $\endgroup$ – Bram28 Nov 16 '19 at 19:13
2
$\begingroup$

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.

$\endgroup$
  • $\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 Nov 16 '19 at 19:00
  • $\begingroup$ Fair, I suppose I was being uncharitable. $\endgroup$ – Noah Schweber Nov 16 '19 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 Nov 16 '19 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$ – Noah Schweber Nov 16 '19 at 19:03
1
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.