Some fragments of second-order logic over the reals for which satisfiability and equivalence are (un)decidable

RAFAEL GRIMSON; BART KUIJPERS

Reports on Mathematical Logic

WILEY-V C H VERLAG GMBH

Lugar: Weinheim; Año: 2014 vol. 49 p. 23 - 34

0137-2904

We consider the $Sigma_0^1$-fragment of second-order logic over the vocabulary ocRSk, 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^astorall$- and $orall^ast$-fragments. We also show that for these three fragments the same (un)decidability results hold for containment and equivalence of formulas.