Model Theory - Axiomatizability, Elimination of Quantifiers, and Model-completeness

Axiomatizability, Elimination of Quantifiers, and Model-completeness

The first step, often trivial, for applying the methods of model theory to a class of mathematical objects such as groups, or trees in the sense of graph theory, is to choose a signature σ and represent the objects as σ-structures. The next step is to show that the class is an elementary class, i.e. axiomatizable in first-order logic (i.e. there is a theory T such that a σ-structure is in the class if and only if it satisfies T). E.g. this step fails for the trees, since connectedness cannot be expressed in first-order logic. Axiomatizability ensures that model theory can speak about the right objects. Quantifier elimination can be seen as a condition which ensures that model theory does not say too much about the objects.

A theory T has quantifier elimination if every first-order formula φ(x₁,...,x_n) over its signature is equivalent modulo T to a first-order formula ψ(x₁,...,x_n) without quantifiers, i.e. holds in all models of T. For example the theory of algebraically closed fields in the signature σ_ring=(×,+,−,0,1) has quantifier elimination because every formula is equivalent to a Boolean combination of equations between polynomials.

A substructure of a σ-structure is a subset of its domain, closed under all functions in its signature σ, which is regarded as a σ-structure by restricting all functions and relations in σ to the subset. An embedding of a σ-structure into another σ-structure is a map f: A → B between the domains which can be written as an isomorphism of with a substructure of . Every embedding is an injective homomorphism, but the converse holds only if the signature contains no relation symbols.

If a theory does not have quantifier elimination, one can add additional symbols to its signature so that it does. Early model theory spent much effort on proving axiomatizability and quantifier elimination results for specific theories, especially in algebra. But often instead of quantifier elimination a weaker property suffices:

A theory T is called model-complete if every substructure of a model of T which is itself a model of T is an elementary substructure. There is a useful criterion for testing whether a substructure is an elementary substructure, called the Tarski–Vaught test. It follows from this criterion that a theory T is model-complete if and only if every first-order formula φ(x₁,...,x_n) over its signature is equivalent modulo T to an existential first-order formula, i.e. a formula of the following form:

,

where ψ is quantifier free. A theory that is not model-complete may or may not have a model completion, which is a related model-complete theory that is not, in general, an extension of the original theory. A more general notion is that of model companions.