Let isolate the principal type. Consistency with means is satisfiable. Because is a complete theory, it must imply ; the alternative would make that extension inconsistent.
Therefore every model of has a tuple satisfying . Each implication then makes satisfy every member of the type. Hence
Completeness is what turns possible realization of the isolating formula into realization in every model.
Take the standard successor structure and its disjoint union with one two-sided integer successor chain:
Both interpret the named zero in the natural-number component. The classification of models of the successor theory describes every model as this distinguished one-sided chain together with an arbitrary collection of two-sided chains. Its axioms are injectivity of , zero outside its range, a predecessor for every nonzero element, and absence of finite cycles. These axioms are complete; equivalently the theory has the successor quantifier-elimination property explained in the concept proposal.
Consequently both displayed structures are models of the standard complete theory. They are not isomorphic: any isomorphism must fix zero and hence every element . The first structure has no other elements; the second has the entire extra integer chain. Being in that additional component is an isomorphism invariant even though being outside all standard iterates of zero is not expressible by one first-order formula.
An atomic model is a model in which every finite tuple realizes an isolated complete type over the empty set. For a complete theory in a countable language, every countable atomic model is prime. The underlying argument is a back-and-forth method in the one-sided form needed for an embedding: enumerate the atomic model, and extend a finite partial elementary map one element at a time using an isolating formula for the enlarged tuple. The target model has the required witness because the already matched tuple has the same complete type.
Thus property (iii) implies property (iv). It need not imply pointwise definability or term-generation. The countable dense linear order without endpoints with a single named point, for example , is atomic: quantifier elimination for dense linear orders without endpoints isolates a tuple by its finite order-and-equality pattern relative to zero. But order structure automorphisms fixing zero move every nonzero rational. Such elements are not parameter-free definable, and no closed term names them. This supplies the failed implications (iii)(ii) and (iii)(i).
An element is parameter-free definable if some formula of the original language has as its unique solution in the structure. Saying this for every element makes the model pointwise definable.
If a finite tuple has individually defining formulas, their conjunction uniquely defines that tuple. Its complete type is isolated by this conjunction: for each formula , the sentence saying the unique tuple does or does not satisfy is decided by the complete theory. Thus
It follows that the countable model is also prime. The converse implication to property (i) fails. In every element is defined by having exactly predecessors, but the only closed term in this language is the constant . This infinite model is pointwise definable and is not term-generated.
A term-generated model is a structure in which every element is the value of a closed term of the original language. Equivalently its substructure generated by the empty set, including interpretations of named constants, is the entire structure. This is the relevant meaning of “term model” for a model of an arbitrary complete theory, rather than a claim about one particular syntactic construction.
Each closed term gives the parameter-free defining formula . Thus
The next parts show that pointwise definability implies atomicity, and countable atomicity is equivalent to primeness. Therefore property (i) implies all three other properties.
A prime model admits an elementary embedding into every model of its complete theory. In the countable setting a prime model is atomic. If a tuple in the prime model had a nonisolated complete type, the omitting types theorem would give a model omitting that type; an elementary embedding of the prime model into it would realize the omitted type, a contradiction.
Combining the four parts, all positive implications are exactly those generated by
The structure refutes (ii)(i). The structure is a countable atomic and hence prime model of its complete theory, while failing both (i) and (ii); it refutes every remaining reverse arrow, including (iv)(i) and (iv)(ii). The counterexamples therefore cover all ordered pairs of distinct properties not forced by the boxed chain.
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.
For the additive first-order structure, let
It defines . These sets are pairwise distinct: if , the integer belongs to but not to . Thus there are infinitely many inequivalent one-variable first-order formulas modulo the complete theory of the additive integers. The Ryll-Nardzewski theorem implies that first-order theory is not aleph-zero-categorical.
For the multiplicative first-order structure define divisibility by . For , the first-order formula
asserts the existence of at least distinct integer divisors. The integer has exactly such divisors, namely for , so it satisfies but not any with . Again there are infinitely many inequivalent one-variable first-order formulas. The Ryll-Nardzewski theorem therefore implies the first-order theory of the multiplicative integers is not aleph-zero-categorical.
A partial type is a set of -first-order formulas in a fixed tuple jointly consistent with . A complete type, the usual meaning of an -type here, is maximal among such consistent sets: for each first-order formula it contains exactly one of .
Add new constants and consider
Every finite subset is satisfiable by consistency of the type. The compactness theorem gives a first-order model of the full set. Its -reduct is a first-order model of , and the interpretations of realize . This proof applies to partial as well as complete types.
For a complete theory in a countable language, the types realized in every first-order model are exactly the isolated types. An isolated type has a consistent first-order formula such that for every . Completeness forces , so every first-order model realizes ; the converse is the omitting types theorem. Countability is a hypothesis of that converse, not of the preceding compactness realization argument. For a partial type the corresponding criterion is an isolating consistent first-order formula, together with its existence in every first-order model; it need not itself belong to the partial type.
If is not complete, no one complete -type can be realized in every first-order model of : a complete type decides sentences, and two completions of disagree on some sentence. Thus the completeness and countability hypotheses must be retained when using the isolated-type characterization.
The Ryll-Nardzewski theorem says that, for a complete theory in a countable first-order language, with infinite first-order models, the following conditions are equivalent: is aleph-zero-categorical; for every positive integer , its type space of complete types over the empty set is finite; and, for every , there are only finitely many -formulas in free variables modulo equivalence over . Here and are equivalent over when .
A complete theory is a consistent first-order theory deciding every sentence in its language:
Equivalently, every two first-order models of are elementarily equivalent. Consistency excludes the vacuous situation in which a first-order theory has no first-order models and entails both alternatives.
Take a countable elementary substructure of containing the named constant, using the Downward Lowenheim-Skolem theorem. Its reduct has infinitely many singleton and doubleton classes. In particular it contains the partner of each of its non-singleton elements, and its interpretation of is exactly the singleton-class predicate.
Choose new distinct elements . Define
In , make a new singleton class. In , make a new doubleton class; keep every old class of unchanged. All three reducts are first-order models of the complete theory, and .
Expand by interpreting as singleton-class membership and retaining the original named constant from . The resulting countable first-order structures are each isomorphic to : all have infinitely many classes of each size, and the bijections of classes can be chosen to preserve the constant and its class. Hence they are first-order models of . Both inclusions and are genuine structure embeddings, since no class meeting was changed. The given quantifier elimination, together with the preceding implication to first-order model completeness, yields
Taking reducts gives . But
so . There is no conflict with quantifier elimination in the expanded language: changes truth value, so is not a substructure of .
No. Let be the displayed infinite axiom set. Any finite subset mentions only finitely many of the two infinitude requirements. Choose at least as large as every index mentioned. A finite equivalence relation with exactly singleton classes and doubleton classes satisfies , but is not a first-order model of the complete theory.
If a finite axiomatization existed, let be the conjunction of its axioms. Then , so the compactness theorem gives a finite with . Every first-order model of would then satisfy the full first-order theory, contradicting the finite first-order model above. This is the finite subaxiomatization from an equivalent finite theory argument: finite axiomatizability would force one finite fragment of the explicit axioms to suffice.
The inclusion is a structure embedding between first-order models of the same complete theory, but it is not an elementary embedding, as the existential partner first-order formula at shows. Therefore the first-order theory is not model-complete. The facts and do not make the intervening inclusion elementary.
Pointwise definable model 2026-10-31
Every element of a pointwise definable model is uniquely specified by a formula with no added parameters. Finite tuples are then uniquely specified by conjunctions of their defining formulas. For a complete theory these formulas isolate the tuple types, so such a model is an atomic model. The converse fails: a countable dense linear order without endpoints with a named point is atomic, while its other points are moved by structure automorphisms fixing that point.
Stable theory Created 2026-09-28 Updated 2026-11-05
A complete theory is -stable, for an infinite cardinal , when for every parameter set of cardinality in a model of . Here is the type space of complete one-variable types. The theory is stable if this holds for some such ; it is omega-stable if it holds for .
For the theory of an infinite set with equality alone, a type over either names one element of or says that it differs from every member of . There are only possibilities. By contrast, a dense linear order without endpoints has the order property, producing many types corresponding to cuts and hence instability. Stability measures the number of ways a new element can relate to existing parameters, rather than simply the number of models.
Strongly minimal theory Created 2026-09-24 Updated 2026-11-05
A complete theory with infinite models is strongly minimal when, in every model, each definable subset in one variable, with parameters allowed, is finite or cofinite. The requirement applies to all models and all parameter choices. The infinite-universe condition excludes trivial finite theories.
For an infinite set in the language of equality, a one-variable formula with finitely many parameters can only distinguish those named elements from the remaining elements, so every definable subset is finite or cofinite. In an algebraically closed field, quantifier elimination likewise makes every one-variable definable subset finite or cofinite, since a nonzero polynomial has finitely many roots. A dense linear order without endpoints fails this property: a proper open interval and its complement are both infinite. Strong minimality is a particularly restrictive source of omega-stability.
Successor structure 2026-10-31
The standard successor structure has the natural numbers as domain, the successor function , and the named element zero. Its complete first-order theory is the theory of successor. Without addition, multiplication, or order, elements outside the zero-generated component are possible in other models of the same complete theory.
In the language containing one binary equivalence relation , require all classes to have size at most two and infinitely many classes of each of the two sizes. This is a complete theory: every countable model has countably many singleton classes and countably many doubleton classes, giving a class-by-class isomorphism; Downward Lowenheim-Skolem theorem then rules out a sentence separating arbitrary models. It is also an aleph-zero-categorical theory.
It is not finitely axiomatizable. Any finite fragment of the explicit infinitude schemes has a finite model with sufficiently many classes of each size; compactness theorem would make such a finite fragment suffice if any finite axiomatization existed. It is not model-complete: adjoining a new singleton preserves the theory, and subsequently giving that new point a partner also preserves the theory, while changing the existential partner formula at that point. Naming the singleton-class predicate removes this particular obstruction to elementary embeddings.
Theory of successor 2026-10-31
The complete theory of the standard successor structure is axiomatized by injectivity of , outside its range, a predecessor for every nonzero element, and the sentences for each positive integer . Its models have a single distinguished one-sided chain generated by zero and any collection of two-sided integer chains. The classification of models of the successor theory proves completeness and explains why the theory is categorical at every uncountable cardinal but not at the countable cardinal.