Arbitrary-target stabilization (issue #17 chunk 5.1)

The kernel of the Scott completion, and the point of contact between #13 and #17: the existing stabilization theory (StabilizesCompletely, from the proved countable refinement hypothesis) upgrades BFEquiv α → BFEquiv (succ α) only against COUNTABLE targets. This file extends it to ARBITRARY targets using the fragment Löwenheim–Skolem machinery:

for each required extension, take a countable A-elementary substructure of the arbitrary target containing the current tuple (and, in the back direction, the requested new element), where the controlling fragment contains the CLOSED level-α Scott formulas of all finite tuples of the countable source (scottSeed — countably many, since the source is countable; closing is relabel Sum.inr, with realize_relabel_sumInr as the bridge). A-elementarity transfers Scott-formula realization between the target and the substructure, where the countable-target stabilization supplies the witness.

The generic extension-family bridge (bfEquiv_all_of_extensionFamily, the two-structure form of the audited thin bridge) then upgrades stabilized BFEquiv α to EVERY ordinal (bfEquiv_all_of_stabilizesCompletely_arbitrary).

The generic extension-family bridge (two arbitrary structures)

theorem FirstOrder.Language.bfEquiv_all_of_extensionFamily {L : Language} {M' N' : Type} [L.Structure M'] [L.Structure N'] (R : (n : ℕ) → (Fin n → M') → (Fin n → N') → Prop) (hzero : ∀ {n : ℕ} {a : Fin n → M'} {b : Fin n → N'}, R n a b → SameAtomicType a b) (hforth : ∀ {n : ℕ} {a : Fin n → M'} {b : Fin n → N'}, R n a b → ∀ (a' : M'), ∃ (b' : N'), R (n + 1) (Fin.snoc a a') (Fin.snoc b b')) (hback : ∀ {n : ℕ} {a : Fin n → M'} {b : Fin n → N'}, R n a b → ∀ (b' : N'), ∃ (a' : M'), R (n + 1) (Fin.snoc a a') (Fin.snoc b b')) (α : Ordinal.{u_1}) {n : ℕ} (a : Fin n → M') (b : Fin n → N') : R n a b → BFEquiv α n a b

The two-structure form of the audited thin bridge: any tuple relation with atomic agreement and the forth/back extensions is BFEquiv at every ordinal.

The closed Scott seed and its fragment

noncomputable def FirstOrder.Language.scottSeed {L : Language} [Countable ((l : ℕ) × L.Relations l)] (N : Type) [L.Structure N] [Countable N] (α : Ordinal.{u_1}) : Set ((n : ℕ) × L.BoundedFormulaω Empty n)

The closed level-α Scott formulas of all finite tuples of the countable source.

Equations

• FirstOrder.Language.scottSeed N α = ⋃ (m : ℕ), (fun (a : Fin m → N) => ⟨m, FirstOrder.Language.BoundedFormulaω.relabel Sum.inr (FirstOrder.Language.scottFormula a α)⟩) '' Set.univ

theorem FirstOrder.Language.scottSeed_countable {L : Language} [Countable ((l : ℕ) × L.Relations l)] {N : Type} [L.Structure N] [Countable N] (α : Ordinal.{u_1}) : (scottSeed N α).Countable

noncomputable def FirstOrder.Language.scottFragment {L : Language} [Countable ((l : ℕ) × L.Relations l)] (N : Type) [L.Structure N] [Countable N] (α : Ordinal.{u_1}) : L.Fragment

The controlling fragment for arbitrary-target stabilization.

Equations

• FirstOrder.Language.scottFragment N α = FirstOrder.Language.Fragment.generated (FirstOrder.Language.scottSeed N α)

theorem FirstOrder.Language.scottFragment_countable {L : Language} [Countable ((l : ℕ) × L.Relations l)] {N : Type} [L.Structure N] [Countable N] (α : Ordinal.{u_1}) : (scottFragment N α).toSet.Countable

theorem FirstOrder.Language.closedScott_mem_scottFragment {L : Language} [Countable ((l : ℕ) × L.Relations l)] {N : Type} [L.Structure N] [Countable N] (α : Ordinal.{u_1}) {m : ℕ} (a : Fin m → N) : ⟨m, BoundedFormulaω.relabel Sum.inr (scottFormula a α)⟩ ∈ (scottFragment N α).toSet

theorem FirstOrder.Language.realize_closedScott_iff {L : Language} [Countable ((l : ℕ) × L.Relations l)] {N : Type} [L.Structure N] [Countable N] {P : Type} [L.Structure P] (α : Ordinal.{u_1}) {m : ℕ} (a : Fin m → N) (b : Fin m → P) : (BoundedFormulaω.relabel Sum.inr (scottFormula a α)).Realize Empty.elim b ↔ (scottFormula a α).Realize b

The closed Scott formula realizes exactly as the open one.

Arbitrary-target stabilization

theorem FirstOrder.Language.countable_functions_of_isRelational {L : Language} [L.IsRelational] : Countable ((n : ℕ) × L.Functions n)

Relational languages have (vacuously) countably many function symbols.

theorem FirstOrder.Language.bfEquiv_iff_of_scottFragment_aElementary {L : Language} [Countable ((l : ℕ) × L.Relations l)] {N : Type} [L.Structure N] [Countable N] {P : Type} [L.Structure P] {α : Ordinal.{u_1}} (hα : α < Ordinal.omega 1) {P₀ : L.Substructure P} (hAe : AElementary (scottFragment N α) P₀.subtype) {m : ℕ} (a : Fin m → N) (b : Fin m → ↥P₀) : (BFEquiv α m a fun (i : Fin m) => ↑(b i)) ↔ BFEquiv α m a b

BFEquiv transfers between the arbitrary target and a fragment-elementary substructure, through the closed Scott formulas.

theorem FirstOrder.Language.bfEquiv_succ_of_stabilizesCompletely_arbitrary {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {N : Type} [L.Structure N] [Countable N] {P : Type} [L.Structure P] {α : Ordinal.{u_1}} (hα : α < Ordinal.omega 1) (hstab : StabilizesCompletely N α) {n : ℕ} {a : Fin n → N} {b : Fin n → P} (h : BFEquiv α n a b) : BFEquiv (Order.succ α) n a b

Arbitrary-target stabilization (the #13 × #17 kernel): a complete stabilization level of the countable source upgrades BFEquiv against an ARBITRARY target.

theorem FirstOrder.Language.bfEquiv_all_of_stabilizesCompletely_arbitrary {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {N : Type} [L.Structure N] [Countable N] {P : Type} [L.Structure P] {α : Ordinal.{u_1}} (hα : α < Ordinal.omega 1) (hstab : StabilizesCompletely N α) {n : ℕ} {a : Fin n → N} {b : Fin n → P} (h : BFEquiv α n a b) (β : Ordinal.{u_2}) : BFEquiv β n a b

Stabilized BFEquiv holds at every ordinal against arbitrary targets — the extension family is BFEquiv α itself.