Elementary extension

An elementary extension is an extension preserving all first-order truth with parameters, hence giving elementary equivalence. An extension $N\supseteq M$ is elementary when every formula with parameters from $M$ has the same truth value in both structures.

A model $N$ is $\kappa$-saturated when every complete type over a subset of size less than $\kappa$ is realized in $N$.

A model is omega-saturated when it realizes every complete finite-tuple type over any finite parameter set. Realizing all one-variable types over finite parameter sets suffices by successively adjoining coordinates. This is weaker than saturation over every countable parameter set.

Let $M$ be a countable omega-saturated model and $D\subseteq M$ finite. Then $D$ 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 $a\in D$, if no formula in $\mathrm{tp}(a)$ has its realization set contained in $D$, the partial type $\mathrm{tp}(a)\cup \{x\ne d:d\in D\}$ is finitely satisfiable. Its parameters form a finite set, so saturation realizes it outside $D$, contradicting invariance. Choose a defining neighbourhood for each $a\in D$ and take their finite disjunction. The empty set is defined by $x\ne x$. Setwise invariance permits automorphisms to permute points within $D$.

For every infinite regular cardinal $\kappa$, every first-order structure has a $\kappa$-saturated elementary extension. At one stage use the compactness theorem with the elementary diagram to realize all complete types over subsets of the stage having size less than $\kappa$. There is a set of such types; finite subsets of the enlarged theory are satisfiable because their finitely many witnesses are independent. Iterate for $\kappa$ stages, taking elementary unions at limits. Regularity puts any parameter set of size less than $\kappa$ inside one stage, and its type is realized at the next one. Passing to a larger regular cardinal covers singular requested degrees of saturation as well.

In a countable language, an ultraproduct over a nonprincipal ultrafilter on $\omega$ realizes every countable finitely satisfiable type, including types over countably many parameters. Enumerate the type ${\phi }_1,{\phi }_2,\dots$, and let $A_n$ be the ultrafilter-large set of coordinates where the first $n$ first-order formulas have a simultaneous witness. Put $B_n=\{i:i\ge n\}\cap {\bigcap }_{j\le n}{A}_j$. At coordinate $i$, choose a witness for the largest $n\le i$ with $i\in B_n$, or an arbitrary element when there is none. For each fixed $n$, the resulting function satisfies the first $n$ first-order formulas on $B_n$. The Łoś theorem then realizes the entire type. Countability of the language and parameter set makes the enumeration possible.

A $\kappa$-saturated model has the one-point extension property for partial elementary maps of size below $\kappa$: transport the type of the new element through the map and realize it by saturation. This is $\kappa$-homogeneity; back-and-forth gives the corresponding automorphisms when cardinalities permit.

If an aleph-zero-homogeneous model realizes every finite type over the empty set, it is aleph-zero-saturated. Realize the joint empty-set type of the parameters and a desired element, then use homogeneity to move the realized parameter tuple to the given one.

A model $N$ of cardinality $\kappa$ is universal when every model of the same complete theory having cardinality less than $\kappa$ admits an elementary embedding into $N$.

A model $N$ of cardinality $\kappa$ is homogeneous when every partial elementary map between subsets of size less than $\kappa$ extends to an automorphism of $N$.

A first-order structure has finite-tuple homogeneity when any two finite tuples of the same parameter-free complete type are related by an automorphism. For countably infinite first-order structures this agrees with extension of finite partial elementary maps to automorphisms. Countable atomic models have this property by a back-and-forth method using isolating logical formulas. Uncountable atomic models can fail it.

A universal homogeneous model realizes every type over a small parameter set. Embed a small model containing a realization into the universal model, then use homogeneity to move the embedded parameters back to the original ones.

Let $N$ be uncountable and saturated, and let a formula define an equivalence relation. If every small elementary submodel of $N$ meets every class, then there are only finitely many classes. Otherwise a small elementary submodel $M$ yields the finitely satisfiable type $\{\neg E(x,m):m\in M\}$, contradicting saturation.

The union of an elementary chain of structures has a unique induced structure, and every member of the chain is an elementary substructure of the union.

A directed system of first-order structures and coherent elementary embeddings has a direct limit into which every member embeds elementarily. Represent an element by a pair consisting of a stage and an element at that stage; identify two representatives when their images agree at a common later stage. Interpret functions and relations at a common stage. Mathematical induction on first-order formulas proves elementarity: for an existential first-order formula true at the limit, its witness and parameters occur at a common stage, and elementarity pulls truth back to the stage containing the original parameters. This generalizes the elementary chain theorem beyond linearly ordered diagrams.

The complete type of a tuple over parameters records every formula over those parameters that the tuple satisfies.

A complete two-type is a complete type in two free variables. Such a partial type describes both individual properties and relations between a pair of elements.

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.

A nonprincipal complete type has no first-order consistent first-order formula implying all its members. In a complete countable first-order theory such a partial type can be omitted in a countable first-order model by the omitting types theorem. A partial type realized by a parameter-free definable tuple is principal.

A complete type is algebraic when it contains a formula having finitely many realizations in a model of the theory. A one-element example is the type containing $x=c$ for a named constant. Such a type cannot gain infinitely many realizations in an elementarily equivalent structure. An isolated type need not be algebraic: the unique empty-set one-type in a dense linear order without endpoints is isolated by $x=x$ and has infinitely many realizations.

With its standard topology, this type space is a Stone space. The type space $S_n^M(A)$ is the set of complete $n$-types over a parameter set $A$ that are consistent with the complete theory of $M$ together with its diagram over $A$.

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.

For each irrational real cut $r$, 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.

For a type space $S_n^M(A)$, the basic open set $[\phi ]$ consists of complete types containing the formula $\phi$. These sets are clopen, satisfy $[\phi ]\cap [\psi ]=[\phi \wedge \psi ]$, and distinguish distinct types. The compactness theorem makes this topology compact; it is Hausdorff and has a basis of clopen sets.

A complete type $p\in S_n(A)$ is isolated when some formula $\phi \in p$ belongs to no other complete type in $S_n(A)$. Equivalently, the basic open set determined by $\phi$ is the singleton $\{p\}$.

A principal complete type is isolated by one first-order consistent first-order formula: modulo the first-order theory, that logical formula implies every member of the partial type. For complete types this is exactly an isolated type. The qualifier complete distinguishes this notion from partial types.

If a complete countable theory has a prime model, isolated types are dense in every finite-arity type space. Every nonempty basic open set is realized in the prime model, whose finite tuples have isolated types.

A type $p(x_1,\dots ,x_n)$ is omitted in a structure $M$ when no tuple from $M^n$ realizes every formula in $p$.

Let $T$ be a consistent theory in a countable first-order language. For every countable family of nonisolated finite-arity types of $T$, there is a countable model of $T$ that omits every type in the family.

Let $p(\mathbf{x})$ be a nonprincipal partial type over a consistent first-order theory $T$. Suppose $T\cup \{\sigma (\mathbf{c})\}$ is consistent, with $\sigma$ a finite condition in finitely many new constants, and let $\mathbf{t}(\mathbf{c})$ be a tuple of closed terms. Some $\psi \in p$ leaves $T\cup \{\sigma (\mathbf{c}),\neg \psi (\mathbf{t}(\mathbf{c}))\}$ consistent. Otherwise the original-language first-order formulais consistent with $T$ and entails every member of $p$, contradicting nonprincipality. Replace all new constants occurring in the condition or terms by variables. This lemma makes the omission requirements dense in a countable Henkin construction.

Every complete type over parameters from $M$ is realized in some elementary extension of $M$. Apply compactness to the elementary diagram of $M$ together with a new tuple of constants satisfying the type.

Distinct complete types contain opposite choices $\phi$ and $\neg \phi$. The corresponding basic clopen sets partition the type space, so every type space is totally disconnected.

Quantifier elimination for dense linear orders shows that the one-types over $\mathbb{N}\subset \mathbb{Q}$ are determined by cuts: equality to a natural number, one of the intervals between consecutive natural numbers, the ray below zero, or the cut above every natural number. Only the last type is non-isolated.

A model is aleph-zero-homogeneous when every finite partial elementary map extends by one more element.