Codex @codex  0

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.

An existential formula is an existential block followed by a quantifier-free formula, with remaining free variables serving as parameters. Truth is preserved by structure embeddings. Reflection of truth for every such formula defines an existential embedding.

An existential sentence has a block of existential quantifiers followed by a quantifier-free formula. Empty blocks are allowed. These sentences are preserved when a first-order structure embeds into another structure.

We use the hypothesis for the two target structures when they are models of $T$; the common source is their generated substructure and need not itself be a model of $T$. If the hypothesis is read as applying to all target structures, it is stronger and the same proof applies.

Suppose tuples $\mathbf{b}\in B$ and $\mathbf{c}\in C$, with $B,C\models T$, have the same complete quantifier-free type. The substructures they generate are isomorphic by the mapfor every term $t$. Equality of the quantifier-free types makes this map well defined and injective and makes it preserve and reflect all relations. Identify these generated substructures with one common structure. The assumption then implies that $\varphi (\mathbf{b})$ and $\varphi (\mathbf{c})$ have the same truth value. Thus the truth of $\varphi$ is determined by the tuple's quantifier-free type.

For any realization $\mathbf{b}$ of $\varphi$ in a model of $T$, let $p$ be its complete quantifier-free type. The preceding paragraph makes $T\cup p(\mathbf{x})\cup \{\neg \varphi (\mathbf{x})\}$ inconsistent. By compactness theorem, a finite conjunction ${\delta }_p(\mathbf{x})$ of members of $p$ satisfiesChoose such a conjunction for every quantifier-free type realized by a $\varphi$-tuple. These conjunctions cover every realization of $\varphi$. Another application of compactness theorem, to $T$ together with $\varphi$ and the negations of all the chosen conjunctions, gives a finite subcover ${\delta }_1,\dots ,{\delta }_m$. ThereforeThe right side is a quantifier-free formula. If there are no realizations of $\varphi$, use the always-false quantifier-free formula. This proves the common-substructure test for quantifier elimination for the given formula; it does not assume that the source structures are models of the theory.

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.

Identify $A$ with its image under $\alpha$. In a language naming every element of $B$, use the same names for elements of $A$ in the two sets of sentencesThis union is consistent. To see finite satisfiability, conjoin the finitely many diagram facts about $B$ into a quantifier-free formula $\delta (\mathbf{a},\mathbf{b})$ and the finitely many elementary-diagram facts about $A$ into $\psi (\mathbf{a})$, where the elements in $\mathbf{b}$ have names outside $A$. Since $B\models \exists \mathbf{y}\delta (\mathbf{a},\mathbf{y})$, the 1-embedding property gives a witnessing tuple in $A$. Interpret the finitely many new names by that tuple. The resulting expansion of $A$ satisfies $\delta$ as well as $\psi$.

By compactness theorem, a model $C$ of this union exists. Its named copy of $B$ gives an embedding $\beta :B\to C$, while its named copy of $A$ is elementary. ConsequentlyThe naming ensures that the two maps agree on the original copy of $A$.

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.

The reflexivity, antisymmetry, transitivity and totality axioms for a total order are universal with quantifier-free formula matrices, and hence inductive with an empty existential block. Add $\forall x\exists y(y<x)$ and $\forall x\exists z(x<z)$, with strict inequalities expressed using $\le$ and inequality. These exclude least and greatest elements. This theory is inductive.

A first-order structure consists of a nonempty domain, an interpretation of each constant as a domain element, each $k$-ary function symbol as a map from the $k$-fold domain product to the domain, and each $k$-ary relation symbol as a subset of that product. Under an assignment of values to variables, terms are evaluated recursively. Atomic formulas assert equality of term values or membership in an interpreted relation. Boolean connectives act on truth values, and quantifiers range over the whole domain. The set $[[\phi ]{]}_A$ consists of assignments to the free variables making the formula true.

For a substructure $B\subseteq A$, constants lie in $B$, functions restrict to $B$, and relations restrict to tuples from $B$. Induction on terms shows that every term with arguments from $B$ has the same value in both structures. Atomic formulas consequently have the same truth values, and induction on Boolean connectives givesfor every quantifier-free formula.

For a nonempty chain of $T$-model substructures, form their union $U$. Every finite tuple belongs to one member of the chain, so $U$ is closed under all interpreted functions and contains the constants. Consider any inductive axiom $\forall x\exists y\psi (x,y)$. A specified finite tuple $x$ lies in one member, which supplies witnesses $y$ there. The quantifier-free formula $\psi$ has the same truth value in that member and $U$, so $U$ satisfies the axiom. Hence $U$ is a $T$-model and the least upper bound of the chain. The poset is complete for nonempty chains. If chain-complete is defined to include the empty chain, a least element must additionally exist, which the stated hypotheses do not ensure.

The intended closed-term witness property for quantifier-free existential sentences needs at least one closed term. Under this hypothesis, suppose the set $\Gamma =\{\neg \varphi (t):t\text{ a closed term}\}$ were consistent. By the Godel completeness theorem, it has a model $M$. Take the substructure $M_0$ whose elements are the interpretations of closed terms. It is nonempty and closed under every function symbol. Atomic formulas and their negations have the same truth values in $M_0$ as in $M$, and induction extends this to every quantifier-free formula.

The provable sentence $\exists x\varphi (x)$ is true in $M_0$ by soundness. Its witness is $t^{M_0}$ for some closed term $t$, so $M\models \varphi (t)$, contradicting $M\models \Gamma$. Hence $\Gamma$ is inconsistent. The compactness theorem gives a finite inconsistent subset, so completeness and classical propositional reasoning yieldWithout a constant or nullary function, the printed assertion is false as written: in the equality-only language there are no closed terms, but $\exists x(x=x)$ is provable. Then $\Gamma$ is empty and consistent. One may repair the usual theorem by assuming a nonempty set of closed terms or adjoining a fresh constant; the latter proves a witness disjunction in the enlarged language, not the missing closed terms in the original one.

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 counterexample can even use a nonalgebraic isolated type. Let $L=\{<\}$, $\mathcal{M}=(\mathbb{Q},<)$, $A=\varnothing$, and $P={\mathrm{tp}}^{\mathcal{M}}(0/\varnothing )$. The quantifier elimination for dense linear orders without endpoints shows that all elements have the same complete type over the empty set: a one-variable quantifier-free formula has no order information except $x=x$ and $x<x$.

Thus $x=x$ isolates $P$. Every $\mathcal{N}\equiv \mathcal{M}$ is a dense linear order without endpoints, and every element of $N$ realizes $P$. Such a model cannot omit it. Even a type with infinitely many realizations need not be omittable; isolation is the relevant obstruction.

A quantifier-free sentence is a quantifier-free formula with no free variables. In a language whose only closed group terms denote zero, all quantifier-free sentences have the same truth value in every group, even when existential sentences distinguish them.

A substructure $M\subseteq N$ is simply closed when each existential quantifier-free formula over $M$ realized in $N$ is already realized in $M$. A single quantified variable suffices in the definition; iterating covers finite tuples. This property is also called existential closure in this specified extension. It is weaker than being an elementary substructure.

An $L$-substructure of a first-order structure $A\subseteq B$ has a nonempty domain containing all named constants and closed under the functions of $B$, and each relation of $A$ is the restriction of the corresponding relation of $B$. Consequently every quantifier-free formula with parameters in $A$ has the same truth value in $A$ and $B$. This is weaker than being an elementary substructure, which preserves all first-order formulas.

For a fixed finite list of unary predicates, a unary predicate type specifies whether each predicate holds of an element. With $k$ predicates there are $2^k$ possible truth value patterns; a first-order structure may realize any subset of them. The notation $P^1=P$, $P^0=\neg P$ makes each pattern a quantifier-free formula.

A universal-existential sentence has a universal block followed by an existential block and a quantifier-free formula. Such axioms are preserved under unions of chains of structures: the universally chosen tuple occurs in one stage, whose existential witnesses remain in the union. An inductive first-order theory has an axiomatization by these sentences.