<p>A something that might be too long for a comment, based on the previous answer by Emil.</p>
<p>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: <a href="https://www.cs.ox.ac.uk/people/james.worrell/LICS-main.pdf" rel="noreferrer">https://www.cs.ox.ac.uk/people/james.worrell/LICS-main.pdf</a>
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.</p>

CC BY-SA 4.0
2020-12-27T16:31:40.760Z
Thank you for the interesting reference!
Caleb Stanford
CC BY-SA 4.0
2020-12-28T00:21:43.803Z
Yes, thank you for the reference.  Is there other related material you can recommend?
tale852150
CC BY-SA 4.0
2020-12-28T08:53:02.750Z
Not really, the only other thing that I know and can be related is Presburger Arithmetics +  Modulo Counting, here: https://link.springer.com/chapter/10.1007%2F978-3-662-46678-0_24
Bartosz Bednarczyk
CC BY-SA 4.0
2020-12-27T11:37:25.367Z
2020-12-27T11:37:25.367Z
Bartosz Bednarczyk
<p>(<span class="math-container">$=$</span> is a logical symbol, hence I will not write it as part of the signature.) The satisfiability problem is decidable, as <span class="math-container">$\gcd$</span> has both a universal and an existential definition in terms of <span class="math-container">$|$</span>, <span class="math-container">$+$</span>, and <span class="math-container">$\le$</span>:
<span class="math-container">$$\begin{align*}
\gcd(a,b)=c&amp;\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)\\
&amp;\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*}$$</span>
Thus, any existential sentence over the structure <span class="math-container">$\langle\mathbb Z,+,\gcd\rangle$</span> (or even <span class="math-container">$\langle\mathbb Z,{\le},+,\gcd\rangle$</span>) can be (in polynomial time) converted to an equivalent existential sentence over the structure <span class="math-container">$\langle\mathbb Z,{\le},+,|\rangle$</span>, which can in turn be converted to an equivalent existential sentence over the structure <span class="math-container">$\langle\mathbb N,+,|\rangle$</span> in the obvious way. The last problem is decidable by the result of Lipshitz [1] quoted in the question.</p>
<p><strong>Reference:</strong></p>
<p>[1] Leonard Lipshitz: <em>The Diophantine problem for addition and divisibility</em>, Transactions of the American Mathematical Society 235 (1978), pp. 271–283, doi: <a href="https://doi.org/10.1090/S0002-9947-1978-0469886-1" rel="noreferrer">10.1090/S0002-9947-1978-0469886-1</a>.</p>

CC BY-SA 4.0
2020-12-27T16:30:50.730Z
Perfectly clear! Thank you for your answer.
Caleb Stanford
CC BY-SA 4.0
2020-12-27T20:07:33.770Z
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.
Caleb Stanford
CC BY-SA 4.0
2020-12-27T20:40:44.767Z
Indeed, this is an interesting connection. lcm has a universal definition similar to gcd, but apparently not an existential definition.
Emil Jeřábek
CC BY-SA 4.0
2021-12-18T02:42:53.313Z
@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.
Turbo
CC BY-SA 4.0
2024-07-18T17:46:39.740Z
@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.
Caleb Stanford
CC BY-SA 4.0
2024-08-10T20:36:21.190Z
Open = quantifier-free.
Emil Jeřábek
CC BY-SA 4.0
2020-12-27T08:42:28.253Z
2020-12-27T09:27:11.510Z
2020-12-27T09:27:11.510Z
Emil Jeřábek
<p>It is well-known that polynomial diophantine equations are undecidable (Hilbert's 10th problem): that is, given a quantifier-free formula over the language <span class="math-container">$\{=, +, \cdot, 1\}$</span> (of equality, addition, multiplication, and the constant <span class="math-container">$1$</span>), with free variables taking values in the integers, deciding whether the formula is satisfiable is undecidable.</p>
<p>If multiplication <span class="math-container">$\cdot$</span> is replaced by the binary greatest-common-divisor (gcd) function, defined appropriately for 0 and negative numbers, does the satisfiability problem remain undecidable?</p>
<hr />
<p>For example, the input might be a formula like
<span class="math-container">$$
a + b = c \land \gcd(a, b) = 2 \land \gcd(a, c) = 1
$$</span>
or
<span class="math-container">$$
\gcd(a, \gcd(b, c) + b) = a + c \land \lnot (\gcd(a, b) = a).
$$</span></p>
<p>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 <em>On Decidability Within the Arithmetic of Addition and Divisibility</em>, Marius Bozga and Radu Iosif) I know of the following classical results:</p>
<ul>
<li><p>The theory of <span class="math-container">$\{=, +, |\}$</span> (where <span class="math-container">$|$</span> is divisibility) <em>allowing quantifiers</em> is undecidable (Julia Robinson 1949).</p>
</li>
<li><p>The satisfiability of quantifier-free formulas over <span class="math-container">$\{=, +, |\}$</span> (i.e. existential fragment of the above) is decidable. (<em>The diophantine problem for addition and divisibility</em>, Leonard Lipshitz 1976.)</p>
</li>
</ul>
<p>Divisibility can be defined in terms of gcd (<span class="math-container">$a \mid b \iff \gcd(a, b) = a$</span>), but vice versa requires existential quantification (<span class="math-container">$\gcd(a, b) = c \iff (c \mid a) \land (c \mid b) \land \exists x \exists y.\; c = ax + by$</span>), 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.</p>

CC BY-SA 4.0
2020-12-27T05:59:45.397Z
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.
Caleb Stanford
CC BY-SA 4.0
2020-12-27T06:07:20.703Z
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).
Caleb Stanford
CC BY-SA 4.0
2020-12-27T08:37:22.623Z
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.
Wei Zhan
<lo.logic><nt.number-theory><decidability>
Decidability of diophantine equations over {=, +, gcd}
Caleb Stanford
# Decidability of diophantine equations over {=, +, gcd}

(Asked by: username_0 on 2020-12-26)

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.

**Tags:** lo.logic, nt.number-theory, decidability

> **Comments:**
> **username_0**: 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.  
> **username_0**: 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).  
> **username_1**: 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.  

---

## 2 answers

### Answer by username_4 on 2020-12-27. Score: 21 | Accepted answer

($=$ 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](https://doi.org/10.1090/S0002-9947-1978-0469886-1).

> **Comments:**
> **username_0**: Perfectly clear! Thank you for your answer.  
> **username_0**: 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.  
> **username_4**: Indeed, this is an interesting connection. lcm has a universal definition similar to gcd, but apparently not an existential definition.  
> **username_5**: @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.  
> **username_0**: @username_5 (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.  
> **username_4**: Open = quantifier-free.  

---

### Answer by username_2 on 2020-12-27. Score: 9

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.

> **Comments:**
> **username_0**: Thank you for the interesting reference!  
> **username_3**: Yes, thank you for the reference.  Is there other related material you can recommend?  
> **username_2**: Not really, the only other thing that I know and can be related is Presburger Arithmetics +  Modulo Counting, here: https://link.springer.com/chapter/10.1007%2F978-3-662-46678-0_24  

---

