I am reading the following paper, On the Combination of the Bernays–Schönfinkel–Ramsey Fragment with Simple Linear Integer Arithmetic: https://arxiv.org/pdf/1705.08792.pdf

In the introduction it states the following: The Bernays-Schönfinkel-Ramsey (BSR) fragment comprises exactly the first-order logic prenex sentences with the $\exists^*\forall^*$ quantifier prefix, resulting in a CNF where all occurring function symbols are constants. Formulas may contain equality. Satisfiability of the BSR fragment is decidable and NExpTime-complete. Its extension with linear arithmetic is undecidable.

However, as far as I knew:

  1. From (https://en.wikipedia.org/wiki/Bernays%E2%80%93Sch%C3%B6nfinkel_class): BSR It is the set of sentences that, when written in prenex normal form, have an $\exists^*\forall^*$ quantifier prefix and do not contain any function symbols.
  2. Linear integer arithmetic (LIA) and linear real arithmetic (LRA) are both decidable. Thus, the whole first-order theory of linear arithmetics is decidable.

So I am not understanding something: in my opinion, BSR modulo LIA/LRA should be decidable.

My reasoning is that, since LIA/LRA is decidable (i.e., not matters the quantifier alternation, it is decidable), then the LIA/LRA restricted to BSR fragment (equivalently, BSR modulo LIA/LRA) should be decidable. I mean, decidability implies $\exists^*\forall^*$-decidability, am I right?

I am sure I am the one that is missing something, so can anyone help me out?

  • $\begingroup$ I think the reason is that the extension of BSR with linear arithmetic allows predicates that are not contained in the signature of LIA/LRA (see, e.g., Example 6 in the paper that you've mentioned, which uses the additional predicates T, Q, and R). For this reason, decidability of LIA/LRA does not imply decidability of BSR + LIA/LRA. $\endgroup$
    – ffrohn
    Commented Jul 6, 2023 at 9:57


You must log in to answer this question.