6.2 Types and Realizations

Types give a precise way to describe all first order properties that an element, or a tuple of elements, may satisfy in a structure. Instead of looking at one formula at a time, a type collects many formulas together and treats them as a possible description of an element. This is useful because model theory often studies not only the elements already present in a structure, but also the kinds of elements that could exist in a larger structure.

Let $L$ be a first order language, let $\mathcal M$ be an $L$-structure with domain $M$, and let $A \subseteq M$ be a set of parameters. We write $L(A)$ for the language obtained from $L$ by adding a constant symbol for each element of $A$. In practice, a formula over $A$ is a formula allowed to use elements of $A$ as parameters.

Partial Types

A partial type is a set of formulas that is intended to describe a possible element or tuple.

Definition 6.30 (Partial Type)

Let $A \subseteq M$, and let $x$ be a tuple of variables:

A partial $n$-type over $A$ is a set $p(x)$ of $L(A)$-formulas whose free variables are among $x$.

Thus:

where each $\varphi_i(x)$ is a formula with parameters from $A$.

A partial type should be read as a collection of conditions that an element or tuple is expected to satisfy at the same time. For example, if $x$ is one variable, then:

describes an element greater than every element of $A$, if such an element exists in the relevant structure.

Realization

A type is realized when some tuple in a structure satisfies all formulas in the type.

Definition 6.31 (Realization)

Let $p(x)$ be a partial type over $A$, and let $\mathcal N$ be an $L$-structure containing $\mathcal M$ or at least containing interpretations of the parameters from $A$.

A tuple $b \in N^n$ realizes $p(x)$ in $\mathcal N$ if:

for every formula $\varphi(x) \in p(x)$.

In this case, we write:

or:

If no tuple in $\mathcal N$ realizes $p(x)$, then we say that $p(x)$ is omitted in $\mathcal N$.

Example 6.32

Let:

and consider the partial type over $\mathbb Q$:

This type says that $x$ is greater than every rational number.

There is no rational number satisfying all formulas in $p(x)$, so $p(x)$ is omitted in $\mathcal Q$.

However, if we pass to a larger ordered field containing an element larger than every rational number, then this type can be realized there. Such an element is called infinitely large relative to $\mathbb Q$.

Example 6.33

In:

consider:

This type says that $x$ is positive and smaller than every positive rational number $1/n$.

No real number realizes this type, because every positive real number is larger than $1/n$ for some sufficiently large $n$.

In a nonstandard extension of the real numbers, such a type may be realized by a positive infinitesimal element.

Finite Satisfiability

A partial type may have infinitely many formulas, so we need a way to test whether its requirements are at least finitely compatible.

Definition 6.34 (Finite Satisfiability)

Let $p(x)$ be a partial type over $A$. We say that $p(x)$ is finitely satisfiable in $\mathcal M$ if every finite subset:

is realized in $\mathcal M$.

Equivalently, for every finite collection:

there exists $a \in M^n$ such that:

Finite satisfiability means that no finite part of the type is contradictory inside the structure. The whole type may still fail to be realized in that structure.

Example 6.35

In:

consider:

This type is finitely satisfiable in $\mathbb N$. Indeed, given finitely many requirements:

choose:

Then $m$ satisfies all formulas in that finite subset.

However, no natural number realizes the whole type, because no natural number is greater than every natural number.

Lemma 6.36 (Realization Implies Finite Satisfiability)

If a partial type $p(x)$ is realized in $\mathcal M$, then $p(x)$ is finitely satisfiable in $\mathcal M$.

Proof

Suppose $a \in M^n$ realizes $p(x)$ in $\mathcal M$.

Then for every formula $\varphi(x) \in p(x)$, we have:

Let $p_0(x)$ be a finite subset of $p(x)$. Since $a$ satisfies every formula in $p(x)$, it satisfies every formula in $p_0(x)$.

Therefore:

Hence every finite subset of $p(x)$ is realized in $\mathcal M$, so $p(x)$ is finitely satisfiable in $\mathcal M$.

Consistency of Types

A partial type is consistent if its formulas can be realized in some structure extending the relevant theory. This notion connects types with compactness.

Definition 6.37 (Consistent Type)

Let $T$ be an $L$-theory, and let $p(x)$ be a set of $L(A)$-formulas. We say that $p(x)$ is consistent with $T$ if:

has a model.

More explicitly, this means that there is a structure $\mathcal N \models T$ and a tuple $b \in N^n$ such that:

for every $\varphi(x) \in p(x)$.

Lemma 6.38 (Compactness for Types)

Let $T$ be an $L$-theory, and let $p(x)$ be a set of $L$-formulas. Then $p(x)$ is consistent with $T$ if and only if every finite subset of $p(x)$ is consistent with $T$.

Proof

If $p(x)$ is consistent with $T$, then there is a model $\mathcal N \models T$ and a tuple $b$ such that $b$ satisfies every formula in $p(x)$. Then $b$ also satisfies every finite subset of $p(x)$, so every finite subset is consistent with $T$.

Conversely, suppose every finite subset of $p(x)$ is consistent with $T$. Introduce new constant symbols:

corresponding to the variables:

For each formula $\varphi(x) \in p(x)$, form the sentence:

Consider the theory:

Every finite subset of this theory is satisfiable by assumption, because it only mentions finitely many formulas from $p(x)$. By the compactness theorem, the whole theory has a model $\mathcal N$.

In that model, the tuple interpreting the constants $c_1,\dots,c_n$ satisfies every formula in $p(x)$. Therefore $p(x)$ is consistent with $T$.

Complete Types

A complete type gives a maximal consistent description. It decides every formula or its negation.

Definition 6.39 (Complete Type)

Let $T$ be an $L$-theory, and let $p(x)$ be a set of $L(A)$-formulas. We say that $p(x)$ is a complete type over $A$ with respect to $T$ if:

1. $p(x)$ is consistent with $T$.

2. For every $L(A)$-formula $\varphi(x)$, exactly one of the following belongs to $p(x)$:

   $$\varphi(x)$$

   or:

   $$¬\varphi(x).$$

Thus a complete type gives a complete truth profile for the tuple $x$ over the parameter set $A$.

Example 6.40

Let:

For an element $a \in \mathbb Q$, the complete type of $a$ over the empty set includes all formulas without parameters that are true of $a$.

In the pure dense order without endpoints, all rational numbers have the same complete type over the empty set. This is because the language has no constants naming particular rational numbers, and the order structure alone cannot distinguish one rational from another without parameters.

However, over the parameter set:

the type of $a$ contains the formula:

so it uniquely determines $a$.

Type of a Tuple

Every tuple in a structure determines a complete type by collecting all formulas true of it.

Definition 6.41 (Type of a Tuple)

Let $\mathcal M$ be an $L$-structure, let $A \subseteq M$, and let $b \in M^n$. The complete type of $b$ over $A$ in $\mathcal M$ is:

When the structure is clear, we write:

This set records every first order property of $b$ that can be expressed using parameters from $A$.

Lemma 6.42 (Tuple Types Are Complete)

Let $\mathcal M$ be an $L$-structure, let $A \subseteq M$, and let $b \in M^n$. Then:

is a complete type over $A$.

Proof

By definition:

First, this type is consistent, because it is realized by $b$ in $\mathcal M$.

Second, let $\varphi(x)$ be any $L(A)$-formula. Since classical first order semantics is two valued, exactly one of the following holds:

or:

Therefore exactly one of:

belongs to $\operatorname{tp}^{\mathcal M}(b/A)$.

Hence $\operatorname{tp}^{\mathcal M}(b/A)$ is complete.

Type Spaces

The set of all complete types over a parameter set is called a type space.

Definition 6.43 (Type Space)

Let $T$ be an $L$-theory and let $A$ be a set of parameters. The set of all complete $n$-types over $A$ consistent with $T$ is denoted:

or, when the theory must be specified:

An element of $S_n(A)$ is a complete description, over $A$, of a possible $n$-tuple in a model of the theory.

When $A=\emptyset$, we write:

for the complete $n$-types over the empty set.

Realized and Omitted Types

Some complete types over $A$ are realized in a given structure, while others are only consistent and become realized in larger structures.

Definition 6.44 (Realized Type)

Let $\mathcal M$ be an $L$-structure and let $A \subseteq M$. A type $p(x) \in S_n(A)$ is realized in $\mathcal M$ if there is a tuple $b \in M^n$ such that:

If no such tuple exists in $\mathcal M$, then $p(x)$ is omitted in $\mathcal M$.

Example 6.45

In:

the partial type:

is finitely satisfiable but omitted.

This means that every finite fragment can be satisfied by choosing a sufficiently large natural number, but the whole type requires an element larger than every natural number, which does not exist in $\mathbb N$.

A larger elementary extension may contain such an element, and in that extension the type is realized.

Lemma 6.46 (Every Consistent Type Is Realized Somewhere)

Let $T$ be an $L$-theory, and let $p(x)$ be a type consistent with $T$. Then there is a model $\mathcal N \models T$ and a tuple $b \in N^n$ such that $b$ realizes $p(x)$.

Proof

Since $p(x)$ is consistent with $T$, by definition:

has a model after the variables $x$ are interpreted by some tuple.

Equivalently, introduce constants:

and consider:

Because $p(x)$ is consistent with $T$, this set of sentences has a model $\mathcal N$. Let $b_i$ be the interpretation of $c_i$ in $\mathcal N$, and put:

Then for every $\varphi(x) \in p(x)$:

Thus $b$ realizes $p(x)$ in $\mathcal N$.

Principal Types

Some types are determined by a single formula. These are called principal types.

Definition 6.47 (Principal Type)

Let $p(x)$ be a complete type over $A$. We say that $p(x)$ is principal if there is a formula $\varphi(x) \in p(x)$ such that, for every formula $\psi(x) \in p(x)$:

In this case, $\varphi(x)$ is said to isolate $p(x)$.

A principal type is therefore controlled by one formula. Once an element satisfies that formula, it must satisfy every formula in the type.

Example 6.48

Let $A$ contain an element $a$ of a structure $\mathcal M$. The type of $a$ over $A$ is principal, because it is isolated by:

Indeed, any element satisfying $x=a$ must satisfy exactly the same formulas over $A$ that $a$ satisfies.

Thus:

is isolated by $x=a$.

Nonprincipal Types

A type may be consistent without being isolated by any single formula.

Example 6.49

In:

the type:

is nonprincipal over $\mathbb N$.

No single formula $x>n$ captures the whole type, because satisfying $x>n$ only guarantees being larger than that particular $n$, not larger than every natural number.

The type is instead described by an infinite collection of conditions.

Complete Types and Maximal Consistency

Complete types can also be described as maximal consistent sets of formulas.

Lemma 6.50 (Complete Types Are Maximal Consistent)

Let $p(x)$ be a complete type over $A$. Then $p(x)$ is maximal among consistent sets of formulas over $A$. That is, if $q(x)$ is consistent and:

then:

Proof

Suppose $p(x)$ is complete and $q(x)$ is consistent with:

Assume for contradiction that:

Then there is a formula:

such that:

Since $p(x)$ is complete, exactly one of $\varphi(x)$ and $¬\varphi(x)$ belongs to $p(x)$. Since $\varphi(x)$ does not belong to $p(x)$, we must have:

Because $p(x) \subseteq q(x)$, it follows that:

Thus $q(x)$ contains both:

and:

This contradicts the consistency of $q(x)$.

Therefore no such $\varphi(x)$ exists, and:

Lemma 6.51 (Maximal Consistent Sets Are Complete)

Let $p(x)$ be a maximal consistent set of formulas over $A$. Then $p(x)$ is a complete type over $A`.

Proof

We must show that for every formula $\varphi(x)$, exactly one of:

belongs to $p(x)$.

First, $p(x)$ cannot contain both $\varphi(x)$ and $¬\varphi(x)$, since that would make it inconsistent.

Now suppose neither $\varphi(x)$ nor $¬\varphi(x)$ belongs to $p(x)$.

If:

is consistent, then this would be a consistent proper extension of $p(x)$, contradicting maximality.

Thus:

is inconsistent.

Similarly, if:

is consistent, it would be a consistent proper extension of $p(x)$, again contradicting maximality.

So both:

and:

would be inconsistent.

But this is impossible. If both extensions are inconsistent, then $p(x)$ would imply both $¬\varphi(x)$ and $\varphi(x)$ in the semantic sense, forcing inconsistency of $p(x)$ itself.

Therefore one of $\varphi(x)$ or $¬\varphi(x)$ must belong to $p(x)$.

Hence $p(x)$ is complete.

Types Over Models

Types over models are especially important because parameters from a model allow formulas to describe the position of a possible element relative to the model.

Let $\mathcal M$ be a model and let:

A realization of $p(x)$ may lie inside $\mathcal M$, but it may also lie in a larger structure $\mathcal N$ extending $\mathcal M$.

If $b \in N^n$ realizes $p(x)$, then $p(x)$ records exactly how $b$ relates to all definable sets over $M$.

For example, in an ordered structure, the type of a new element over $M$ records, for every parameter $a \in M$, whether:

In richer languages, the type records much more than order position, because it includes all formulas with parameters from $M`.

Types and Definable Sets

Types can be viewed as choices of sides with respect to definable sets.

If $D \subseteq M^n$ is definable over $A$ by a formula $\varphi(x)$, then a complete type $p(x)$ over $A$ decides whether a realization should lie in $D$ or outside $D$.

More precisely, since $p(x)$ is complete, exactly one of:

or:

belongs to $p(x)$.

Thus a complete type over $A$ selects, for every $A$-definable set, whether the tuple lies inside that set or in its complement.