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 be a first-order theory. Suppose that whenever have a common substructure , then, for every quantifier-free formula and every finite tuple ,
The condition is symmetric because it applies also with and exchanged. The conclusion is quantifier elimination for : for every first-order formula there is a quantifier-free formula such that
The common substructure need not itself satisfy , and witnesses are sought in the whole models, not necessarily in . This test is the QET1 version of the common-substructure test for quantifier elimination.
Let denote the universal consequences of a theory: all universal first-order sentences entailed by . A first-order structure satisfies exactly when it embeds into a model of , by the compactness theorem applied to its diagram of a structure.
The theory has algebraically prime models if, for every , there are and a structure embedding such that every structure embedding , , factors as for some structure embedding . Neither nor is required to be elementary.
For , simple closure means that every existential quantifier-free formula over which has a witness in has one in :
Now take two models with common substructure . Since embeds into , it satisfies . Choose its algebraically prime extension , and embed into both and over .
If holds in , the image of in is a model of . The assumed simple closure of this image transfers a witness from into . Its embedding into then transfers the quantifier-free formula and its witness into . Thus the hypothesis of QET1 is satisfied. The second test follows: has quantifier elimination.
A torsion-free divisible Abelian group is naturally a vector space over the rational numbers: for and , define as the unique with . Divisibility supplies existence and torsion-freeness supplies uniqueness.
In the usual group first-order language , a model of the universal part of DAG is a torsion-free group which is Abelian. If the language instead uses only , a substructure can be merely a torsion-free cancellative commutative monoid. Handle this convention by first taking its Grothendieck group : its elements are formal differences , with
The cancellative commutative monoid condition makes injective. If , then , and torsion-freeness gives ; hence is a torsion-free abelian group. In the full group language simply take .
For form its rational divisible hull
Concretely its elements are fractions with , where if . The canonical embedding of into is injective, and is nontrivial, divisible, Abelian and torsion-free, so it satisfies DAG.
Let be any structure embedding into a model of DAG. Extend it first to formal differences if necessary. Its unique extension to the rational divisible hull sends to the unique element with . This is a group homomorphism fixing the given copy of . It is injective: an element mapped to zero has , hence . Thus every embedding into a DAG model factors through .
The zero case must be treated separately: its rational divisible hull is zero and does not satisfy DAG. Instead choose . Given any nontrivial DAG model , choose ; the map embeds into over zero. Therefore DAG has algebraically prime models, including over the trivial base.
Both assertions are false. For simple closure, take the inclusion
Both satisfy DAG prime, but the quantifier-free formula has a witness in and none in . The same example works in the reduced language .
For quantifier elimination, the first-order sentence 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. Hence
Including the trivial group is exactly what makes the proposed simple closure condition fail.

Articles by others on the same topic (0)

There are currently no matching articles.