–
Room P4.35, Mathematics Building
Quantifier elimination revisited
It is well known that quantifier elimination can play a relevant role in proving decidability of theories. We present new compositional techniques for establishing quantifier elimination in a semantic way, capitalising on the fact that a 1-model-complete theory with algebraically prime models has quantifier elimination. We propose two ways of showing that a theory has algebraically models namely iteration and adjunction and we provide a guided way to prove that a theory is 1-model-complete. The applicability of these new conditions is illustrated on the theories of the natural numbers with successor, term algebras and algebraically closed fields. This talk is based on ongoing joint work with Cristina Sernadas.