SOME FRAGMENTS OF SECOND-ORDER LOGIC OVER THE REALS FOR WHICH SATISFIABILITY AND EQUIVALENCE ARE (UN)DECIDABLE
SOME FRAGMENTS OF SECOND-ORDER LOGIC OVER THE REALS FOR WHICH SATISFIABILITY AND EQUIVALENCE ARE (UN)DECIDABLE

Summary/Abstract: We consider the fragment of second-order logic over the vocabulary <+; x; 0; 1; <; S1; ...; Sk>, interpreted over the reals, where the predicate symbols Si are interpreted as semi-algebraic sets. We show that, in this context, satisfiability of formulas is decidable for the first-order 9-quantifier fragment andundecidable for 8-fragments. We also show that forthese three fragments the same (un)decidability results hold forcontainment and equivalence of formulas..

• Details
• Contents