A First Order Definition of the Mod Function

Question

Is there a good FOL definition of a $\bmod$ predicate in the language of Peano arithmetic? I tried $M(x,n,r) \equiv Ey(x=ny+r)$ but I don't like it very much.

Answer 1

We want to say that $r$ is the remainder when $x$ is divided by $n$. I will assume that variables range over the non-negative integers.

So we want to say that there exists a $q$ such that $x=nq+r$ and $r\lt n$. To say $r\lt n$, we need to say that $\lnot (r=n)$ and there is a $t$ such that $t+r=n$. Putting things together, we get $$\exists q\exists t((x=nq+r)\land \lnot(r=n)\land (t+r=n)).$$

Note that if we use this definition then we have decided that the predicate $M(x,n,r)$ will not hold if $n=0$. If we want to make another choice in the case $n=0$, suitable modification can be made.