Exploration 2: Types

November 3, 2023.

The goal of this exploration is to show how properties are expressed in model theory, and how we can derive the compactness theorem using such properties.

Currently we consider models to be some unordered jumble of elements that give meaning to constants, functions, and relations in a language $L$ .

But sometimes it’s useful to talk about a specific subset of those elements. For instance, if we have a model of the theory of integers, we might want to single out the elements of the model that signify prime integers.

Typically we do this by defining some formulas that fully describe said elements. In the prime number example, we might have $\phi(p)\equiv\lnot\exists x y\ldotp x\ge 2\land y\ge 2\land x\times y=p$ “a number is prime if there is no product of two integers $\ge 2$ equal to it”. Then every element $a$ in our model that satisfies $\phi(p)$ are the prime numbers.

In general, given $A\models T$ we can write a set of formulas $tp_A(\bar{x})$ consistent with the given theory $T$ , called a type over $T$ . This type singles out some subset of elements $\bar{a}\subseteq A$ by saying that $\bar{a}$ realizes $tp_A$ .

Recall that theories are made up of sentences, which are formulas without parameters. Intuitively, a type over $T$ is a parameterized theory, with the additional condition that it must be consistent with some existing theory $T$ (in the above case, the theory of integers). Types can also be unparameterized (if the set of parameters is empty) but typically they are parameterized.

In this section, we show how to compare two types.

Every element of a model has its own type. If we consider a single element $a$ of a model $A$ of some theory $T$ , we can define the type of $a$ over $T$ as every formula $\phi(x)$ (with one free variable $x$ ) where $\phi(a)$ is true in $A$ . This type is guaranteed to include $a$ , so every element of a model has its own type $tp(a)$ .

Sometimes a type is a superset of another type. For example, anything that is true about the set of prime numbers is true about the prime integer $5$ in particular. That means the set of formulas true about the integer $5$ , $tp(5)$ , contains the set of formulas true about the prime numbers, $tp_{prime}$ . We say $tp(5)$ is stronger than $tp_{prime}$ , or $tp_{prime}$ is weaker than $tp(5)$ , because $tp_{prime}\subseteq tp(5)$ . So we have a partial ordering of types based on inclusion.

By definition of $tp(5)$ , there aren’t any more formulas true about $5$ that aren’t already in $tp(5)$ . Much like theories can be complete (having $\phi$ or $\lnot\phi$ for every sentence $\phi$ in the language), $tp(5)$ is a complete type (having $\phi(\bar{x})$ or $\lnot\phi(\bar{x})$ for every formula $\phi(\bar{x})$ in the language). Complete types are by definition the strongest types. We can’t add any more formulas $\phi(\bar{x})$ to it without making it inconsistent with the given theory.

In this section, we define the model of a theory by its strongest types.

Now let’s model the theory of integers with this concept of strongest types (complete types).

Getting the strongest types

The first step is to find all of the strongest types. Let’s start from an example type, like $tp_{prime}$ , which encodes all facts about the prime numbers. Given such a type, we’d like to get all types stronger than it, such as $tp(5)$ . Define a set containing $tp_{prime}$ as well as every type stronger than $tp_{prime}$ . We call this set a principal filter over $tp$ . In our case, the principal filter on $tp_{prime}$ includes $tp_{prime}$ , $tp(5)$ , $tp(3)$ , in fact all the $tp(\text{prime number})$ , and in fact every type that singles out any subset of the prime numbers.

The principal filter on complete types like $tp(5)$ contains only itself, $\{tp(5)\}$ . When a non-empty filter, like $\{tp(5)\}$ , can’t be extended with additional stronger types without making two types inconsistent with each other, we call it an ultrafilter, meaning it’s a filter that already contains all the strongest types.

We care about ultrafilters because while a filter might contain types that conflict (are inconsistent with each other), an ultrafilter necessarily cannot have conflicting types. By taking all the ultrafilters of the theory, we essentially have access to all the strongest types that don’t conflict with each other.

Showing that there is an ultrafilter for every filter

Since the set of all types is typically infinite, to take all the ultrafilters in the space of types requires applying the Axiom of Choice (in the form of Zorn’s Lemma).

To this end we prove the Ultrafilter lemma: every filter $F$ is contained in some ultrafilter. Proof:

Form a partial ordering $M$ of filters that contain $F$ .
Zorn’s lemma: $M$ has a maximal element (= our ultrafilter) if we can prove that every non-empty chain in $M$ has an upper bound in $M$ .
Take an arbitrary non-empty chain in $M$ .
Every union of a chain of filters is a filter. So take the union of this chain to get a filter $U$ . $U$ contains every filter in the chain, and therefore is an upper bound of this chain.
To show $U$ is in $M$ , we just need to show that $U$ contains $F$ , since every filter containing $F$ is in $M$ . But $U$ is the union of some filters from $M$ that contain $F$ by definition, which means $U$ contains $F$ too.
By Zorn’s Lemma, there is a maximal filter in $M$ , the ultrafilter containing $F$ .

This lemma shows that we can extend any filter to an ultrafilter.

Getting every ultrafilter via finite subsets of the theory

Next, we require that every finite subset of $T$ to have a model. Sound familiar? It’s the same requirement as the Compactness Theorem, which we are essentially proving by constructing a model of an arbitrary theory.

Now create a filter $F$ containing each finite subset of $T$ as a type. Extend this filter with every type that is stronger than some type already in $F$ , so that the resulting filter $F^+$ contains all the strongest types (complete types) consistent with $T$ . This might add types that are inconsistent with each other, so we use the Ultrafilter lemma to take the ultrafilter $U$ of $F^+$ to ensure that all types within $U$ agree on every formula $\phi$ in the language.

Defining a model via an ultrafilter of types

Then, every complete 1-type (single-parameter type) $p(x)$ in the ultrafilter $U$ defines some element $a_p$ in our model $A$ , so that $a_p$ realizes $p(x)$ in our model.

Since our domain are elements that correspond to a type, we can identify every term in the language with a type in order to construct our model. In particular, we identify every term $t$ with the complete 1-type in $U$ containing $\phi(x)\equiv x=t$ . The ultrafilter $U$ ensures that we can’t have two complete 1-types that disagree on what element $t$ is equal to, so this is well-defined.

This gives an interpretation to all the constant symbols (when $t$ is some constant $c$ ) and implicitly requires us to lift all the function symbols to operate on our elements $a_p$ . This is well-defined, because our complete types in $U$ define the outcome of every possible $f(\bar{x})$ via formulas like $\phi(y)\equiv y=f(\bar{x})$ . We lift all the relation symbols similarly.

Because this construction is based on complete types consistent with $T$ , the resulting elements $a_p$ are defined so that every sentence in $T$ is true.

In the end we have essentially proved the compactness theorem again — we constructed a model for $T$ directly by treating finite subsets of $T$ as types.

< Back to category Exploration 2: Types (permalink)
Exploration 1: The canonical model of a theory Exploration 3: Homomorphism preservation theorems