Complete L_{ω₁ω}-types and their isolation

The complete L_{ω₁ω}-type of a tuple a : Fin n → M is the set of L_{ω₁ω} formulas with n bound positions and no free variables that hold of a in M. The realized types of M at arity n are the complete types of its n-tuples. A complete type contains, for every formula, either the formula or its negation, so one complete type can lie inside another only when the two are equal.

Isomorphic structures realize the same complete types. At arity 0 the only realized type is the L_{ω₁ω} theory of the structure, so two structures satisfy the same L_{ω₁ω} sentences exactly when they realize the same complete types at arity 0.

The main result is the isolation of realized types. If M realizes only countably many complete n-types, then each realized type p is isolated among them by one formula: for every other realized type q, pick a formula of p outside q; the countable conjunction of these choices holds of a tuple b of M exactly when the type of b is p. No fragment, no countability of the language and no relational hypothesis is involved. Isolating formulas are the basic tool for analysing structures that realize countably many types.

Main definitions

• FirstOrder.Language.infinitaryType: the complete L_{ω₁ω}-type of a tuple.
• FirstOrder.Language.realizedTypes: the complete types realized in a structure at an arity.

Main results

• FirstOrder.Language.infinitaryType_subset_iff: a complete type lies inside another only when the two are equal.
• FirstOrder.Language.StrongHomClass.infinitaryType_comp and FirstOrder.Language.StrongHomClass.realizedTypes_eq: isomorphisms preserve complete types and realized types.
• FirstOrder.Language.omitsType_iff_forall_mem_realizedTypes_not_subset: a structure omits a partial type exactly when no realized type contains it.
• TauCeti.infEquivAt_nat_iff_realizedTypes_zero_eq: two structures satisfy the same L_{ω₁ω} sentences exactly when they realize the same complete types at arity 0.
• TauCeti.SameAtomicType.infinitaryType_eq_of_isExtensionPair: between relational structures forming extension pairs in both directions, such as nonempty dense linear orders without endpoints, tuples of the same atomic type have the same complete type.
• FirstOrder.Language.exists_isolatingFormula: if a structure realizes countably many complete n-types, each realized type is isolated among them by a single formula.

References

• D. Marker, Lectures on Infinitary Model Theory, Cambridge University Press, 2016, for complete L_{ω₁ω}-types and structures realizing countably many of them.
• The shape of infinitaryType and realizedTypes follows Mathlib's first-order FirstOrder.Language.Theory.typeOf and FirstOrder.Language.Theory.realizedTypes (Mathlib/ModelTheory/Types.lean).

def FirstOrder.Language.infinitaryType {L : Language} (M : Type w) [L.Structure M] {n : ℕ} (a : Fin n → M) : Set (L.BoundedFormulaω Empty n)

The complete L_{ω₁ω}-type of a tuple a : Fin n → M: the formulas with n bound positions and no free variables that hold of a in M.

@[simp]

theorem FirstOrder.Language.mem_infinitaryType {L : Language} {M : Type w} [L.Structure M] {n : ℕ} {a : Fin n → M} {φ : L.BoundedFormulaω Empty n} : φ ∈ infinitaryType M a ↔ BoundedFormulaInf.Realize φ Empty.elim a

A formula belongs to the complete type of a tuple exactly when it holds of the tuple.

theorem FirstOrder.Language.infinitaryType_subset_iff {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n : ℕ} {a : Fin n → M} {b : Fin n → N} : infinitaryType M a ⊆ infinitaryType N b ↔ infinitaryType M a = infinitaryType N b

Complete types are maximal. The complete type of a tuple lies inside the complete type of another tuple, possibly in another structure, only when the two types are equal: a formula of the larger type missing from the smaller one would put its negation in the smaller one.

def FirstOrder.Language.realizedTypes {L : Language} (M : Type w) [L.Structure M] (n : ℕ) : Set (Set (L.BoundedFormulaω Empty n))

The complete types realized in M at arity n: the complete types of the n-tuples of M.

@[simp]

theorem FirstOrder.Language.mem_realizedTypes {L : Language} {M : Type w} [L.Structure M] {n : ℕ} {p : Set (L.BoundedFormulaω Empty n)} : p ∈ realizedTypes M n ↔ ∃ (a : Fin n → M), infinitaryType M a = p

A set of formulas is a realized type of M exactly when it is the complete type of some tuple of M.

theorem FirstOrder.Language.infinitaryType_mem_realizedTypes {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (a : Fin n → M) : infinitaryType M a ∈ realizedTypes M n

The complete type of a tuple of M is a realized type of M.

theorem FirstOrder.Language.realizedTypes_zero {L : Language} (M : Type w) [L.Structure M] : realizedTypes M 0 = {infinitaryType M Fin.elim0}

At arity 0 the only realized type is the complete type of the empty tuple, which is the L_{ω₁ω} theory of the structure.

theorem FirstOrder.Language.omitsType_iff_forall_mem_realizedTypes_not_subset {L : Language} {M : Type w} [L.Structure M] {n : ℕ} {p : Set (L.BoundedFormulaω Empty n)} : OmitsType M p ↔ ∀ q ∈ realizedTypes M n, ¬p ⊆ q

A structure omits a partial type exactly when none of its realized types contains it.

@[simp]

theorem FirstOrder.Language.StrongHomClass.infinitaryType_comp {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n : ℕ} {F : Type u_1} [EquivLike F M N] [L.StrongHomClass F M N] (g : F) (a : Fin n → M) : infinitaryType N (⇑g ∘ a) = infinitaryType M a

An isomorphism preserves complete types: the image of a tuple has the type of the tuple.

theorem FirstOrder.Language.StrongHomClass.realizedTypes_eq {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {F : Type u_1} [EquivLike F M N] [L.StrongHomClass F M N] (g : F) (n : ℕ) : realizedTypes M n = realizedTypes N n

Isomorphic structures realize the same complete types.

Isolating formulas

theorem FirstOrder.Language.exists_isolatingFormula {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (h : (realizedTypes M n).Countable) (a : Fin n → M) : ∃ (χ : L.BoundedFormulaω Empty n), ∀ (b : Fin n → M), BoundedFormulaInf.Realize χ Empty.elim b ↔ infinitaryType M b = infinitaryType M a

Realized types are isolated. If M realizes only countably many complete n-types, then the type of each tuple a is isolated among the realized types by a single formula χ: χ holds of a tuple b of M exactly when b has the type of a. The formula χ is the countable conjunction, over the realized types q, of a formula of the type of a that does not lie in q when q differs from the type of a.

theorem TauCeti.infEquivAt_nat_iff_realizedTypes_zero_eq {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : InfEquivAt ℕ M N ↔ FirstOrder.Language.realizedTypes M 0 = FirstOrder.Language.realizedTypes N 0

L_{ω₁ω}-equivalence is equality of the realized types at arity 0. Two structures satisfy the same L_{ω₁ω} sentences exactly when they realize the same complete types at arity 0.

theorem TauCeti.SameAtomicType.infinitaryType_eq_of_isExtensionPair {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] {n : ℕ} {a : Fin n → M} {b : Fin n → N} (h : SameAtomicType a b) (hMN : L.IsExtensionPair M N) (hNM : L.IsExtensionPair N M) : FirstOrder.Language.infinitaryType M a = FirstOrder.Language.infinitaryType N b

Atomic types determine complete types along extension pairs. In a relational language, when M and N form an extension pair in both directions, tuples of M and N with the same atomic type have the same complete L_{ω₁ω}-type: they are back-and-forth equivalent at every level, in particular at the quantifier rank of each formula.