Quantifier elimination via adjunction
João Rasga, Cristina Sernadas · 2010
Sufficient conditions are provided for quantifier elimination to hold in a first-order theory. The conditions have two main purposes: (1) to ensure that satisfaction of existential formulas is reflected by an embedding; and (2) to guarantee the existence of a “minimal " model of the theory extending a model of the universal formulas entailed by the theory. The first goal is obtained by requiring that a theory is ∃-adequate and the second by imposing the existence of an adjunction. Recognizing that, in some cases, a “minimal " model extending another can be obtained by iterating a construction, we also provide conditions that guarantee the existence of a ω-“limit " functor identifying such an extension, when the theories are in ∀2. Examples are provided along the paper.