Boundary between decidability and undecidability for small theories 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)$
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!