<p>Let $V_k (n)$ be the function that maps $n$ to the largest power of $k$ dividing $n$.  (<em>Not</em> the <em>exponent</em> of the largest power; the largest power itself.)  It follows from the work of Büchi (as corrected by, e.g., Hodgson) that the first-order theory Th($N, +, V_k$) for fixed integer $k \geq 2$ is decidable.  But Villemaire showed (￼Theoretical Computer Science 106 (1992), 337-349) that Th($N, +, V_k, V_l$) is undecidable if $k, l$ are multiplicatively independent.  So this is a nice boundary between decidable and undecidable.  </p>

<p>The survey paper of Bès (available here:  <a href="http://lacl.univ-paris12.fr/bes/publi/survey.ps">http://lacl.univ-paris12.fr/bes/publi/survey.ps</a> ) makes good reading!</p>

CC BY-SA 3.0
2016-08-05T14:47:51.243Z
2016-08-05T14:47:51.243Z
Jeffrey Shallit
<p>One possible avenue for this question is to find problems with <em>difficult undecidability proofs</em> (see also <a href="https://cstheory.stackexchange.com/questions/18846/a-simple-problem-whose-decidability-is-not-known">this question</a>), as they are usually close to a boundary with an undecidable problem.</p>

<p>Some examples that come to mind are:</p>

<ul>
<li><p>Higher-order unification/matching of typed $\lambda$-terms: Unification is undecidable at order 3 by results of Huet. Matching modulo $\beta$ is undecidable as well for some high order, but matching modulo $\beta\eta$ is believed to be decidable, though the proof is quite complex, and I'm not sure if it is universally accepted. Certainly the problem is resolved for orders up to 5.</p></li>
<li><p>Subtype entailment (problem #16 of <a href="http://tlca.di.unito.it/opltlca/" rel="nofollow noreferrer">this list</a>) is a problem that relates to typing in the presence of subtyping with function types, but is a rather simple problem (to state!) in first-order logic. Decidability is not known.</p></li>
<li><p>A lot of work explores the limit between decidability and undecidability for extensions of presburger arithmetic. See <a href="http://www.sciencedirect.com/science/article/pii/S0304397500001134" rel="nofollow noreferrer">this overview</a> for example.</p></li>
<li><p>A fun example is the following, from rewriting theory (<a href="http://link.springer.com/chapter/10.1007%2F11532231_10" rel="nofollow noreferrer">Zhang &amp; al</a>):</p>

<ol>
<li>The first order theory of terms with <em>Knuth-Bendix ordering</em> is decidable</li>
<li>The first order theory of terms with <a href="https://en.wikipedia.org/wiki/Path_ordering_(term_rewriting)" rel="nofollow noreferrer"><em>lexicographic path ordering</em></a> is undecidable</li>
</ol></li>
</ul>

<p>All these problems feel "computer sciency" but I'd argue that they are all logic problems (unification is decidability of an existential statements in a theory of equality).</p>

CC BY-SA 3.0
2016-08-05T15:09:25.027Z
2016-08-05T15:09:25.027Z
2017-04-13T12:32:28.167Z
cody
<p>There is a lot of research on the boundary between decidability and undecidability of the halting problem for small models of computation: Turing machines, tag systems, CAs, ... This boundary is clearly linked to the (non-)universality of such models.</p>

<p>I'm wondering if there are similar works on the "logic-side":</p>

<blockquote>
  <p>What are the <em>smallest</em> theories for which the boundary between  decidability and undecidability (of valid formulas) is unknown ?
  Is there a survey paper on the subject ?</p>
</blockquote>

<p>I realize that it is not easy to formalize the notion of "small theory" (or "simple" theory), but it should include the number of axioms of the theory and the size of the signature.</p>

<p>For example Andrzej Grzegorczyk in “Undecidability without arithmetization” (Studia Logica 79(2005))
proved that Tarski’s theory of concatenation (TC) <em>is already undecidable</em>; the axioms are:</p>

<p>TC1: $x*(y*z) = (x*y)*z$<br>
TC2: $(x*y = u*v ) \to \exists w((x*w = u \land w*v = y)\lor(u*w = x \land w*y = v))$<br>
TC3: $\neg (\alpha = x*y)$<br>
TC4: $\neg (\beta = x*y)$<br>
TC5: $\neg (\alpha = \beta)$</p>

CC BY-SA 3.0
2016-08-05T15:48:48.147Z
The question seems to aim backwards. In the realm of logical theories, *removing* axioms makes theories *harder* to decide, not easier. In particular, pure predicate logic with no non-logical axioms in a language with one binary relation symbol is undecidable.
Emil Jeřábek
<reference-request><lo.logic>
Boundary between decidability and undecidability for small theories
Marzio De Biasi
# Boundary between decidability and undecidability for small theories

(Asked by: username_0 on 2016-08-05)

There is a lot of research on the boundary between decidability and undecidability of the halting problem for small models of computation: Turing machines, tag systems, CAs, ... This boundary is clearly linked to the (non-)universality of such models.

I'm wondering if there are similar works on the "logic-side":

> What are the *smallest* theories for which the boundary between decidability and undecidability (of valid formulas) is unknown ?
> Is there a survey paper on the subject ?

I realize that it is not easy to formalize the notion of "small theory" (or "simple" theory), but it should include the number of axioms of the theory and the size of the signature.

For example Andrzej Grzegorczyk in “Undecidability without arithmetization” (Studia Logica 79(2005))
proved that Tarski’s theory of concatenation (TC) *is already undecidable*; the axioms are:

TC1: $x\*(y\*z) = (x\*y)\*z$  
TC2: $(x\*y = u\*v ) \to \exists w((x\*w = u \land w\*v = y)\lor(u\*w = x \land w\*y = v))$  
TC3: $\neg (\alpha = x\*y)$  
TC4: $\neg (\beta = x\*y)$  
TC5: $\neg (\alpha = \beta)$

**Tags:** reference-request, lo.logic
> **Comments:**
> **username_1**: The question seems to aim backwards. In the realm of logical theories, *removing* axioms makes theories *harder* to decide, not easier. In particular, pure predicate logic with no non-logical axioms in a language with one binary relation symbol is undecidable.  

---

## 2 answers

### Answer by username_2 on 2016-08-05. Score: 9

Let $V\_k (n)$ be the function that maps $n$ to the largest power of $k$ dividing $n$. (*Not* the *exponent* of the largest power; the largest power itself.) It follows from the work of Büchi (as corrected by, e.g., Hodgson) that the first-order theory Th($N, +, V\_k$) for fixed integer $k \geq 2$ is decidable. But Villemaire showed (￼Theoretical Computer Science 106 (1992), 337-349) that Th($N, +, V\_k, V\_l$) is undecidable if $k, l$ are multiplicatively independent. So this is a nice boundary between decidable and undecidable.

The survey paper of Bès (available here: <http://lacl.univ-paris12.fr/bes/publi/survey.ps> ) makes good reading!


---

### Answer by username_3 on 2016-08-05. Score: 4

One possible avenue for this question is to find problems with *difficult undecidability proofs* (see also [this question](https://cstheory.stackexchange.com/questions/18846/a-simple-problem-whose-decidability-is-not-known)), as they are usually close to a boundary with an undecidable problem.

Some examples that come to mind are:

* Higher-order unification/matching of typed $\lambda$-terms: Unification is undecidable at order 3 by results of Huet. Matching modulo $\beta$ is undecidable as well for some high order, but matching modulo $\beta\eta$ is believed to be decidable, though the proof is quite complex, and I'm not sure if it is universally accepted. Certainly the problem is resolved for orders up to 5.
* Subtype entailment (problem #16 of [this list](http://tlca.di.unito.it/opltlca/)) is a problem that relates to typing in the presence of subtyping with function types, but is a rather simple problem (to state!) in first-order logic. Decidability is not known.
* A lot of work explores the limit between decidability and undecidability for extensions of presburger arithmetic. See [this overview](http://www.sciencedirect.com/science/article/pii/S0304397500001134) for example.
* A fun example is the following, from rewriting theory ([Zhang & al](http://link.springer.com/chapter/10.1007%2F11532231_10)):

  1. The first order theory of terms with *Knuth-Bendix ordering* is decidable
  2. The first order theory of terms with [*lexicographic path ordering*](https://en.wikipedia.org/wiki/Path_ordering_(term_rewriting)) is undecidable

All these problems feel "computer sciency" but I'd argue that they are all logic problems (unification is decidability of an existential statements in a theory of equality).


---

