In a model of the axioms for the theory of successor, repeatedly taking successor and predecessor partitions the domain into components. Injectivity and the predecessor axiom leave only the zero-generated one-sided chain and two-sided chains; the no-cycle axioms exclude finite components. Choosing one origin in each remaining component gives the displayed structure.
These axioms have quantifier elimination. To eliminate one existential quantification, put its quantifier-free matrix in disjunctive normal form. In a conjunction, an equality between a successor iterate of the bound variable and a parameter term fixes at most one candidate, by injectivity. Existence of the finitely many necessary predecessors excludes only finitely many initial zero iterates; the other equalities and inequalities then translate to conditions on the parameters by cancellation of successor iterates. If there is no such fixing equality, only finitely many candidates are excluded, so some point on the infinite zero chain works. Equalities between two different iterates of the same variable are false by absence of cycles. Thus the existential formula reduces to a quantifier-free formula.
Every closed quantifier-free sentence is decided by the distinct zero iterates, proving completeness. A one-variable formula over the empty set is a Boolean combination of finitely many equalities , modulo this theory. All points in added integer chains therefore realize the same nonisolated complete type over the empty set. At an uncountable cardinal a model has exactly integer components, proving categoricity there. A countable model with infinitely many integer components is an omega-saturated model because finite parameters involve only finitely many components, leaving a fresh one for every new-component type.
Countable atomic model without a countable saturated model Created 2026-10-14 Updated 2026-10-31
Take a countable structure with countably many independent unary predicates, every finite predicate pattern realized infinitely often, and a constant naming every element. Its complete theory has an atomic model: tuples of named elements have types isolated by equations to their names. But every infinite binary predicate pattern, together with inequalities to every named element, is consistent. There are uncountably many such one-types, so no countable omega-saturated model exists. Thus existence of a countable atomic model does not imply existence of a countable saturated one.
For each irrational real cut , the displayed comparisons with named rationals are finitely satisfiable. Quantifier elimination for dense linear orders makes them determine a complete type, omitted by the named rational structure itself. Different cuts give different types, so there are continuum many. An omega-saturated model must realize all of them and cannot be countable, although the named rational structure is countable, atomic and prime.
Add constants 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 over its least-upper-bound parameter .
Let be a countable omega-saturated model and finite. Then is a parameter-free definable set exactly when every structure automorphism preserves it setwise. One direction is automorphism invariance of parameter-free definability. For the converse, saturation implies homogeneity and the back-and-forth method show that equal empty-set types are in the same automorphism orbit. For , if no formula in has its realization set contained in , the partial type is finitely satisfiable. Its parameters form a finite set, so saturation realizes it outside , contradicting invariance. Choose a defining neighbourhood for each and take their finite disjunction. The empty set is defined by . Setwise invariance permits automorphisms to permute points within .
A definable set has parameter-free definability when its defining first-order formula uses only the original first-order language, with no additional constants naming elements. Constants already present in the language are allowed. Every such set is invariant under all automorphisms of a first-order structure. For example, zero in the constant-free additive integers is defined by , while the singleton containing one is not parameter-free definable because negation is an additive automorphism moving it. Invariance is a necessary condition in every structure, and becomes sufficient for finite sets in a countable omega-saturated model.
An atomic model is a model in which every finite tuple's complete type over the empty set is isolated by a formula. An omega-saturated model realizes every complete type in finitely many variables over every finite parameter set; equivalently it realizes all one-variable types over finite parameter sets, then successive realizations give the finite-tuple version.
Suppose is countable and omega-saturated. Every type in is realized by a tuple in , so is countable. This is a compact Hausdorff Stone space with a clopen basis. Its isolated points are dense. Indeed, if a nonempty clopen subset had no isolated point, split it into two disjoint nonempty clopen subsets and recursively split every resulting subset. Such splits exist because each subset has at least two points and the space is zero-dimensional. Compactness supplies a point in each nested sequence along an infinite binary branch, while disjoint siblings make different branches yield different points. This would give uncountably many points, contradicting countability.
For each , let consist of the negations of all formulas that isolate complete -types. Density of isolated types means that every consistent formula has a consistent refinement to an isolating formula ; this refinement excludes the member of . Thus locally omits every . The omitting types theorem gives a countable model omitting them all. Every tuple in therefore satisfies some isolating formula, so is atomic. If some is itself inconsistent, its omission is automatic and does not obstruct this argument.
The converse about existence is false. Here is a countable atomic model without a countable saturated model. Take a countable set with unary predicates , , such that every finite Boolean pattern of the predicates occurs infinitely often. For example, use finite binary words paired with a natural number, with recording the th bit when it exists and false otherwise. Add a constant naming each element, and put in this countable language. Every tuple of has its type isolated by equations to its named coordinates, so is a countable atomic model.
For each infinite binary sequence , the family
is finitely satisfiable in : realize its finitely many predicate requirements while avoiding finitely many named elements. By compactness theorem, it extends to a complete one-type. Different sequences give different types, so is uncountable. Any omega-saturated model must realize all these empty-parameter types, which a countable model cannot do. This disproves the existence converse, rather than merely exhibiting an atomic model that is itself nonsaturated.
An omega-saturated model realizes every complete type of a finite tuple over every finite set of its domain. It suffices to require this for one-variable types: realize the coordinates successively, enlarging the finite parameter set at each step.
Every complete theory here has such a model, with no countability requirement on its size. Start with a model of size at most . There are at most types over its finite sets, because the language is countable and each such type is a set of formulas in a countable collection. By the compactness theorem and the elementary diagram construction, pass to an elementary extension realizing all these types, keeping size at most by the Löwenheim-Skolem theorem.
Repeat this for stages and take the union of the elementary chain. Any finite parameter set in the union lies in some stage, and every type over it is realized at the next stage. The union is therefore omega-saturated. Countable language does not by itself guarantee that a countable saturated model exists.
No. The parameter-free partial type
is finitely satisfiable in the ordered real field: choose a number larger than the finitely many bounds. By compactness theorem it extends to a complete type over the empty set. But no real number realizes it, by the Archimedean property. Therefore the ordered real field is not an omega-saturated model.
The named unit and addition make every integer bound expressible, even without extra parameters. This is why the obstruction is present in the ordered-field language and absent in the two reducts above.
Yes. As an Abelian group, the reals are a nontrivial torsion-free divisible group, equivalently a vector space over the rationals. Rational scalar multiplication is uniquely definable by equations such as , so adding those operations is a definitional expansion.
In this language, quantifier elimination for torsion-free divisible Abelian groups reduces formulas to Boolean combinations of rational linear equations. Over finitely many parameters, a complete one-variable type either fixes a value in their linear span or excludes every value in that span. The first kind is realized in the span itself; the second is realized by any real number outside it. That span is countable, while the reals are uncountable. Thus every such type is realized and the additive real group is an omega-saturated model.
For finite tuples, the same argument successively supplies any required finite number of new rationally linearly independent elements. The order and multiplication of the real field are absent from this language, so they cannot impose additional type conditions.
Suppose is an omega-categorical theory. By the Ryll-Nardzewski theorem, every finite-arity complete type over the empty set is isolated. Let be a complete type over a finite tuple in the unique countable model , and take an elementary extension realizing it at . The joint type of is isolated by a formula .
The complete type of contains , since this formula is true of in the extension. Hence it is true of in , and some satisfies . Isolation of the joint type implies that realizes . Thus the countable model is an omega-saturated model.
The converse fails. The complete successor theory from question 4 has a countable model
with countably infinitely many two-sided successor components. It is omega-saturated. Over finitely many parameters, a complete one-variable type either fixes a finite successor/predecessor translate of a parameter or zero, or asks for a point in no component represented by those parameters and zero. The first kind is realized in the named component, and the second in an unused integer component. The quantifier-elimination description of classification of models of the successor theory shows there are no other cases.
Nevertheless this theory is not omega-categorical: and its standard model are countable and not isomorphic. Thus existence of a countable saturated model is strictly weaker than countable categoricity.
Here fixed means fixed setwise: for every structure automorphism , not that each point must be fixed individually. A parameter-free definable set has this invariance by automorphism invariance of parameter-free definability.
For the converse, first establish the needed saturation implies homogeneity step. In a countable omega-saturated model, a finite partial elementary map can be extended to include any prescribed additional element in its domain. Transfer the element's complete type over the old finite domain along the map. Each finite part of this transported type has a witness because the old map is elementary; the omega-saturated model realizes the full transported type. The inequalities in the type maintain injectivity. Apply the same construction to the inverse map to enlarge the range. Alternating these steps through an enumeration of the countable domain is the back-and-forth method, giving a structure automorphism. In particular, any two elements with the same complete type over the empty set are related by a structure automorphism.
Assume now that is finite and invariant, and fix . All realizations in of belong to , by the preceding homogeneity and the invariance assumption. Suppose that no parameter-free first-order formula has all its realizations in . Then every finite subset of
is satisfiable in : conjoin the finitely many first-order formulas from , and use the assumed absence of a defining neighbourhood inside to find a witness outside . This is a partial type over the finite parameter set . The omega-saturated model would realize it by an element outside with the same empty-set type as , a contradiction. Hence such a does exist.
There are only finitely many , so
For , use . Thus finite invariant sets in a countable saturated structure are definable. Finiteness is used twice: the extra parameters form a finite set, and the final disjunction is a first-order formula rather than an infinite disjunction.
An omega-saturated model realizes every complete one-type over every finite subset of its domain that is consistent with the first-order structure's first-order theory with those named parameters. Equivalently, every partial type in a finite tuple over finitely many parameters that is finitely satisfiable in the first-order structure has a realization there. The equivalence follows by extending a partial type to a complete type; finite tuples can be handled one coordinate at a time.
For an example, take a countably infinite set in the language of equality alone. Over finitely many named elements, a complete one-type either requires equality with one of them or inequality with all of them. Both possibilities are realized. quantifier elimination for an infinite pure set follows by choosing a quantified variable either equal to one of the finitely many named values or distinct from all of them. Indeed every permutation fixing the parameters is a structure automorphism, and all other elements have the same type, so there are no further one-types. This first-order structure is omega-saturated.
For a counterexample, take , where . The parameter-free partial type
is finitely satisfiable: choose an integer beyond the finitely many excluded numerals. It is not realized in the first-order structure, because every natural number is one of those numerals. Any complete extension of this partial type is therefore omitted as well. Thus the standard successor first-order structure is not omega-saturated.
In a torsion-free divisible Abelian group, division by a nonzero integer is unique. The rational scalar operations are therefore a definitional expansion. Formulas reduce to Boolean combinations of rational linear equations: eliminate an existential variable in a conjunction by solving any equation with nonzero coefficient; if none fixes the variable, the finitely many nontrivial disequalities exclude only finitely many choices in an infinite group. Equations with zero coefficient reduce to parameter conditions.
Thus over a finite parameter set a complete one-variable type either specifies an element of its linear span, or excludes every element of that span. An uncountable rational vector space realizes the latter type because a finite-parameter span is countable. It is consequently an omega-saturated model in the additive language.