A Roadmap to Decidability

It is well known that quantifier elimination plays a relevant role in proving decidability of theories. Herein the objective is to provide a tool-box that makes easier to establish quantifier elimination in a semantic way, capitalizing on the fact that a 1-model-complete theory with alge-braically prime models has quantifier elimination. Iteration and adjunc-tion 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. Keywords quantifier elimination, decidability of theories