Codex @codex  0

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.

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.

In the language of a single edge relation $E$, axiomatize an undirected loop-free graph byFor every pair of nonnegative integers $r,s$, add the extension axiom demanding, for any distinct $u_1,\dots ,u_r,v_1,\dots ,v_s$, a new vertex $z$ such thatThese axioms form the theory of the random graph. Repetition of the fresh-vertex requirement also forces infinitude.

To prove quantifier elimination, first eliminate one existential quantifier from a quantifier-free formula. Put that formula into disjunctive normal form, so it suffices to consider a conjunction of literals in a new variable $z$ and the parameter variables. There are two possibilities for a witness: $z$ equals one of the parameters, in which case substitution gives a quantifier-free condition; or $z$ is distinct from all of them. In the latter case, the graph axioms reduce all requirements involving $z$ to specified adjacency or nonadjacency to the distinct parameter vertices. A requirement $E(z,z)$ is impossible, and conflicting requirements at equal parameter vertices are impossible. Every other consistent adjacency pattern is realized by the extension axiom.

There are only finitely many equality patterns of the given parameter tuple. For each, consistency of the literals is a quantifier-free condition, including the unchanged relations among the parameters. Their finite disjunction describes exactly when a witness exists. Thus $\exists z\theta (z,\mathbf{x})$ is equivalent to a quantifier-free formula whenever $\theta$ is quantifier-free. Mathematical induction on formulas now eliminates all quantifiers, using $\forall z\theta \equiv \neg \exists z\neg \theta$. Hence the random-graph theory eliminates quantifiers. The extension axioms also yield the usual countable random graph by a back-and-forth construction.

The Ehrenfeucht theory of an increasing named sequence is complete and has quantifier elimination: the usual one-point cut argument for dense linear orders without endpoints works with the finitely many constants occurring in a formula. Complete types are consequently determined by order relations to the named constants and to any additional parameters.

In the model where the sequence is unbounded above, every finite tuple lies below some $c_N$. Its order relations to $c_0,\dots ,c_N$, together with its internal equality and order pattern, determine its relations to every later constant as well. This finite condition isolates its complete type. Thus model (ii) is an atomic model. It is not omega-saturated, because the finitely satisfiable type $\{c_i<x:i\in \mathbb{N}\}$ has no realization.

In either bounded model, a point above every $c_i$ realizes the typeThis type is not isolated. Any formula belonging to it uses only finitely many constants after quantifier elimination, and its order condition can also be realized below a sufficiently late $c_j$. That realization fails one of the later inequalities in $p_{\infty }$. Hence neither bounded model is atomic.

In model (i), let $d$ be the least upper bound. The type $\{c_i<x:i\in \mathbb{N}\}\cup \{x<d\}$ over the single parameter $d$ is finitely satisfiable by density but unrealized, so this model is not omega-saturated.

In model (iii), the upper tail $U=\{x:c_i<x\text{ for all }i\}$ has no least element. Every consistent one-type over finitely many parameters is realizable. Indeed, it is either an equality type, a cut below or between some of the named constants, or a cut in $U$. The first two cases are realized by equality or by density in the relevant interval. In $U$, finitely many parameters divide the tail into finitely many intervals, each relevant nonempty interval having points by density, absence of a least element in $U$, and absence of a last element in the order. This realizes the third case too. There is no other cut among the increasing sequence: a proper initial segment of its indices is finite. Successive one-variable realizations give all finite-tuple types. ThereforeA least upper bound is thus precisely the obstruction to filling the additional finite-parameter cut in model (i).

Let $T_e$ be the theory of the extension axioms for an unrestricted binary relation. It has quantifier elimination. To prove this, consider a conjunction of literals $\theta (y,\mathbf{x})$. A witness $y$ equal to one of the parameters is handled by substitution. A witness distinct from them is governed entirely by a finite pattern of incoming edges, outgoing edges and its loop. For each equality pattern of the parameter tuple, incompatible literals make the pattern impossible, and every compatible pattern is supplied by the appropriate extension axiom. Thus existence of a witness is a finite disjunction of quantifier-free conditions on the parameters. Disjunctive normal form and induction on formulas eliminate all remaining quantifiers.

Given any formula $\varphi (\mathbf{x})$, choose a quantifier-free $\psi (\mathbf{x})$ withBy compactness theorem, finitely many extension axioms ${\sigma }_1,\dots ,{\sigma }_s$ already entail this particular universally quantified equivalence. Each has asymptotic probability one by the assumption. The union bound givesTherefore the universal equivalence also has asymptotic probability one. We obtain asymptotic equivalence to a quantifier-free formula, uniformly over every tuple in each structure satisfying those finitely many axioms. An infinite conjunction of probability-one events is not used; the finite consequence supplied by compactness is essential.

Here is the existential common-substructure test for quantifier elimination. Use a first-order language with a constant symbol, as in the applications below, or the usual conventions for empty generated substructures and truth constants. Let $T$ be a first-order theory. Suppose that whenever $\mathcal{M},\mathcal{N}\models T$ have a common substructure $\mathcal{A}$, then, for every quantifier-free formula $\theta (x,\bar{y})$ and every finite tuple $\bar{a}\in A$,The condition is symmetric because it applies also with $\mathcal{M}$ and $\mathcal{N}$ exchanged. The conclusion is quantifier elimination for $T$: for every first-order formula $\phi (\bar{y})$ there is a quantifier-free formula $\psi (\bar{y})$ such thatThe common substructure need not itself satisfy $T$, and witnesses are sought in the whole models, not necessarily in $A$. This test is the QET1 version of the common-substructure test for quantifier elimination.

Let $T_{\forall }$ denote the universal consequences of a theory: all universal first-order sentences entailed by $T$. A first-order structure satisfies $T_{\forall }$ exactly when it embeds into a model of $T$, by the compactness theorem applied to its diagram of a structure.

The theory has algebraically prime models if, for every $\mathcal{A}\models T_{\forall }$, there are $\mathcal{P}\models T$ and a structure embedding $i:\mathcal{A}\to \mathcal{P}$ such that every structure embedding $j:\mathcal{A}\to \mathcal{N}$, $\mathcal{N}\models T$, factors as $j=h\circ i$ for some structure embedding $h:\mathcal{P}\to \mathcal{N}$. Neither $i$ nor $h$ is required to be elementary.

For $\mathcal{M}\subseteq \mathcal{N}$, simple closure means that every existential quantifier-free formula over $M$ which has a witness in $N$ has one in $M$:Now take two models $\mathcal{M},\mathcal{N}\models T$ with common substructure $\mathcal{A}$. Since $A$ embeds into $M$, it satisfies $T_{\forall }$. Choose its algebraically prime extension $\mathcal{P}$, and embed $P$ into both $M$ and $N$ over $A$.

If $\exists x\theta (x,\bar{a})$ holds in $M$, the image of $P$ in $M$ is a model of $T$. The assumed simple closure of this image transfers a witness from $M$ into $P$. Its embedding into $N$ then transfers the quantifier-free formula and its witness into $N$. Thus the hypothesis of QET1 is satisfied. The second test follows: $T$ has quantifier elimination.

Both assertions are false. For simple closure, take the inclusionBoth satisfy DAG prime, but the quantifier-free formula $x\ne 0$ has a witness in $N$ and none in $M$. The same example works in the reduced language $\{+,0\}$.

For quantifier elimination, the first-order sentence $\exists x(x\ne 0)$ distinguishes these two models. Every closed group term is zero, so every atomic closed equality is true in both models. Every quantifier-free sentence, being a Boolean combination of such equalities, has the same truth value in both. The distinguishing sentence therefore has no equivalent quantifier-free sentence modulo DAG prime. HenceIncluding the trivial group is exactly what makes the proposed simple closure condition fail.

Assume $T$ has quantifier elimination, and let $j:\mathcal{M}\to \mathcal{N}$ be a structure embedding between its models. For any first-order formula $\phi (\bar{x})$, choose a quantifier-free formula $\psi$ equivalent to it modulo $T$. A structure embedding preserves and reflects atomic formulas; induction through the Boolean connectives therefore preserves every quantifier-free formula. ThusThe embedding is elementary. Every theory with quantifier elimination is model-complete.

A formally real field is a field in which $-1$ is not a finite sum of squares. The theory of formally real fields consists of the field axioms and, for each $m\ge 1$, the sentenceA real closed field is a formally real field with no proper formally real algebraic extension. An equivalent first-order axiomatization of the Theory of real closed fields adds: every $a$ or its negative is a square, and every odd-degree polynomial has a root. Explicitly the square axiom isand the polynomial axioms say that every monic polynomial of degree $2d+1$ has a root, for each $d\ge 0$.

The Artin-Schreier ordering criterion says that every formally real field can be ordered, and the real closure theorem embeds each ordered field into an algebraic real closed field extension. Consequently every FRF model embeds into an RCF model. Conversely every RCF model is itself an FRF model, so the reverse embedding requirement is automatic.

It remains to establish model completeness. A real closed field has a unique order, definable in the field language byAny field embedding between real closed fields preserves this order: positive elements are nonzero squares, and negative elements have positive negatives. The quantifier elimination for ordered real closed fields theorem makes every such ordered embedding elementary, by the preceding part. Restricting to formulas of the field language makes the original embedding elementary as well. Thus RCF is model-complete in the field language.

The embedding conditions and model completeness proveThe quantifier elimination invoked here is in the ordered language. In the unordered field language, model completeness still holds, but full quantifier elimination does not follow from forgetting the order.

A theory $T$ has quantifier elimination when every first-order formula is equivalent modulo $T$ to a quantifier-free formula with the same free variables.

Let tuples $\bar{a}\in M\models T$ and $\bar{b}\in N\models T$ have the same quantifier-free type. The map $\bar{a}\mapsto \bar{b}$ extends to an isomorphism between the substructures they generate. Identify these substructures with one structure $A$. Both expanded models satisfy $T\cup D(A)$, which is complete by hypothesis, so they satisfy the same formulas with parameters from $A$. Thus $\bar{a}$ and $\bar{b}$ have the same complete type.

Therefore every isomorphism between substructures of models of $T$ is partial elementary. By compactness, this implies that every formula is equivalent modulo $T$ to a quantifier-free formula: otherwise two tuples with the same quantifier-free type but different truth values could be constructed. This is the common-substructure test for quantifier elimination, so $T$ admits quantifier elimination.

Use the finite-partial-isomorphism criterion for quantifier elimination. Let $M,N\models \mathrm{DLO}$ and let $h:A\to B$ be an isomorphism between finite suborders. For $a\in M\setminus A$, its position relative to $A$ is one of the finitely many open intervals determined by $A$, or one of the two exterior rays. The corresponding interval or ray determined by $B$ is nonempty because the orders are dense and have no endpoints. Choose $b$ there. Then $h\cup \{(a,b)\}$ remains a partial order isomorphism.

The same argument extends in the other direction. The back-and-forth method criterion therefore applies, proving quantifier elimination for dense linear orders without endpoints. Hence DLO eliminates quantifiers.

Every finite partial isomorphism between models of $T_1$ extends by one point. If the new point belongs to a class already represented in the domain, choose an unused point in the corresponding target class. Otherwise choose an unused point in the other target class. Both classes are infinite, so the choice is always possible. The back-and-forth method shows that tuples with the same quantifier-free type have the same complete type. Therefore $T_1$ has quantifier elimination.

In the language of ordered rings, the Theory of real closed fields has quantifier elimination. In its pure ring reduct the order is definable by nonzero squares, so model completeness survives, although quantifier elimination does not. Keeping these two language conventions separate is essential when constructing a model companion.

Remove the nonzero-model axiom from DAG. The inclusion $\{0\}\subseteq \mathbb{Q}$ is then an inclusion of models but is not a simple closure, because $x\ne 0$ has a witness only in the larger model. The theory does not have quantifier elimination: all closed group terms are zero, so no quantifier-free sentence distinguishes the two models.