Boundary between decidability and undecidability for small theories

Question

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)$

Answer 1

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 2

One possible avenue for this question is to find problems with difficult undecidability proofs (see also this question), 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) 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 for example.

• A fun example is the following, from rewriting theory (Zhang & al):

  1. The first order theory of terms with Knuth-Bendix ordering is decidable
  2. The first order theory of terms with lexicographic path ordering 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).