# Predicate formulas on the natural numbers using only $\le$.

We want to find predicate formulas about the natural numbers using only the $\le$ predicate and no constants. For instance, the following predicate formula defines equality:

$[x=y] ::= [x \le y \; \land y \le x].$

And then, using that we can define $[x>0]$:

$[x>0]::= \exists y. x\neq y \; \land y \le x.$

$[x =0]$ is then:

$[x =0]::= [\forall y \ x \le y].$

Now, then, how would I define $[x = y+1]$?

$x=y+1$ iff both $x>y$ and there is no $z$ with $x>z$ and $z>y$.

First, I would like to point out a problem. You define:

$[x =0]::= [x \le 0 \; \land 0 \le x].$

But as such, you are using the constant $0$

$[x =0]::= \forall y \ x \le y$

Also, I would suggest to define the following two useful predicates:

$[x>y]::= \neg x \le y$

$[x<y]::= y > x$

Indeed, the latter allows us to quickly define:

$[x = y+1]::= [\forall z ( z < x \leftrightarrow z \le y)]$

Let's show that this is arithmetically equivalent to Lord Shark's suggestion:

$x=y+1$ iff both $x>y$ and there is no $z$ with $x>z$ and $z>y$.

which formulates to:

$x=y+1:== [x>y \land \neg \exists z (x>z \land z>y)]$

This is equivalent to:

$x=y+1:== [x>y \land \forall z (\neg x>z \lor \neg z>y)]$

which is the same as:

$x=y+1:== [x>y \land \forall z (x \le z \lor z \le y)]$

Now, we can note that we have $x > y$ if and only if we cannot both have $x \le z$ and $z \le y$, and so this is the same as saying:

$x=y+1:== [\forall z \neg (x \le z \land z \le y) \land \forall z (x \le z \lor z \le y)]$

which is equivalent to:

$x=y+1:== \forall z [\neg (x \le z \land z \le y) \land (x \le z \lor z \le y)]$

and that is equivalent to:

$x=y+1:== [\forall z (x \le z \ XOR \ z \le y)]$

which is:

$x=y+1:== [\forall z (\neg x \le z \leftrightarrow z \le y)]$

which is:

$x=y+1:== [\forall z (x > z \leftrightarrow z \le y)]$

and thus:

$x=y+1:== [\forall z (z < x \leftrightarrow z \le y)]$

Personally, I really like biconditionals, because they are great to work with in practice: if you have one side, you can infer the other side, and if you have a negation of one side, you can infer the negation of the other side.

• Thank you for the correction. I admit I prefer the formulation of the predicate another user implied, using $\lnot \exists z(z<x \land y<z)$, and then simplifying to $\forall z(x \le z \lor z \le y)$ Could you speak to reconciling your formulation using the biconditional with what I have done here (or indeed, if there's anything I've done incorrectly)? – Kanpachi Jun 5 '18 at 22:28
• @Kanpachi You did that correctly, and I showed the arithmetical equivalence of those formulations in my post – Bram28 Jun 6 '18 at 12:29