# Decidability of diophantine equations over {=, +, gcd}

It is well-known that polynomial diophantine equations are undecidable (Hilbert's 10th problem): that is, given a quantifier-free formula over the language $$\{=, +, \cdot, 1\}$$ (of equality, addition, multiplication, and the constant $$1$$), with free variables taking values in the integers, deciding whether the formula is satisfiable is undecidable.

If multiplication $$\cdot$$ is replaced by the binary greatest-common-divisor (gcd) function, defined appropriately for 0 and negative numbers, does the satisfiability problem remain undecidable?

For example, the input might be a formula like $$a + b = c \land \gcd(a, b) = 2 \land \gcd(a, c) = 1$$ or $$\gcd(a, \gcd(b, c) + b) = a + c \land \lnot (\gcd(a, b) = a).$$

I suspect this to be a basic result in the study of decidability results for integer theories, but this came up in another context and I am not entirely familiar. From a brief literature search (see On Decidability Within the Arithmetic of Addition and Divisibility, Marius Bozga and Radu Iosif) I know of the following classical results:

• The theory of $$\{=, +, |\}$$ (where $$|$$ is divisibility) allowing quantifiers is undecidable (Julia Robinson 1949).

• The satisfiability of quantifier-free formulas over $$\{=, +, |\}$$ (i.e. existential fragment of the above) is decidable. (The diophantine problem for addition and divisibility, Leonard Lipshitz 1976.)

Divisibility can be defined in terms of gcd ($$a \mid b \iff \gcd(a, b) = a$$), but vice versa requires existential quantification ($$\gcd(a, b) = c \iff (c \mid a) \land (c \mid b) \land \exists x \exists y.\; c = ax + by$$), which won't work in quantifier-free formulas in a negated context, so at least at first glance I am not sure that gcd is equivalent to divisibility for the purposes of decidability.

• It came up in another context -- decidability of fragments of regular expressions can be studied by starting from regular expressions over a unary alphabet, and looking at the subsets of integer constraints that can be encoded. One such fragment gave rise to roughly this theory. Commented Dec 27, 2020 at 5:59
• Thanks! As to the original problem I am afraid I can't be more precise, I hadn't formulated everything myself clearly. There are different fragments corresponding to different integer theories and the correspondence is not so direct (for instance, for the original fragment of unary alphabet REs I was thinking of, I believe more can be expressed than just $\gcd$. But per your comments, remains undecidable). Commented Dec 27, 2020 at 6:07
• Isn't $\mathrm{gcd}(a,b)\neq c$ the same as $(c\nmid a)\vee(c\nmid b)\vee(\exists d. (c|d)\wedge(c\neq \pm d)\wedge(d|a)\wedge(d|b))$? So it reduced to quantifier-free divisibility formulas no matter negated or not. Commented Dec 27, 2020 at 8:37

($$=$$ is a logical symbol, hence I will not write it as part of the signature.) The satisfiability problem is decidable, as $$\gcd$$ has both a universal and an existential definition in terms of $$|$$, $$+$$, and $$\le$$: \begin{align*} \gcd(a,b)=c&\iff c\ge0\land c\mid a\land c\mid b\land\forall d\:(d\mid a\land d\mid b\to d\mid c)\\ &\iff c\ge0\land c\mid a\land c\mid b\land\exists u,v\:(a\mid u\land b\mid v\land c=u+v). \end{align*} Thus, any existential sentence over the structure $$\langle\mathbb Z,+,\gcd\rangle$$ (or even $$\langle\mathbb Z,{\le},+,\gcd\rangle$$) can be (in polynomial time) converted to an equivalent existential sentence over the structure $$\langle\mathbb Z,{\le},+,|\rangle$$, which can in turn be converted to an equivalent existential sentence over the structure $$\langle\mathbb N,+,|\rangle$$ in the obvious way. The last problem is decidable by the result of Lipshitz [1] quoted in the question.

Reference:

[1] Leonard Lipshitz: The Diophantine problem for addition and divisibility, Transactions of the American Mathematical Society 235 (1978), pp. 271–283, doi: 10.1090/S0002-9947-1978-0469886-1.

• Perfectly clear! Thank you for your answer. Commented Dec 27, 2020 at 16:30
• This is all the more interesting because it would appear that using least common multiple (lcm) instead of gcd becomes undecidable. lcm can be used to encode squares via the trick $x^2 - 1 = \text{lcm}(x + 1, x - 1)$ (assuming $x$ even, with a similar constraint for $x$ odd), then squares can be used to encode multiplication. Commented Dec 27, 2020 at 20:07
• Indeed, this is an interesting connection. lcm has a universal definition similar to gcd, but apparently not an existential definition. Commented Dec 27, 2020 at 20:40
• @EmilJeřábek The paper quoted also states multiplication can be defined from $+,|$. So is any existential sentence over $\langle\mathbb Z,+,\times\rangle$ decidable? The paper states $\exists x_1,\dots,x_n\forall y\Delta(x_1,\dots,x_n,y)$ might be undecidable if $\Delta$ is an open formula. I do not know what an open formula means. Commented Dec 18, 2021 at 2:42
• @Turbo (late reply) "is any existential sentence over ⟨ℤ,+,×⟩ decidable?" Certainly not as that is Hilbert's 10th problem. I didn't take another look at the paper but probably the definition of multiplication uses quantifiers. Commented Jul 18 at 17:46

A something that might be too long for a comment, based on the previous answer by Emil.

In the case you are interested in the complexity of such a logic, consider reading LICS'2015 paper by Joël Ouaknine, Antonia Lechner and Ben Worrell. A preprint is available here: https://www.cs.ox.ac.uk/people/james.worrell/LICS-main.pdf According to the authors, the proof by Lipshitz is of considerable mathematical depth and intricacy and is difficult to read and understand. So I hope that the attached paper will be more useful in this context.

• Thank you for the interesting reference! Commented Dec 27, 2020 at 16:31
• Yes, thank you for the reference. Is there other related material you can recommend? Commented Dec 28, 2020 at 0:21
• Not really, the only other thing that I know and can be related is Presburger Arithmetics + Modulo Counting, here: link.springer.com/chapter/10.1007%2F978-3-662-46678-0_24 Commented Dec 28, 2020 at 8:53