Quantifier elimination

A theory has quantifier elimination when every formula is equivalent modulo the theory to a quantifier-free formula.

For a binary relation with no symmetry or loop restrictions, an extension axiom demands a fresh element realizing any prescribed choices of incoming edges, outgoing edges and its own loop relative to a finite list of distinct parameters. All such axioms together eliminate quantifiers: the quantifier-free type of a parameter tuple determines which witness patterns can occur. These axioms differ from the undirected loop-free theory of the random graph.

A theory $T$ eliminates quantifiers if, whenever two models of $T$ contain isomorphic copies of the same substructure $A$, they satisfy the same formulas over $A$. Equivalently, $T\cup D(A)$ is complete for every substructure of a model of $T$.

For a first-order theory $T$, suppose every existential quantifier-free formula over a common substructure has a witness in either of two $T$-models exactly when it has one in the other. Then $T$ has quantifier elimination. One may test a single quantified variable, since elimination of these formulas inductively eliminates all quantifiers. A language with a constant avoids empty-generated-substructure and quantifier-free-sentence conventions.

If $T$ has algebraically prime models and every inclusion between models of $T$ is a simple closure, then $T$ has quantifier elimination. For a common base $A$, embed its algebraically prime extension into both models. Simple closure transfers a witness into that extension; the second embedding transfers it to the other model.

A partial embedding is an injective map between subsets of structures that preserves and reflects atomic formulas. It therefore preserves every quantifier-free formula.

The theory of algebraically closed fields of a fixed characteristic eliminates quantifiers in the language of rings. Over a parameter field $F$, the complete type of a tuple is determined by the prime ideal of polynomial relations it satisfies.

Complete $n$-types over a subfield $F$ of an algebraically closed field correspond to prime ideals of $F[X_1,\dots ,X_n]$, or equivalently to generic points of irreducible affine varieties over $F$. The Stone topology corresponds to the constructible topology: polynomial equalities and inequalities define basic clopen sets.

The theory of the random graph says that the edge relation is irreflexive and symmetric and that, for every two finite disjoint vertex sets, a new vertex is adjacent to every vertex of the first and none of the second.

Every small partial embedding of a monster random graph extends by back-and-forth to an automorphism, using saturation and the extension axioms. It is therefore elementary, and the theory of the random graph eliminates quantifiers.

For every small set $A$ in a monster random graph,Any vertex outside $A$ has infinitely many conjugates over $A$ with the same adjacency pattern.

The three-types of the random graph are determined by equality and adjacency among three variables. There is one all-equal type, six types with exactly two variables equal, and eight types with all variables distinct, for a total of fifteen.

The back-and-forth method constructs an isomorphism by alternately extending finite partial isomorphisms to include elements from each structure.

An effective back-and-forth construction alternately extends a finite partial isomorphism of structures to include the least unused domain and range elements, searching computably for a compatible extension. If extension always exists and its finite compatibility conditions are decidable, the union is a computable isomorphism. Decidable presentations of a dense linear order without endpoints provide a basic example.

A dense linear order without endpoints is a linear order in which a third point lies strictly between every two distinct points and every point has points both below and above it.

Add constants $c_0<c_1<\cdots$ to the theory of dense linear orders without endpoints. The three countable models have respectively a least upper bound for the named sequence, no upper bound, or upper bounds with no least one. The unbounded model is an atomic model; the bounded model with no least upper bound is an omega-saturated model. The remaining model omits the type $c_i<x<d$ over its least-upper-bound parameter $d$.

A complete dense linear order without endpoints with the countable chain condition for a linear order, but with no countable order-dense subset.

The assertion that there is no Suslin line, equivalently that every complete dense linear order without endpoints satisfying the interval countable chain condition is separable. A Suslin tree gives a counterexample.

The theory of dense linear orders without endpoints eliminates quantifiers. A finite partial order isomorphism extends by placing each new point in the corresponding interval or ray.