Repository | Book | Chapter

202757

(2015) The road to universal logic I, Basel, Birkhäuser.

A roadmap to decidability

João Rasga, Cristina Sernadas, Amílcar Sernadas

pp. 423-445

It is well known that quantifier elimination plays a relevant role in proving decidability of theories. Herein the objective is to provide a toolbox that makes it easier to establish quantifier elimination in a semantic way, capitalizing on the fact that a 1-model-complete theory with algebraically prime models has quantifier elimination. Iteration and adjunction are identified as important constructions that can be very helpful, by themselves or composed, in proving that a theory has algebraically prime models. Some guidelines are also discussed towards showing that a theory is 1-model-complete. Illustrations are provided for the theories of the natural numbers with successor, term algebras (having stacks as a particular case) and algebraically closed fields.

Publication details

DOI: 10.1007/978-3-319-10193-4_20

Full citation:

Rasga, J. , Sernadas, C. , Sernadas, A. (2015)., A roadmap to decidability, in A. Koslow & A. Buchsbaum (eds.), The road to universal logic I, Basel, Birkhäuser, pp. 423-445.

This document is unfortunately not available for download at the moment.