1
$\begingroup$

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

$\endgroup$
3
$\begingroup$

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

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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)? $\endgroup$ – Kanpachi Jun 5 '18 at 22:28
  • $\begingroup$ @Kanpachi You did that correctly, and I showed the arithmetical equivalence of those formulations in my post $\endgroup$ – Bram28 Jun 6 '18 at 12:29

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.