Fragment types and bounded back-and-forth: the two minimal adapters

The comparison audit (roadmap step 2) found the existing machinery sufficient except for two small adapters between realized fragment types (Fragment.realizedType) and back-and-forth equivalence (BFEquiv). Both are stated at the exact rank the underlying theorems use, ≤ α, with no successor.

• A. Fragment.realizedType_eq_of_bfEquiv: if every member of the arity-n slice of F has quantifier rank ≤ α, then BFEquiv α n a b gives equal realized F-types. This is the carrier-generic forward transfer BFEquiv_implies_agreeQR read through openBounds (qrank_openBounds), so it holds for any carriers in any universes and needs no countability.

• B. Fragment.bfEquiv_of_realizedType_eq: at a countable source carrier and a countable relational signature, if the bounded form scottBounded a α of the Scott formula of a at level α < ω₁ belongs to F, then equal realized F-types give BFEquiv α n a b. One source tuple's Scott formula suffices for the pairwise implication. Membership is a sufficient hypothesis: other formula families can separate the same classes, and the hypothesis is not to be replaced by countability or generation of F.

Neither adapter promotes a bounded level to fragment elementarity or to an extension theorem, and neither shortens "all levels" to "countable levels". The pairwise adapters do not supply countability of realized extension spectra; that second counting input is separate (FragmentBFSuccessor.lean). B needs countability of the source carrier only, not of the target, and the two carriers may live in different universes.

Classical background: Marker, Lectures on Infinitary Model Theory (Cambridge, 2016), Theorem 2.1.4 and Theorem 2.1.13 (agreement up to quantifier rank ≤ α and back-and-forth at level α); Gao, Invariant Descriptive Set Theory (CRC Press, 2009), Definitions 12.1.1–12.1.2. The fragment-slice packaging is as implemented here.

theorem FirstOrder.Language.Fragment.realizedType_eq_of_bfEquiv {L : Language} [L.IsRelational] (F : L.Fragment) {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {α : Ordinal.{0}} {n : ℕ} {a : Fin n → M} {b : Fin n → N} (h : BFEquiv α n a b) (hF : ∀ (φ : F.slice n), (↑φ).qrank ≤ α) : F.realizedType M a = F.realizedType N b

A. Bounded back-and-forth gives fragment agreement. Every member of the arity-n slice has quantifier rank ≤ α; then BFEquiv α n a b forces the realized F-types to coincide. Carrier-generic, any universes, no countability.

noncomputable def FirstOrder.Language.Fragment.scottBounded {L : Language} [Countable ((l : ℕ) × L.Relations l)] {M : Type w} [L.Structure M] [Countable M] {n : ℕ} (a : Fin n → M) (α : Ordinal.{u_1}) : L.BoundedFormulaω Empty n

The bounded form of the Scott formula of a at level α: its free variables rebound.

Equations

• FirstOrder.Language.Fragment.scottBounded a α = FirstOrder.Language.BoundedFormulaω.relabel Sum.inr (FirstOrder.Language.scottFormula a α)

theorem FirstOrder.Language.Fragment.realize_scottBounded_iff {L : Language} {M : Type w} [L.Structure M] [Countable M] [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {N : Type w'} [L.Structure N] {n : ℕ} (a : Fin n → M) (b : Fin n → N) (α : Ordinal.{u_1}) (hα : α < Ordinal.omega 1) : (scottBounded a α).Realize Empty.elim b ↔ BFEquiv α n a b

theorem FirstOrder.Language.Fragment.bfEquiv_of_realizedType_eq {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (F : L.Fragment) {M : Type w} [L.Structure M] [Countable M] {N : Type w'} [L.Structure N] {α : Ordinal.{u_1}} (hα : α < Ordinal.omega 1) {n : ℕ} {a : Fin n → M} {b : Fin n → N} (hmem : ⟨n, scottBounded a α⟩ ∈ F) (h : F.realizedType M a = F.realizedType N b) : BFEquiv α n a b

B. Fragment agreement gives bounded back-and-forth, when the bounded Scott formula of the source tuple at level α < ω₁ is a member of F. Countable source carrier and countable relational signature, as the Scott formula's construction requires. The membership is sufficient, not necessary.