Questions: Advanced Type Theory: Omission and Realization

Question 1

A complete theory T has a type p(x) that is isolated by a formula φ(x) — meaning T ⊨ ∀x(φ(x) → p(x)) for every formula in p. What can we conclude about models of T?

• A. Some models of T can omit p, since isolation is a property of the theory, not of any particular model
• B. Every model of T must realize p, because any element satisfying φ forces realization of p
• C. No model of T needs to realize p, since p can always be omitted by the Omitting Types Theorem
• D. Models of T can realize or omit p depending on their cardinality

Answer: (B)

If p is isolated by φ, then any model of T that contains an element satisfying φ must realize p — and since T ⊨ ∃x φ(x) (isolation requires φ to be consistent with T and force p), every model of T contains such an element. Therefore p is realized in every model of T. The Omitting Types Theorem applies only to non-isolated types — types where no single formula forces their realization. Isolation is precisely the obstruction to omission.

Question 2

Why can countably many non-isolated types be simultaneously omitted in a countable model, but this approach does not directly generalize to uncountably many types?

• A. Uncountable collections of types are inherently contradictory, so no model can realize them all
• B. The Baire category theorem guarantees countable intersections of dense open sets are non-empty in the relevant space, but fails for uncountable intersections
• C. The Löwenheim-Skolem theorem only applies to countable theories, making uncountable type omission impossible
• D. Uncountable type omission requires saturated models, which exist only for stable theories

Answer: (B)

The Omitting Types Theorem for countably many types rests on a Baire category argument: each non-isolated type imposes a dense open condition on the space of Henkin constructions, and the Baire category theorem guarantees that countably many dense open sets have non-empty intersection. For uncountably many types, this argument fails — uncountable intersections of dense open sets need not be non-empty. The failure is genuine: there are theories with uncountably many non-isolated types that cannot all be simultaneously omitted in a single model.

Question 3

In a saturated model of a complete theory, every type consistent with a finite set of parameters from the model is realized by some element of the model.

• T. True
• F. False

Answer: True

This is the definition of saturation (or rather, ω-saturation for the countable case). A saturated model is maximally type-rich: it contains witnesses for every consistent type over finite parameter sets. This is the exact opposite of omitting types — rather than building a sparse model that avoids types, saturation ensures the model contains all possible types. Any two saturated models of the same cardinality are isomorphic, meaning the collection of realized types completely determines the model up to isomorphism at that cardinality.

Question 4

An isolated type can be omitted in some model of a complete theory by choosing a sufficiently simple or small model.

• T. True
• F. False

Answer: False

Isolation is an absolute obstruction to omission, not a matter of model size. If φ(x) isolates p(x), then T ⊨ ∃x φ(x), so every model of T contains an element satisfying φ — and that element must realize all of p. There is no escape: even the smallest (prime) model of T must realize every isolated type. This is why the dichotomy between isolated and non-isolated types is the fundamental divide in the Omitting Types Theorem — isolation means 'must realize in every model,' non-isolation means 'can omit in some model.'

Question 5

Explain the distinction between an isolated and a non-isolated type, and why this distinction determines whether a type can be omitted in some model of the theory.

Model answer: A type p(x) is isolated if there exists a formula φ(x) consistent with T such that T ⊨ ∀x(φ(x) → ψ(x)) for every ψ ∈ p — i.e., φ alone entails the entire type. Since T proves the existence of something satisfying φ, every model must contain a realizer of p. A non-isolated type has no such formula: no single consistent formula forces the type. In a Henkin-style model construction, isolated types are automatically realized by any element witnessing the isolating formula; non-isolated types can be avoided at each construction step by choosing witnesses that don't commit to them. The Baire category argument formalizes why this avoidance can be sustained for countably many types simultaneously.

The practical upshot is that isolation acts as a logical 'magnet' that forces types into every model. Non-isolation means the type is optional — consistent but not forced. Controlling which types appear in a model by distinguishing isolated from non-isolated types is the core technical tool of the classification theory of first-order theories, underpinning results about ω-categoricity, stability, and saturated model existence.