Definability in FO($\mathbb{Q}, +, \leq$)

Question

Is the set $\left\{(x, y) \in \mathbb{Q}_{>0}^2 \, : \, \frac{x}{y} \in 2\mathbb{N} - 1\right\}$ definable in FO($\mathbb{Q}, +, \leq$).

Answer 1

I suspect not; the condition appears to be an infinite disjunction of $\phi_n(x,y): \underbrace{y + \cdots + y}_{2n-1 \text{ copies of } y} = x$.

Since any automorphism of $\mathrm{FO}(\Bbb Q, +, \le)$ must be $\Bbb Q$-linear (by its preservation of an adapted form of $\phi_n$, taking sums of $x$s as well), these are only $x \mapsto \lambda x$ with $\lambda \in \Bbb Q$, and your relation is preserved under automorphisms; thus, it isn't contradicted that it be definable by this method.

Maybe somebody else can come up with more sophisticated non-definability criteria.

Answer 2

Hint: the theory of ordered divisible Abelian groups admits quantifier elimination in the language $\{+, <, 0\}$.