502 – Notes on compactness

October 1, 2009

The goal of this note is to present a proof of the following fundamental result. A theory {T} is said to be satisfiable iff there is a model of {T.}

Theorem 1 (Compactness) Let {T} be a first order theory. Suppose that any finite subtheory {T_0\subseteq T} is satisfiable. Then {T} itself is satisfiable.

As indicated on the set of notes on the completeness theorem, compactness is an immediate consequence of completeness. Here I want to explain a purely semantic proof, that does not rely on the notion of proof.

The argument I present uses the notion of ultraproducts. Although their origin is in model theory, ultraproducts have become an essential tool in modern set theory, so it seems a good idea to present them here. We will require the axiom of choice, in the form of Zorn’s lemma.

The notion of ultraproduct is a bit difficult to absorb the first time one encounters it. I recommend working out through some examples in order to understand it well. Here I confine myself to the minimum necessary to make sense of the argument.

Read the rest of this entry »


580 -Cardinal arithmetic (9)

March 7, 2009

2. The ultrapower construction

The study of ultrapowers originates in model theory, although it has found applications both in algebra and in analysis. However, it is accurate to say that it is mainly exploited in set theory. Here I present the basic idea, showing its close connection to the study of measurable cardinals, defined last lecture.

Suppose first that {{\mathcal U}} is an ultrafilter over a set {X.} We want to define the ultrapower of the universe {V} of sets by {{\mathcal U}.} The basic idea is to consider the product of {X} many copies of the structure {(V,\in).} We want to “amalgamate” them somehow into a new structure {(\tilde V,\tilde\in).} For this, we look for the “typical” properties of the elements {\{f(x): x\in X\}} of each “thread” {f:X\rightarrow V,} and add an element {\tilde f} to {\tilde V} whose properties in {(\tilde V,\tilde\in)} are precisely these typical properties. We use {{\mathcal U}} to make this precise, by saying that a property {\varphi} is typical of the range of {f} iff {\{x\in X:\varphi(f(x))\}\in{\mathcal U}.} This leads us to the following definition, due to Dana Scott, that adapts the ultrapower construction to the context of proper classes:

Definition 1 Let {{\mathcal U}} be an ultrafilter over a nonempty set {X.} We define the ultrapower {(V^X/{\mathcal U},\hat\in)} of {V} by {{\mathcal U}} as follows:

For {f,g:X\rightarrow V,} say that

\displaystyle f=_{\mathcal U} g \mbox{ iff } \{x \in X: f(x)=g(x)\} \in{\mathcal U}.

This is easily seen to be an equivalence relation. We would like to make the elements of {V^X/{\mathcal U}} to be the equivalence classes of this relation. Unfortunately, these are all proper classes except for the trivial case when {X} is a singleton, so we cannot within the context of our formal theory form the collection of all equivalence classes.

Scott’s trick solves this problem by replacing the class of {f} with

\displaystyle [f]:= \{g : X\rightarrow V : g=_{\mathcal U}f \mbox{ and } {\rm rk}(g)\mbox{ is least possible}\}.

Here, as usual, {{\rm rk}(g) = {\rm min}\{\alpha : g\in V_{\alpha+1}\} = \sup\{ {\rm rk}(x) +1 : x\in g\}.} All the “classes” {[f]} are now sets, and we set {V^X/{\mathcal U} = \{[f] :  f:X\rightarrow V\}.}

We define {\hat\in} by saying that for {f,g:X\rightarrow V} we have

\displaystyle [f]\hat\in[g] \mbox{ iff } \{x \in X : f(x)\in g(x)\} \in {\mathcal U}.

(It is easy to see that {\hat\in} is indeed well defined, i.e., if {f=_{\mathcal U}f'} and {g=_{\mathcal U}g'} then {\{x\in X : f(x)\in g(x)\} \in {\mathcal U}} iff {\{x\in X : f'(x)\in g'(x)\} \in {\mathcal U}.})

(The ultrapower construction is more general than as just defined; what I have presented is the particular case of interest to us.) The remarkable observation, due to \mbox{\L o\'s,} is that this definition indeed captures the typical properties of each thread in the sense described above:

Read the rest of this entry »