The back-and-forth stabilization ordinal

The back-and-forth hierarchy of any pair of structures collapses at a set-sized ordinal, with no countability hypothesis anywhere: bfStabilizationOrdinal L M N is the supremum, over the triples that fail somewhere, of their least failure level, so equivalence at that one ordinal already implies equivalence at every ordinal (bfEquiv_bfStabilizationOrdinal_iff_all).

The argument is purely cardinal: each failing triple has a least failure level by well-ordering of the ordinals (csInf_mem), and the family of triples is small, so those least levels are bounded (Ordinal.bddAbove_of_small). Nothing about the language or the structures enters.

Relation to ModelTheory/ArbitraryStabilization.lean

That file solves a different problem and its results are not comparable to these. It transfers stabilization from a countable source to arbitrary targets, upgrading BFEquiv α to BFEquiv (succ α) at a level supplied externally (StabilizesCompletely, itself obtained from the countable refinement hypothesis), and it pays for arbitrary targets with the fragment Löwenheim–Skolem machinery. Here there is no source/target asymmetry, no fragment machinery and no countability: the collapse level is produced outright from the two structures. The price is that the level is a supremum with no bound better than smallness — in particular this does not give the < ω₁ bound that Scott rank needs for countable structures, which remains the business of the refinement-counting route.

Main definitions

• bfStabilizationOrdinal: the level at which the hierarchy between two structures collapses.

Main results

• bfEquiv_bfStabilizationOrdinal_iff_all: equivalence at the stabilization ordinal is equivalence at every ordinal.
• bfEquiv_bfStabilizationOrdinal_succ: the self-stability form, propagating level-bfStab equivalence of two tuples of one structure to the successor level.

noncomputable def FirstOrder.Language.bfStabilizationOrdinal (L : Language) (M : Type w) [L.Structure M] (N : Type w') [L.Structure N] [Small.{uι, max w' w} ((n : ℕ) × (Fin n → M) × (Fin n → N))] : Ordinal.{uι}

The stabilization ordinal of the back-and-forth hierarchy between M and N: the supremum, over all triples that fail somewhere, of their least failure level.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.bfEquiv_bfStabilizationOrdinal_iff_all {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] [Small.{uι, max w' w} ((n : ℕ) × (Fin n → M) × (Fin n → N))] {n : ℕ} {a : Fin n → M} {b : Fin n → N} : BFEquiv (L.bfStabilizationOrdinal M N) n a b ↔ ∀ (β : Ordinal.{uι}), BFEquiv β n a b

Stabilization: back-and-forth equivalence at the stabilization level already implies equivalence at every level. The equivalence hierarchy of an arbitrary pair of structures collapses at a set-sized ordinal.

theorem FirstOrder.Language.bfEquiv_bfStabilizationOrdinal_succ {L : Language} {M : Type w} [L.Structure M] [Small.{uι, w} ((n : ℕ) × (Fin n → M) × (Fin n → M))] {n : ℕ} {a a' : Fin n → M} (h : BFEquiv (L.bfStabilizationOrdinal M M) n a a') : BFEquiv (L.bfStabilizationOrdinal M M + 1) n a a'

Self-stability of M at its own stabilization ordinal: level-bfStabilizationOrdinal equivalence of two M-tuples propagates to the successor level. This is the form the backward direction of a Scott sentence consumes.