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

Question

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]$?

Answer 1

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

Answer 2

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$

I would suggest instead:

$[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.