Some Fragments of Second-Order Logic Over the Reals for Which Satisfiability and Equivalence Are (Un)Decidable

Rafael Grimson; Bart  Kuijpers

Some Fragments of Second-Order Logic Over the Reals for Which Satisfiability and Equivalence Are (Un)Decidable

Publication date: 21.10.2014

Reports on Mathematical Logic, 2014, Number 49, pp. 23-34

https://doi.org/10.4467/20842589RM.14.002.2272

Authors

Download full text

PDF

Titles

Some Fragments of Second-Order Logic Over the Reals for Which Satisfiability and Equivalence Are (Un)Decidable

Abstract

We consider the Σ1-fragment of second-order logic over the vocabulary (+, ×, 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 ∃∗-quantifier fragment and undecidable for the ∃∗∀- and ∀∗-fragments. We also show that for these three fragments the same (un)decidability results hold for containment and equivalence of formulas.

References

Download references

[1] J. Bochnak, M. Coste, M.-F. Roy, Real Algebraic Geometry, Volume 36 of Ergebenisse der Mathematik und ihrerGrenzgebiete, 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 ofSymbolic 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 Symposium: Logic Colloquium ’81, volume 107of Studies in Logic and the Foundationsof 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.

Information

Information: Reports on Mathematical Logic, 2014, Number 49, pp. 23-34

DOI: https://doi.org/10.4467/20842589RM.14.002.2272

Article type: Original article

Authors

Rafael Grimson

CONICET and Escuela de Ciencia y Tecnologica, Universidad de San Marteen, Campus Miguelete (CP1650). San Martn, Provincia de Buenos Aires, Argentina

Bart Kuijpers

Databases and Theoretical Computer Science Group, Hasselt University, Agoralaan, Gebouw D, 3590 Diepenbeek, Belgium

Published at: 21.10.2014

Article status: Open

Licence: None

Percentage share of authors:

Rafael Grimson (Author) - 50%

Bart Kuijpers (Author) - 50%

Article corrections:

Publication languages:

English

View count: 2138

Number of downloads: 1325

Some Fragments of Second-Order Logic Over the Reals for Which Satisfiability and Equivalence Are (Un)Decidable

Download xml