Examples of Exists-Forall-decidable first-order theories that are not overall decidable

decidabilityfirst-order-logiclogicpredicate-logicquantifiers

I am looking for first-order theories that are decidable on its $\exists^*\forall^*$ fragment, but I am really struggling with it.

I mean, I know there are lots of theories that are (overall) decidable; and thus, $\exists^*\forall^*$ decidable: say (from Wikipedia: ):

  • The set of first-order logical validities in the signature with only equality.
  • The set of first-order logical validities in a signature with equality and one unary function.
  • The first-order theory of the natural numbers in the signature with equality and addition (a.k.a. Presburger arithmetic).

However, I am interested in those theories that are not overall decidable, but only $\exists^*\forall^*$ decidable (or more decidable, but not overall decidable: say, $\forall\exists^*\forall^*$ decidable, $\exists^*\forall\exists^*\forall^*$ decidable etc.)

Could anyone provide some example of theories like these? Also, does anyone know any survey on this topic? The closest one I have found is (https://link.springer.com/article/10.1007/s10817-020-09567-8), which explores decidable $\exists^*\forall^*$ fragments of linear rational arithmetic modulo uninterpreted predicates.

Moreover, I am particularly interested on those theories that are not arithmetic. For instance, in (https://arxiv.org/abs/1610.04707), they address the fragment of first-order separation logic (SL) restricted to the Bernays-Schonfinkel-Ramsey class (i.e., $\exists^*\forall^*$ with no function symbols), where the quantified variables range over the set of memory locations. This is decidable. However, SL becomes undecidable when the quantifier prefix belongs to $\exists^*\forall^*\exists^*$ instead. A similar phenomenon occurs with the theory of arrays.

Best Answer

There are a number of examples coming from computability theory, specifically the various "degree structures." For example, the two-quantifier theory of the Turing degrees (as a partial order) is decidable, but the three-quantifier theory of the Turing degrees is undecidable. Interestingly, the same combinatorial fact - that every countable lattice is isomorphic to an initial segment of the Turing degrees (due to Lerman) - is used in both of these facts. See the introduction and bibliography of Shore/Slaman, The $\forall\exists$ theory of $\mathcal{D}(\le,\vee,')$ is undecidable (and note that, per the title, the precise structure we put on the degrees matters a ton in terms of exactly where we switch from decidability to undecidability).

Related Question