Complete infinitary types and small models

The general types API of the countably-many-types project (issue #11): the complete L_{ω₁ω}-type of a finite tuple over the empty set (infinitaryType), the family of realized types at each arity (RealizedInfinitaryTypes), and the smallness predicate (Lomega1omegaSmall: countably many realized types at every arity).

Smallness DESCENDS along reducts (Lomega1omegaSmall.of_expansion — each reduct type is the preimage of an expansion type under mapLanguage, so the realized reduct types are a countable image); it does NOT ascend through arbitrary expansions, which is why the arbitrary-language endpoint of issue #11 must go through a canonical uniform expansion rather than this lemma.

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

The complete infinitary type of a tuple over the empty set: all L_{ω₁ω}-formulas (in n free variables) it realizes.

Equations

• FirstOrder.Language.infinitaryType M a = {ψ : L.BoundedFormulaω Empty n | ψ.Realize Empty.elim a}

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

The realized complete types of M at arity n.

Equations

• FirstOrder.Language.RealizedInfinitaryTypes M n = Set.range fun (a : Fin n → M) => FirstOrder.Language.infinitaryType M a

def FirstOrder.Language.Lomega1omegaSmall {L : Language} (M : Type w) [L.Structure M] : Prop

Smallness: M realizes only countably many complete L_{ω₁ω}-types, across all finite arities.

Equations

• FirstOrder.Language.Lomega1omegaSmall M = ∀ (n : ℕ), (FirstOrder.Language.RealizedInfinitaryTypes M n).Countable

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

theorem FirstOrder.Language.infinitaryType_equiv {L : Language} {M N : Type w} [L.Structure M] [L.Structure N] (e : L.Equiv M N) {n : ℕ} (a : Fin n → M) : infinitaryType M a = infinitaryType N fun (i : Fin n) => e (a i)

Isomorphism transport for types: an L-isomorphism carries the complete type of a tuple to the complete type of its image.

theorem FirstOrder.Language.Lomega1omegaSmall.of_equiv {L : Language} {M N : Type w} [L.Structure M] [L.Structure N] (e : L.Equiv M N) (h : Lomega1omegaSmall M) : Lomega1omegaSmall N

Smallness is invariant under structure isomorphism.

theorem FirstOrder.Language.Lomega1omegaSmall.of_expansion {L L' : Language} (g : L →ᴸ L') {M : Type w} [L.Structure M] [L'.Structure M] [g.IsExpansionOn M] (h : Lomega1omegaSmall M) : Lomega1omegaSmall M

Smallness descends along reducts: if M is small as an L'-structure and g : L →ᴸ L' is an expansion on M, then M is small as an L-structure. (The converse FAILS for arbitrary expansions — new symbols can realize new types.)