I am reading a paper and there is the following theorem:

Let $n$ be a fixed integer, and $n >1$.

Denote divisibility in $\mathbb{Z}[\frac{1}{n}]$ by $|_n$, thus for all $x, y \in \mathbb{Z}$ $$x |_n y \leftrightarrow \exists q, f \in \mathbb{Z}: y=xqn^{-f}$$ Then the positive existential theory of $(\mathbb{Z}; +, |_n)$ is undecidable, i.e. there is no algorithm to decide formulas of the form $$\exists x_1, \dots , x_m \in \mathbb{Z}: \land_{i=1}^s F_i (x_1, \dots , x_m) |_n G_i (x_1, \dots , x_m), $$ where $F_i$ and $G_i$ are polynomials over $\mathbb{Z}$ of degree one or less, and where $\land_{i=1}^s$ denotes a finite conjunction.

Why does the positive existential theory of $(\mathbb{Z}; +, |_n)$ contain formulas of the form $\exists x_1, \dots , x_m \in \mathbb{Z}: \land_{i=1}^s F_i (x_1, \dots , x_m) |_n G_i (x_1, \dots , x_m), $ ?

This formula does not contain $+$. Do we suppose that the polynomials $F_i$ and $G_i$ contain additions?

Also why are these polynomials of degree one or less?

definitionof the positive existential theory in this case? $\endgroup$ – Emil Jeřábek Sep 3 '15 at 8:36