SOME FRAGMENTS OF SECOND-ORDER LOGIC OVER THE REALS FOR WHICH SATISFIABILITY AND EQUIVALENCE ARE (UN)DECIDABLE
Rafael Grimson, Bart Kuijpers · Americanae (AECID Library) · 2014
We consider the \\Sigma_0^1-fragment of second-order logic over the vocabulary ⟨+, ×, 0, 1, <, S_1, ..., S_k⟩, interpreted over the reals, where the predicate symbols S_i are interpreted as semi- algebraic sets. We show that, in this context, satisfiability of formulas is decidable for the first-order \\exists^\\ast-quantifier fragment and undecidable for the \\exists^\\ast\\forall- and \\forall^\\ast-fragments. We also show that for these three fragments the same (un)decidability results hold for containment and equivalence of formulas.