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.

Improve this question
$\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$
    – Caleb Stanford
    Commented Dec 27, 2020 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$
    – Caleb Stanford
    Commented Dec 27, 2020 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$
    – Wei Zhan
    Commented Dec 27, 2020 at 8:37

2 Answers 2

Reset to default
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.

Improve this answer
$\endgroup$
6
  • 1
    $\begingroup$ Perfectly clear! Thank you for your answer. $\endgroup$
    – Caleb Stanford
    Commented Dec 27, 2020 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$
    – Caleb Stanford
    Commented Dec 27, 2020 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$
    – Emil Jeřábek
    Commented Dec 27, 2020 at 20:40
  • $\begingroup$ @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. $\endgroup$
    – Turbo
    Commented Dec 18, 2021 at 2:42
  • 2
    $\begingroup$ @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. $\endgroup$
    – Caleb Stanford
    Commented Jul 18 at 17:46
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.

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ Thank you for the interesting reference! $\endgroup$
    – Caleb Stanford
    Commented Dec 27, 2020 at 16:31
  • $\begingroup$ Yes, thank you for the reference. Is there other related material you can recommend? $\endgroup$
    – tale852150
    Commented Dec 28, 2020 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$
    – Bartosz Bednarczyk
    Commented Dec 28, 2020 at 8:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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