Proof of CountableRefinementHypothesis

This file proves CountableRefinementHypothesis and provides unconditional wrappers for all Sentence.lean-level theorems. Together with the downstream wrappers in Rank.lean, Height.lean, CountableCorollary.lean, and CountingModels.lean, this recovers the full unconditional API.

Strategy

The proof uses the "constant chain" argument:

1. Self-stabilization (exists_complete_self_stabilization) gives α₀ < ω₁ where the internal BFEquiv relation on M is frozen.
2. Under self-stabilization, forth/back witnesses chosen at level α₀ automatically work at all higher levels (chain_step + witness_at_all_levels).
3. By transfinite induction (BFEquiv_of_all_finite_levels), BFEquiv (α₀+k) for all k upgrades to BFEquiv ε for all ε.
4. Hence no refinement ordinals exist above γ = sup_k(α₀+k) < ω₁, and R(n,a) ⊆ [0,γ) is countable.

Main Result

• countableRefinementHypothesis : CountableRefinementHypothesis L

Countability of initial segments below ω₁

Self-stabilization to full stabilization

The key insight: SelfStabilizesCompletely M α₀ (internal BFEquiv stabilization) implies that the back-and-forth game cannot create new refinements above α₀ + ω, because any forth/back witness at level α₀ already works at all higher levels (the "constant chain" argument). This avoids the need to count external BFEquiv types directly.

The Counting Lemma

theorem FirstOrder.Language.countableRefinementHypothesis {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] : L.CountableRefinementHypothesis

The countable refinement hypothesis holds for all countable relational languages.

For a countable structure M in a countable relational language, and any n-tuple a from M, the set of refinement ordinals R(n, a) = {ε < ω₁ | ∃ (N, b), BFEquiv ε ∧ ¬BFEquiv (succ ε)} is countable.

Proof: Self-stabilization (exists_complete_self_stabilization) gives α₀ < ω₁ where internal BFEquiv on M is frozen. For any ε above γ = sup_k(α₀+k) with BFEquiv ε n a b, the monotonicity of BFEquiv gives BFEquiv (α₀+k) for all k. The "constant chain" argument (witness_at_all_levels) shows that forth/back witnesses at level α₀ work at all higher levels (via self-stabilization + transitivity), so BFEquiv_of_all_finite_levels upgrades BFEquiv to the successor. Hence no refinement ordinals exist above γ < ω₁.

Unconditional Wrappers (Sentence.lean level)

Each theorem below is a one-liner applying countableRefinementHypothesis to the corresponding _of variant in Sentence.lean.

theorem FirstOrder.Language.countable_refinement_steps {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {M : Type w} [L.Structure M] [Countable M] (n : ℕ) (a : Fin n → M) : {α : Ordinal.{0} | α < Ordinal.omega 1 ∧ ∃ (N : Type w) (x : L.Structure N) (_ : Countable N) (b : Fin n → N), BFEquiv α n a b ∧ ¬BFEquiv (Order.succ α) n a b}.Countable

The set of refinement ordinals for any tuple is countable.

theorem FirstOrder.Language.per_tuple_stabilization_below_omega1 {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {M : Type w} [L.Structure M] [Countable M] (n : ℕ) (a : Fin n → M) : ∃ γ < Ordinal.omega 1, ∀ (α : Ordinal.{0}), γ ≤ α → α < Ordinal.omega 1 → Order.succ α < Ordinal.omega 1 → ∀ (N : Type w) [inst : L.Structure N] [Countable N] (b : Fin n → N), BFEquiv α n a b ↔ BFEquiv (Order.succ α) n a b

Per-tuple stabilization below ω₁.

theorem FirstOrder.Language.exists_complete_stabilization {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (M : Type w) [L.Structure M] [Countable M] : ∃ α < Ordinal.omega 1, StabilizesCompletely M α

Complete stabilization below ω₁.

theorem FirstOrder.Language.exists_stabilization {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (M : Type w) [L.Structure M] [Countable M] : ∃ α < Ordinal.omega 1, StabilizesAt M α

Existence of a stabilization ordinal (BFEquiv0 characterizes isomorphism).

theorem FirstOrder.Language.stabilizationOrdinal_lt_omega1' {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (M : Type w) [L.Structure M] [Countable M] : stabilizationOrdinal M < Ordinal.omega 1

The stabilization ordinal is below ω₁.

theorem FirstOrder.Language.stabilizationOrdinal_stabilizes {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (M : Type w) [L.Structure M] [Countable M] : StabilizesAt M (stabilizationOrdinal M)

The characterization property holds at stabilizationOrdinal.

theorem FirstOrder.Language.stabilizationOrdinal_spec {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (M : Type w) [L.Structure M] [Countable M] (N : Type w) [L.Structure N] [Countable N] : BFEquiv0 M N (stabilizationOrdinal M) ↔ Nonempty (L.Equiv M N)

BFEquiv0 at stabilizationOrdinal characterizes isomorphism.

theorem FirstOrder.Language.scottSentence_characterizes {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (M : Type w) [L.Structure M] [Countable M] (N : Type w) [L.Structure N] [Countable N] : (scottSentence M).realize_as_sentence N ↔ Nonempty (L.Equiv M N)

The Scott sentence of M characterizes M up to isomorphism among countable structures.

theorem FirstOrder.Language.scottSentence_realizes_implies_equiv {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (M : Type w) [L.Structure M] [Countable M] (N : Type w) [L.Structure N] [Countable N] (h : (scottSentence M).realize_as_sentence N) : Nonempty (L.Equiv M N)

If N realizes the Scott sentence of M, then M ≃[L] N.

theorem FirstOrder.Language.scottSentence_self {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (M : Type w) [L.Structure M] [Countable M] : (scottSentence M).realize_as_sentence M

M itself satisfies its own Scott sentence.

theorem FirstOrder.Language.scottSentence_of_equiv {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (M N : Type w) [L.Structure M] [L.Structure N] [Countable M] [Countable N] (e : L.Equiv M N) : (scottSentence M).realize_as_sentence N

Isomorphic structures satisfy each other's Scott sentences.