Directed unions of A-elementary substructures, and omitting types (issue #13 units 6–7)

Per the frozen audit (docs/fragments-audit.md §7–§8): the PRIMARY chain theorem is a common-ambient directed-union result — a nonempty directed family of A-elementary substructures of ONE model M has an A-elementary directed union (aElementary_iSup), and each link is A-elementary in the union (aElementary_inclusion_iSup, via two-out-of-three). The linearly-ordered chain corollary (aElementary_iSup_of_monotone) covers both the ω- and ω₁-chain forms that #16 consumes; abstract direct limits are deliberately deferred.

The finite-arity OmitsFiniteType API (unit 7): omission passes down to A-elementary substructures (OmitsFiniteType.of_aElementary) and through directed unions (OmitsFiniteType.iSup) when the type's formulas lie in the fragment.

theorem FirstOrder.Language.aElementary_iSup {L : Language} {M : Type w} [L.Structure M] {A : L.Fragment} {ι : Type u_1} [Nonempty ι] {S : ι → L.Substructure M} (hdir : Directed (fun (x1 x2 : L.Substructure M) => x1 ≤ x2) S) (hS : ∀ (i : ι), AElementary A (S i).subtype) : AElementary A (⨆ (i : ι), S i).subtype

The common-ambient directed union theorem: a nonempty directed family of A-elementary substructures has an A-elementary union.

theorem FirstOrder.Language.aElementary_inclusion_iSup {L : Language} {M : Type w} [L.Structure M] {A : L.Fragment} {ι : Type u_1} [Nonempty ι] {S : ι → L.Substructure M} (hdir : Directed (fun (x1 x2 : L.Substructure M) => x1 ≤ x2) S) (hS : ∀ (i : ι), AElementary A (S i).subtype) (i : ι) : AElementary A (Substructure.inclusion ⋯)

Each link is A-elementary in the union (two-out-of-three).

theorem FirstOrder.Language.aElementary_iSup_of_monotone {L : Language} {M : Type w} [L.Structure M] {A : L.Fragment} {ι : Type u_2} [Nonempty ι] [LinearOrder ι] {S : ι → L.Substructure M} (hmono : Monotone S) (hS : ∀ (i : ι), AElementary A (S i).subtype) : AElementary A (⨆ (i : ι), S i).subtype

The chain corollary (the ω- and ω₁-chain forms): a monotone chain over a nonempty linear order has an A-elementary union.

Omitting types (unit 7)

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

Finite-arity type omission: no tuple realizes every formula of p.

Equations

• FirstOrder.Language.OmitsFiniteType M p = ∀ (a : Fin n → M), ∃ φ ∈ p, ¬φ.Realize Empty.elim a

theorem FirstOrder.Language.OmitsFiniteType.of_aElementary {L : Language} {M : Type w} [L.Structure M] {A : L.Fragment} {n : ℕ} {p : Set (L.BoundedFormulaω Empty n)} {N : L.Substructure M} (hAe : AElementary A N.subtype) (hp : ∀ φ ∈ p, ⟨n, φ⟩ ∈ A.toSet) (h : OmitsFiniteType M p) : OmitsFiniteType (↥N) p

Omission passes down to A-elementary substructures when the type lies in the fragment.

theorem FirstOrder.Language.OmitsFiniteType.iSup {L : Language} {M : Type w} [L.Structure M] {A : L.Fragment} {ι : Type u_1} [Nonempty ι] {S : ι → L.Substructure M} (hdir : Directed (fun (x1 x2 : L.Substructure M) => x1 ≤ x2) S) (hS : ∀ (i : ι), AElementary A (S i).subtype) {n : ℕ} {p : Set (L.BoundedFormulaω Empty n)} (hp : ∀ φ ∈ p, ⟨n, φ⟩ ∈ A.toSet) (h : ∀ (i : ι), OmitsFiniteType (↥(S i)) p) : OmitsFiniteType (↥(⨆ (i : ι), S i)) p

Omission passes through directed unions of A-elementary links when the type lies in the fragment: a union tuple lives in one link, which omits, and the link's A-elementarity in the union transports the failure.