2Model theory
III Logic
2.4 The omitting type theorem
Definition
(Type)
.
A type is a set of formulae all with the same number of free
variables. An n-type is a set of formulae each with n free variables.
What is the motivation of this? A 1-type is a set of formulae all with one
free variable. So if we have a model
M
and an element
x ∈ M
, then we can
consider all formulae that x satisfies, and we see that this gives as a 1-type.
Definition
(Realization of type)
.
A model
M
realizes an
n
-type Σ if there
exists x
1
, · · · , x
n
∈ M such that for all σ ∈ Σ, we have
M σ(x
1
, · · · , x
n
).
Any fool can realize a type, but it takes a model theorist to omit one!
Definition
(Omit a type)
.
A model
M
omits an
n
-type Σ if for all
x
1
, · · · , x
n
,
there exists σ ∈ Σ such that
M 6 σ(x
1
, · · · , x
n
).
Example.
Consider the language of PA, and consider the type containing
σ
i
(
x
)
saying x 6= s
i
(x). We really want to omit this type!
Of course, it is not hard in this case — the standard model of PA does.
Let’s look for a condition on
T
and Σ for
T
to have a model that omits this
type.
Definition (Locally realize). We say ϕ realizes Σ locally if
T ` ∀
x
(ϕ(x) → σ(x)).
Suppose there is some ϕ ∈ L(T ) such that
T ` ∃
x
ϕ(x)
and ϕ(x) locally realizes Σ, then we certainly cannot omit Σ.
Now if
T ∀
x
¬ϕ
(
x
) whenever
ϕ
locally realizes Σ, then we have a chance.
We say T locally omits Σ. It turns out this is sufficient!
Theorem
(Omitting type theorem)
.
Let
T
be a first-order theory, and Σ an
n-type. If
T ` ∀
x
¬ϕ(x)
whenever ϕ locally realizes Σ, then T has a model omitting Σ.
We first prove a special case for propositional logic.
Theorem.
Let
T
be a propositional theory, and Σ
⊆ L
(
T
) a type (with
n
= 0).
If T locally omits Σ, then there is a T -valuation that omits Σ.
Proof.
Suppose there is no
T
-valuation omitting Σ. By the completeness theorem,
we know everything in Σ is a theorem of T . So T can’t locally omit Σ.
That was pretty trivial. But we can do something more than that — the
extended omitting types theorem. It says we can omit countably many types
simultaneously.
Theorem.
Let
T
be a propositional theory, and for each
i ∈ N
, we let Σ
i
⊆ L
(
T
)
be types for each
i ∈ N
. If
T
locally omits each Σ
i
, then there is a
T
-valuation
omitting all Σ
i
.
Proof.
We will show that whenever
T ∪ {¬A
1
, · · · , ¬A
i
}
is consistent, where
A
n
∈ Σ
n
for n ≤ i, then we can find A
n+1
∈ Σ
n+1
such that
T ∪ {¬A
1
, · · · , ¬A
n
, ¬A
n+1
}
is consistent.
Suppose we can’t do this. Then we know that
T `
^
1≤j≤n
¬A
j
→ A
n+1
,
for every
A
n+1
∈
Σ
n+1
. But by assumption,
T
locally omits Σ
i+1
. This implies
T ` ¬
^
1≤j≤n
¬A
j
,
contradicting the inductive hypothesis that T ∪ {¬A
1
, · · · , ¬A
i
} is consistent.
Thus by compactness, we know
T ∪ {¬A
1
, ¬A
2
, · · · }
is consistent, and a
model of this would give us a model of T omitting all those types.
We now prove the general case.
Proof.
Let
T
be a first order theory (in a countable language) locally omitting
Σ. For simplicity, we suppose Σ is a 1-type. We want to find a model omitting
Σ. Suppose
T
locally omits Σ, and let
{c
i
:
i ∈ N}
be a countable set of new
constant symbols. Let
hϕ
i
:
i ∈ Ni
be an enumeration of the sentences of
L
(
T
).
We will construct an increasing sequence
{T
i
:
i ∈ N}
of finite extensions of
T
such that for each m ∈ N,
(0) T
m+1
is consistent.
(i) T
m+1
decides ϕ
n
for n ≤ m, i.e. T
m+1
` ϕ
n
or T
m+1
` ¬ϕ
n
.
(ii)
If
ϕ
m
is
∃
x
ψ
(
x
) and
ϕ
m
∈ T
m+1
, then
ψ
(
c
p
)
∈ T
m+1
, where
c
p
is the first
constant not occurring in T
m
or ϕ
m
.
(iii) There is a formula σ(x) ∈ Σ such that ¬σ(c
m
) ∈ T
m+1
.
We will construct this sequence by recursion. Given
T
m
, we construct
T
m+1
as
follows: think of T
m
as T ∪ {θ
1
, · · · , θ
r
}, and let
Θ =
^
j≤r
θ
j
.
We let {c
1
, · · · , c
N
} be the constants that have appeared in Θ, and let
Θ(x)
be the result of replacing
c
i
with
x
i
in
θ
. Then clearly, Θ(
x
) is consistent with
T . Since T locally omits Σ, we know there exists some σ(x) ∈ Σ such that
Θ ∧ ¬σ(x
m
)
is consistent with T . We put ¬σ(c
m
) into T
m+1
, and this takes care of (iii).
If
ϕ
m
is consistent with
T
m
∪ {¬σ
(
c
m
)
}
, then put it into
T
m+1
. Otherwise,
put in ¬ϕ
m
. This takes care of (i).
If
ϕ
m
is
∃
x
ψ
(
x
) and it’s consistent with
T
m
∪ {¬σ
(
c
m
)
}
, we put
ψ
(
c
m
) into
T
m+1
. This takes care of (ii).
Now consider
T
∗
=
[
n∈N
T
n
Then T
∗
is complete by construction, and is complete by compactness.
Consider an arbitrary countable model of
T
∗
, and the submodel generated
by the constants in
C
. This is a model of
T
∗
⊇ T
and condition (iii) ensures
that it omits Σ.