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.
CITATION STYLE
Rasga, J., Sernadas, C., & Sernadas, A. (2015). A Roadmap to Decidability. In Studies in Universal Logic (pp. 423–445). Springer Nature. https://doi.org/10.1007/978-3-319-10193-4_20
Mendeley helps you to discover research relevant for your work.