A roadmap to decidability

João Rasga

Cristina Sernadas

Amílcar Sernadas

pp. 423-445

in: Arnold Koslow, Arthur Buchsbaum (eds), The road to universal logic I, Basel, Birkhäuser, 2015

Abstract

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.