Let be the reduced product by a proper filter on a set. Its underlying equivalence relation is when . Operations are interpreted coordinatewise, and a relation holds of the classes exactly when its coordinate truth set belongs to .
Evaluation of a first-order term commutes with passage to the quotient, by mathematical induction on terms. Consequently the desired equivalence holds for every atomic formula, including logical equality. For a formula and representatives , write .
For logical conjunction, . The filter on a set axioms giveThus the induction hypothesis transfers a conjunction in both directions.
For existential quantification, first suppose . Choose a representative of a witness. Induction gives , and this set is contained in . Upward closure therefore gives .
Conversely, suppose . For each , choose a coordinate witness , and choose an arbitrary element of outside . These simultaneous choices use the axiom of choice, as does the usual product construction. Then , so that truth set belongs to . Induction gives , providing the required witness. Thereforefor every primitive positive formula. The exam's tame formulas are exactly this fragment, built using logical conjunction and existential quantification. No ultrafilter dichotomy was used.
Take and the proper filter on a set . In the first-order language with unary predicates , let both factors be one-element first-order structures. Set true and false in the first factor, and reverse these truth values in the second.
The reduced product also has one element . Neither nor holds there: their truth sets are and , neither belonging to . ThusLogical disjunction can therefore break the equivalence. A union can belong to a filter on a set without either summand belonging to it; the corresponding union property does hold for an ultrafilter.
Use the same two-index filter on a set , with a unary predicate true only in the first one-element factor. In the reduced product, is false, so is true. ButLogical negation also breaks the equivalence. For a general proper filter on a set, a set and its complement can both be absent. In an ultrafilter, exactly one belongs, which is the step used to transfer logical negation in the Łoś theorem.
An ultrafilter on is kappa-complete if, for every index set with and every family of members of ,The bound is strictly fewer than sets. In particular every ultrafilter is -complete, since this requires only finite intersections; countably complete ultrafilters require intersections of countably many members, equivalently -completeness.
First use the fact that a small set is absent from a complete nonprincipal ultrafilter. Indeed, if and , then every , , belongs to by nonprincipality. Kappa-completeness gives , so . In particular every final segment belongs to .
Suppose for contradiction that the ultrapower has at most elements. List representatives for all its classes, indexed by ; repetitions are allowed. At coordinate , fewer than values occur among with . Since , chooseThis diagonal argument for ultrapower cardinality uses the axiom of choice. For each fixed , the functions and disagree throughout the final segment , which belongs to . Their equality set therefore cannot belong to , and .
This contradicts the assumed enumeration of the ultrapower. HenceThe proof uses only that each ordinal has cardinality below ; it does not require a separate assumption of regularity.
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 thatThe 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 , withThe 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 hullConcretely 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 inclusionBoth 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. HenceIncluding the trivial group is exactly what makes the proposed simple closure condition fail.
A first-order theory is model-complete if every structure embedding between models of is an elementary embedding. Equivalently, whenever and both satisfy , one has :for every first-order formula and every finite tuple . This is preservation of all formulas with parameters, rather than merely all first-order sentences.
Assume has quantifier elimination, and let be a structure embedding between its models. For any first-order formula , choose a quantifier-free formula equivalent to it modulo . 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 model companion of a first-order theory , in the same first-order language, is a model-complete theory with the same universal consequences of a theory as :Equivalently, every model of embeds into a model of , and every model of embeds into a model of . The equivalence follows from the diagram embedding criterion for universal theories, which is an application of the compactness theorem. A model companion need not be a syntactic extension of , and uniqueness is understood up to logical equivalence of theories.
Suppose and are model companions of . Their universal consequences of a theory agree, so the diagram embedding criterion for universal theories permits embeddings in both directions between their model classes.
Starting from any , alternately take such extensions, identifying each model with its image under the embedding:Since is model-complete, ; since is model-complete, . The two subsequences have the same union . The elementary chain theorem givesEvery axiom of , as a sentence true in , is therefore true in . Thus every model of is a model of . Reversing their roles proves the converse. The model companion is unique up to logical equivalence. If is inconsistent, its only possible companion is likewise inconsistent, so the same uniqueness conclusion holds.
A formally real field is a field in which is not a finite sum of squares. The theory of formally real fields consists of the field axioms and, for each , 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 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 has a root, for each .
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.
The quantifier rank measures maximum nesting depth:Two first-order structures are rank-n equivalent if they agree on all first-order sentences of quantifier rank at most . For tuples one similarly compares all such formulas evaluated at the tuples.
In the -round Ehrenfeucht-Fraïssé game, player I, the Spoiler, chooses an element from either structure each round; player II, the Duplicator, chooses an element in the other. After rounds the corresponding chosen tuples must define a partial isomorphism of structures: all atomic formulas, including equality and the interpretations of constants, have matching truth values. Repetitions must be respected. Failure of this condition is a loss for II.
The precise finite-vocabulary Ehrenfeucht-Fraïssé theorem is: for a finite relational language, allowing finitely many constants,The tuple version has the same conclusion when the corresponding tuples are fixed before play. The implication from a winning strategy to rank equivalence holds for arbitrary languages, by induction on formulas. For the converse, finite relational vocabulary ensures only finitely many rank-bounded types in a fixed tuple of variables; their defining formulas let one transfer the type of the next move. Without a finiteness hypothesis, the converse for the full atomic-diagram game need not hold. This qualification matters in the next part.
Under the finite relational vocabulary hypothesis of the Ehrenfeucht-Fraïssé theorem, II wins the timed game exactly when the structures are elementarily equivalent. If II wins, then for every choice of by I, its strategy restricts to a winning strategy in . Hence the models agree on every sentence of quantifier rank at most . Every first-order sentence has finite quantifier rank, so they agree on all sentences.
Conversely, elementary equivalence gives for every . Choose a winning strategy for each , and use that strategy once I announces . Unlike the infinite game, the timed game permits the strategy to depend on the announced horizon.
The PDF does not explicitly impose finite vocabulary. If an arbitrary language and the full partial isomorphism of structures winning condition are intended, the reverse assertion is false. Here is a failure of finite-round game equivalence in infinite languages. Let be unary relational. Letand obtain by adjoining one point satisfying every .
For any finite sublanguage, every Boolean cell of predicates has infinitely many elements in both structures. Every finite partial isomorphism of structures of these reducts can therefore be extended in either direction. Induction on formulas, or a back-and-forth method, shows their reducts are elementarily equivalent. Since every sentence uses finitely many symbols, in the whole language.
Nevertheless I wins by choosing : every point of fails some , so no response preserves all atomic formulas. Thus the printed unrestricted equivalence requires the finite-vocabulary convention, or a game which additionally restricts each play to a finite vocabulary fragment.
Use the one-relation language and the total orderswhere the second is the order sum: every point in its natural-number block lies below every point in its integer block.
To show II wins every finite Ehrenfeucht-Fraïssé game, use the interval threshold strategy for discrete linear orders. With rounds left, corresponding open intervals and end rays between already matched points have either the same size below , or both have at least elements. Their sizes may be infinite. The chosen-point correspondence is order preserving. Initially the unique interval is infinite in both orders, so the invariant holds.
If I chooses a repeated point, II repeats its counterpart. If I chooses in a short interval, II chooses the point with the same finite rank in the matching interval. In a long interval, let . If one side of the chosen point has fewer than elements, reproduce that size in the other interval; the opposite sides then both have at least elements. Otherwise choose a response having at least elements on each side. Such a response exists because the interval has at least elements. The endpoint and successor/predecessor properties of these two discrete orders allow the finite small-side counts to be reproduced. This establishes the invariant with rounds left and gives a finite-game winning strategy. Therefore II wins the timed game.
In the infinite Ehrenfeucht-Fraïssé game, I first chooses a point in the integer block of . It has infinitely many predecessors. II must respond with some , which has exactly predecessors. I then chooses distinct predecessors of . To preserve order and equality, II would need distinct points below , which is impossible. ThusI chooses the required finite length only after seeing II's first response, which explains why this does not contradict the timed-game result.
Take a rooted directed graph with one root and one terminal vertex , with its sole edge . Let have a root and two terminal vertices , with edges and . The relationis a bisimulation. Each root move can be matched by a root move ending in a related terminal vertex. At all related terminal pairs there are no further edges, so both matching conditions are vacuous. Yet the directed graphs have two and three vertices and cannot be isomorphic. Bisimilarity need not preserve the number of successors.
Here and in the next part, the second graph's edge relation is , and its response vertices belong to . These are the corrections to the printed relation and vertex slips in the bisimulation clauses.
Suppose first that is a bisimulation containing the root pair. II maintains the invariant that the current pair lies in . If I moves in the first rooted directed graph, the forth clause supplies a matching successor in the second; if I moves in the second, the back clause supplies a matching successor in the first. II can choose such a response every time I can move. Therefore II never loses after finitely many steps and wins the bisimulation game.
Conversely, let be a winning strategy for II. Define to consist of all endpoint pairs of finite legal plays starting at the roots and consistent with , including the initial root pair. This definition keeps every possible history; it does not assume that depends only on the current position.
Take and a finite history realizing it. For any successor of , extend that history by having I choose the edge . Since is winning, it supplies a successor of . The new endpoint pair belongs to , proving forth. Letting I choose any successor of proves back in the same way. Hence is a bisimulation andConnectedness ensures that both projections of cover all vertices: I can walk any finite directed path from either root and II's strategy supplies the matching path. The equivalence itself only concerns the rooted reachable behaviour and remains valid without connectedness.
Expand the language by constants for and write . An A-type over a structure is a set of formulas in a fixed finite tuple , with parameters from , consistent with this complete theory.
Let . If no tuple of realized , thenThat sentence belongs to and contradicts the consistency of . ConsequentlyFor , any tuple works because domains are nonempty. This proves finite satisfiability; realization of the entire partial type may require an elementary extension.
The Stone topology on a type space has basic open setswhere ranges over formulas with parameters in and free variables. Here points are complete types consistent with . Arbitrary open sets are unions of these basic sets.
The identitiesshow that the basic sets are clopen sets and form a basis. Distinct complete types contain opposite choices for some formula, so this topology is Hausdorff. The compactness theorem gives compactness: a family of basic closed sets with the finite intersection property determines a consistent set of formulas, which extends to a complete type. Thus logical formulas provide a basis of clopen tests for distinguishing points of the type space.
A precise countable-language form of the omitting types theorem is the following. Let be a consistent first-order theory in a countable first-order language, and let be a countable family of nonprincipal partial types, each in finitely many variables. Then there is a finite or countably infinite model of omitting all the .
A partial type is a set of formulas jointly consistent with . It is principal if there is a formula such that is consistent andFor a complete type, this is exactly being an isolated type. Nonprincipal means that no such formula exists. A model omits if no tuple in that model satisfies every formula in ; different tuples may fail different members of the type. The model in the theorem need not omit each individual formula everywhere.
For parameter types, use the expanded language naming the parameters. Countability then applies to that expanded language, and hence requires a countable parameter set as well. There is no countability restriction in the finite-satisfiability argument of part (a).
Let be an isolated type over , with isolating formula over . Its consistency with and the complete theory property implyotherwise would belong to , contradicting consistency. Choose a tuple satisfying . By isolation,so satisfies every member of . Therefore every isolated A-type is realized in the original structure. The same reasoning works for a principal partial type whose isolating formula need not itself be a member of the type.
Use the first-order language with one constant , take with equality only, and let . SetThis complete type contains and is isolated by that formula. In any first-order structure, at most one element can satisfy . In every , its interpretation of realizes , by elementary equivalence. Hence no elementarily equivalent model has infinitely many realizations of . An algebraic type can have a fixed finite number of realizations in every model.
A counterexample can even use a nonalgebraic isolated type. Let , , , and . 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 and .
Thus isolates . Every is a dense linear order without endpoints, and every element of realizes . Such a model cannot omit it. Even a type with infinitely many realizations need not be omittable; isolation is the relevant obstruction.
Use the countable-language hypothesis of the omitting types theorem, which is the usual convention for this prime-model result. Let be a prime model of and .
First, is complete up to logical consequence: every model receives an elementary embedding of , so it satisfies exactly the same sentences as . We may therefore replace by without changing its model class or the prime model property.
Suppose were not isolated. The omitting types theorem, applied to this single complete type, would produce omitting . By primality choose an elementary embedding . For every ,Then realizes , contradicting omission. ConsequentlyThe same proof applies to every finite tuple, giving an atomic model. Countability of the language is a hypothesis of this argument, not a restriction on parameter sets in the separate parts (a) and (d). The PDF does not state that standing hypothesis explicitly; it must be included when invoking this version of the theorem.
Articles by others on the same topic
There are currently no matching articles.