21
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ 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. $\endgroup$
    – 6005
    Dec 27 '20 at 5:59
  • $\begingroup$ 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). $\endgroup$
    – 6005
    Dec 27 '20 at 6:07
  • 3
    $\begingroup$ 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. $\endgroup$ Dec 27 '20 at 8:37
21
$\begingroup$

($=$ 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.

$\endgroup$
3
  • 1
    $\begingroup$ Perfectly clear! Thank you for your answer. $\endgroup$
    – 6005
    Dec 27 '20 at 16:30
  • 4
    $\begingroup$ 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. $\endgroup$
    – 6005
    Dec 27 '20 at 20:07
  • 2
    $\begingroup$ Indeed, this is an interesting connection. lcm has a universal definition similar to gcd, but apparently not an existential definition. $\endgroup$ Dec 27 '20 at 20:40
9
$\begingroup$

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.

$\endgroup$
3
  • 1
    $\begingroup$ Thank you for the interesting reference! $\endgroup$
    – 6005
    Dec 27 '20 at 16:31
  • $\begingroup$ Yes, thank you for the reference. Is there other related material you can recommend? $\endgroup$
    – tale852150
    Dec 28 '20 at 0:21
  • $\begingroup$ 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 $\endgroup$ Dec 28 '20 at 8:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.