An equivalence-relation first-order structure with exactly two infinite classes, one countable and one uncountable, is atomic but lacks finite-tuple homogeneity. Its first-order theory has quantifier elimination: a new point is either assigned a previously used class or an available unused class, and can avoid finitely many forbidden points in that infinite class. Finite equality-and-equivalence patterns therefore isolate all tuple partial types. All elements have the same complete one-type, but no automorphism exchanges the two differently sized classes.
Complete one-type 2026-10-31
A complete one-type is a complete type in one free variable. It chooses exactly one of each first-order formula and its negation consistently with the first-order theory and the named parameters.
Continuum many one-types of the integer ring 2026-10-31
For every subset of the standard prime numbers, prescribe exactly which of those primes divide a nonzero element. Every finite prescription is realized by the product of its finitely many positive divisibility requirements. Compactness theorem extends each prescription to a complete one-type of the complete theory of the integer ring. Different subsets give incompatible partial types. The countable first-order language supplies the matching upper bound.
Omega-stability of a theory 2026-10-31
A complete theory in a countable first-order language is omega-stable if over every countable set of parameters it has only countably many complete one-types. The theory of a free bijection is an example: a new point is either a specified integer translate of a parameter or lies in a new orbit. It is omega-stable but not omega-categorical.
Use the first-order language with one equivalence relation . Let have exactly two equivalence classes, one countably infinite and one uncountable, with no further first-order structure. Its complete theory says that there are exactly two classes and both are infinite.
This first-order theory has quantifier elimination. To eliminate one existential logical variable from a conjunction of atomic formulas and negated atomic formulas, a logical equality either fixes its value, or finitely many inequalities exclude finitely many points. Its required equivalence-class membership is determined by the finitely many existing classes represented among the parameters. A required unused class exists exactly when fewer than two classes have already been used. Once its class is possible, infinitude supplies a point avoiding the finite exclusions. These tests are quantifier-free logical equality and equivalence conditions on the parameters. Disjunctive normal form and induction eliminate all quantifiers and also show completeness.
Thus a finite tuple's complete type is isolated by its finite equality-and-equivalence pattern. Every realized finite-tuple partial type is principal, so is atomic. In particular all individual elements have the same complete one-type, isolated by .
Choose in the countable class and in the uncountable class. Any automorphism taking to would give a bijection from their whole equivalence classes, impossible because their cardinalities differ. ThereforeIts uncountability is precisely what avoids the conclusion of (iii).
Enumerate the standard positive primes as . For each subset consider the partial typewhere divisibility is the ring logical formula .
Every finite subset is realized in : take the product of the finitely many primes required to divide , or if there are none. This is nonzero and is not divisible by any of the distinct finitely many primes required not to divide it. Compactness theorem supplies a complete type extending .
Distinct subsets yield distinct complete extensions, because at an index in their symmetric difference they require opposite divisibility statements. There are such subsets, so there are at least that many complete one-types. There are at most that many because the first-order language has only countably many logical formulas and a partial type is a set of them. HenceIn particular the number of complete one-types is uncountable, despite every partial type realized in the particular countable first-order model being a principal complete type.
Use , the complete theory of algebraically closed fields of characteristic zero. Its quantifier elimination is a standard characterization of this complete theory. Algebraically closed fields of a fixed characteristic are classified up to isomorphism by transcendence degree over their prime field.
For such a field ,when the transcendence degree is infinite, while finite transcendence degree also gives a countable field. This follows by counting rational functions in a transcendence basis and then algebraic elements over that field. Thus every first-order model of cardinality has transcendence degree , and the classification gives a unique such first-order model.
On the other hand and an algebraic closure of are countably infinite first-order models with transcendence degrees zero and one, so are not isomorphic. HenceThe transcendental complete one-type consists of for every nonzero polynomial over . Quantifier elimination makes it complete. It is nonprincipal: any parameter-free one-variable logical formula containing a transcendental element defines a cofinite set, hence contains algebraic elements as well and cannot isolate this partial type. The first-order model omits it, concretely illustrating the omitting types theorem. The existence of infinitely many algebraic complete one-types, together with this nonprincipal complete type, also agrees with the failure of the Ryll-Nardzewski finiteness condition.
Use the first-order theory of a bijection with named inverse and no finite cycles. Its axioms areEvery first-order model is a disjoint union of free two-sided integer orbits. Write for positive powers of and for powers of when is negative.
This first-order theory is complete and eliminates quantifiers. Every first-order term reduces to , and atomic logical formulas reduce to statements . To eliminate an existential logical variable in a conjunction of literals, first remove self-equalities using the no-finite-cycle axioms. If an equation fixes that logical variable as an integer translate of another logical variable, substitute that value. If no such equation remains, only finitely many points are excluded by the remaining inequalities, so some value exists in the infinite domain. Apply this to disjunctive normal form and then induct on logical formulas. The resulting parameter-free first-order sentences are decided, proving completeness.
For each fixed finite , a complete type records a partition of the logical variables into common orbits and finitely many integer offsets within each block. There are countably many possibilities. Countable first-order models with one orbit and with two orbits are not isomorphic, so the first-order theory is not -categorical.
Thus this example has the source's explicitly defined countable-type property. In fact it also satisfies ordinary omega-stability: over a countable parameter set, an element is either a specified integer translate of a parameter, giving countably many possibilities, or lies in an entirely new orbit, giving one further complete one-type. The same finite-orbit-pattern description handles finite tuples. ThereforeThe source prints the label “-stable”; the construction meets its stated definition as well as the usual stronger omega-stability condition. The difference between countably many and finitely many partial types is exactly why Ryll-Nardzewski does not yield categoricity here.
Reuse the complete free-bijection theory from part (e). Quantifier elimination shows that every one-variable atomic statement is already decided by the no-finite-cycle axioms. Thus there is exactly one complete one-type, isolated by .
For two logical variables, each integer gives a different complete type isolated byThere is also the complete typesaying that the two elements lie in different orbits. These exhaust the possibilities by quantifier elimination. In particularThe last complete type is a nonprincipal complete type. Any logical formula uses only finitely many integer offsets after quantifier elimination; a pair in a single orbit with a sufficiently different offset agrees with a different-orbit pair on those tests. Hence no single logical formula can isolate .
The one-orbit first-order model omits , while a two-orbit first-order model realizes it. This illustrates the omitting types theorem and shows concretely why finitely many complete one-types alone cannot replace the all-arities condition in Ryll-Nardzewski.
The Ryll-Nardzewski theorem says that for a complete theory in a countable first-order language with infinite first-order models, the following are equivalent: is -categorical; for every positive integer , the set of complete parameter-free -types is finite; every such finite-arity complete type is isolated by a logical formula. The countable-language hypothesis and the requirement for every finite arity are important.
The omitting types theorem says that, for a first-order consistent complete theory in a countable first-order language, a countable family of nonprincipal partial types in finite tuples of logical variables can all be omitted in a countable first-order model. Here nonprincipal means that no logical formula first-order consistent with the first-order theory implies every logical formula of the partial type. Omission means that no tuple in the constructed first-order model satisfies all logical formulas of that partial type. The complete one-type version is the special case of one partial type in one logical variable.
Theory of a free bijection 2026-10-31
The first-order theory of a bijection with named inverse and no finite cycles has first-order models consisting of disjoint integer orbits. Atomic logical formulas reduce to for integer . An existential logical variable is either fixed by such a logical equality or must avoid finitely many points. This proves quantifier elimination and completeness. There is one complete one-type; the complete two-types are the integer offsets and the nonprincipal different-orbit partial type. There are countably many finite-arity partial types but countable first-order models with different numbers of orbits are not isomorphic.