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

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.

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).
• @TheoDeep Yes, $\exists\forall$-decidability is equivalent to $\forall\exists$-decidability: to tell if $\exists x\forall y\varphi$ is true, just ask whether $\forall x\exists y\neg\varphi$ is false. Commented Jul 12, 2022 at 22:36