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

Rafael Grimson,

Bart Kuijpers

Abstrakt

We consider the 10-fragment of second-order logic over the vocabulary h+;; 0; 1; <; S1; :::; Ski, interpreted over the reals, where the predicate symbols Si are interpreted as semialgebraic sets. We show that, in this context, satis ability of formulas is decidable for the rst-order 9-quanti er fragment and undecidable for the 98- and 8-fragments. We also show that for these three fragments the same (un)decidability results hold for containment and equivalence of formulas.

References

[1] J. Bochnak, M. Coste, M.-F. Roy, Real Algebraic Geometry, Volume 36 of Ergebenisse der Mathematik und ihrer Grenzgebiete, Folge 3, Springer-Verlag, Berlin, 1998.

[2] G. Jeronimo and J. Sabia, On the number of sets definable by polynomials, Journal Algebra 227:2 (2000), 633–644.

[3] E. B¨orger, E. Gr¨adel and Y. Gurevich, The Classical Decision Problem, Monographs in Mathematical Logic, Springer-Verlag, 2000.

[4] D. Grigoriev and N. N. (jr.) Vorobjov, Solving systems of polynomial inequalities in subexponential time, Journal of Symbolic Computation 5 (1988), 37–64.

[5] J. P. Jones and Y. V. Matijasevich, Exponential Diophantine representation of recursively enumerable sets, In J. Stern, editor, Proceedings of the Herbrand Sym- posium: Logic Colloquium ’81, volume 107of Studies in Logic and the Foundations of Mathematics, Amsterdam. North Holland, 1982, pp.159–177.

[6] Y. V. Matijasevich, Hilbert’s Tenth Problem, MIT Press, Cambridge, MA, 1993.

[7] J. Paredaens, G. Kuper and L. Libkin, editors, Constraint databases, Springer- Verlag, 2000.

[8] A. Tarski, A Decision Method for Elementary Algebra and Geometry, University of California Press, 1951.

Czasopismo ukazuje się w sposób ciągły on-line.
Pierwotną formą czasopisma jest wersja elektroniczna.