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