Question about finding formulas in predicate calculus Let a language $L=\{+,<\}$. Let $M$ be the structure $(\mathbb{Z},+,<)$. Find a formula $\phi[x]$ with $x$ is the only free variable (thus you can use other symbols like $\forall y$, etc.) such that for any $a \in \mathbb{Z}$, $\phi[a]$ is satisfied in $M$ if and only if $a-1$ is divisible by $3$.
Attempt: What I think was that $a-1$ is divisible by $3$ if and only if  $a \equiv 1$. So I want to put something like divides then get the remainder $0<y<2$ but this doesn't work since we are not given division. That's all I can think of. Any hint would be appreciated. Thanks!
 A: For this kind of thing you have to spell out what multiplication by a constant like $3$ means in terms of addition:
$$\phi(a) \equiv \exists i(i + i + i + 1 = a)$$
You will often see something like this abbreviated as:
$$\phi(a) \equiv \exists i(3i + 1 = a)$$
where it is understood that multiplication by a constant is just an abbreviation for repeated addition: $3i = i + i + i$.
According to your comment, you are working over the signature that only has function symbols for $+$ and $<$ and no other non-logical symbols (I count = as a logical symbol). In this case, you need to introduce a local definition of the number 1 into $\phi$, which you can do as follows:
$$
\phi(a) \equiv \exists z \cdot\exists e \cdot \exists i\cdot (z + z = z \land z < e \land (\forall j\cdot\lnot(z < j \land j < e)) \land  3i + e = a)
$$
Here the formula $z + z = z$ acts as a definition of $z$ as $0$. Then $z < e$ and $\forall j\cdot\lnot(z < j \land j < e)$ act as a definition of $e$ as the smallest positive integer, i.e., $1$.
(Note that in this example, you don't even need to take = as a logical symbol.)
A: First note that you can pin down $0$ as being the unique $y \in \mathbb{Z}$ such that $x+y=x$ for all $x \in \mathbb{Z}$:
$$\mathtt{zero}(y) \equiv \forall x(x+y=x)$$
Then whenever you want to write $\psi(0)$, you instead write $\forall y(\mathtt{zero}(y) \to \psi(y))$, and so on.
We can also pin down $1$ as being the unique $y \in \mathbb{Z}$ such that $0<y$ and, for all $x \in \mathbb{Z}$, if $0 < x$ then $y \le x$. So let
$$\mathtt{one}(y) \equiv \forall z((\mathtt{zero}(z) \to z<y) \wedge \forall x (\forall z(\mathtt{zero}(z) \to z<x) \to w < x \vee w=x))$$
Finally, you can pin down the 'minus one' operation as follows: given $n \in \mathbb{Z}$, take the unique $y$ such that $y+1=n$. That is
$$\mathtt{minusone}(n;y) \equiv \forall z(\mathtt{one}(z) \to y+z=n)$$
So here's a sentence in all its gory describing what you want:
$$\forall y (\mathtt{minusone}(x;y) \to \exists z(y = (z+z)+z))$$
