3
$\begingroup$

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.

$\endgroup$

1 Answer 1

4
$\begingroup$

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

$\endgroup$
3
  • $\begingroup$ Hi, thanks for the answer! I am not so into this topic, so I do not understand the answer very well, sorry :( I mean, note that I do not know what Turing degrees are, but, in any case, your reference is talking about the ∀∃ (and ∃ and ∃∀∃) fragments, not ∃∀; or does ∀∃-decidability imply ∃∀ decidability? I will accept the answer as soon as I understand it!! $\endgroup$
    – Theo Deep
    Commented Jul 12, 2022 at 21:42
  • 1
    $\begingroup$ @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. $\endgroup$ Commented Jul 12, 2022 at 22:36
  • $\begingroup$ Then I can explore ∀∃-decidability results to apply them to ∃∀-decidability! Now, I have three sources to research: (1) the Bernays-Schonfinkel-Ramsey class, (2) the paper I cited in the post and (3) ∀∃-decidable theories. Am I right? Any other idea? Thanks a lot! $\endgroup$
    – Theo Deep
    Commented Jul 12, 2022 at 22:44

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .