Scott Sentences

This file proves the main theorem about Scott sentences: every countable structure in a relational countable language has a Scott sentence characterizing it up to isomorphism.

Main Definitions

• scottSentence: The Scott sentence of a countable structure.

Main Results

• scottSentence_characterizes: A countable structure N satisfies the Scott sentence of M if and only if M and N are isomorphic.

Implementation Notes

The proof proceeds by showing:

1. High enough BF-equivalence (with the empty tuple) implies IsExtensionPair in both directions.
2. IsExtensionPair in both directions between countable structures implies isomorphism (using mathlib's equiv_between_cg).
3. The Scott formula at the stabilization ordinal captures exactly this.

Helper definitions to reduce repetition

@[reducible, inline]

abbrev FirstOrder.Language.BFEquiv0 {L : Language} (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] (α : Ordinal.{u_1}) : Prop

BFEquiv at the empty tuple level. This is the key semantic predicate for Scott sentences.

Equations

• FirstOrder.Language.BFEquiv0 M N α = FirstOrder.Language.BFEquiv α 0 Fin.elim0 Fin.elim0

def FirstOrder.Language.StabilizesAt {L : Language} (M : Type w) [L.Structure M] (α : Ordinal.{u_1}) : Prop

The ordinal α stabilizes for M if BFEquiv0 at level α characterizes isomorphism with M among all countable structures of the same type.

Equations

• FirstOrder.Language.StabilizesAt M α = ∀ (N : Type ?u.24) [inst : L.Structure N] [Countable N], FirstOrder.Language.BFEquiv0 M N α ↔ Nonempty (L.Equiv M N)

def FirstOrder.Language.StabilizesForTuples {L : Language} (M : Type w) [L.Structure M] (α : Ordinal.{u_1}) (n : ℕ) : Prop

BFEquiv α on n-tuples from M equals BFEquiv (succ α) for all countable N. This captures when the BFEquiv relation has stopped distinguishing tuples at level α.

Equations

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

def FirstOrder.Language.StabilizesCompletely {L : Language} (M : Type w) [L.Structure M] (α : Ordinal.{u_1}) : Prop

All tuple sizes stabilize at α. This is the key condition for the back-and-forth argument to yield an isomorphism.

Equations

• FirstOrder.Language.StabilizesCompletely M α = ∀ (n : ℕ), FirstOrder.Language.StabilizesForTuples M α n

def FirstOrder.Language.StrongStabilizesForTuples {L : Language} (M : Type w) [L.Structure M] (α : Ordinal.{u_1}) (n : ℕ) : Prop

Strong stabilization: BFEquiv is constant for all β ≥ α. This is a priori stronger than StabilizesForTuples (which only compares α to succ α), but the two are equivalent. The strong form is more convenient for upgrading BFEquiv to arbitrary higher ordinals.

Equations

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

theorem FirstOrder.Language.StrongStabilizesForTuples.toStabilizesForTuples {L : Language} {M : Type w} [L.Structure M] {α : Ordinal.{u_1}} {n : ℕ} (h : StrongStabilizesForTuples M α n) : StabilizesForTuples M α n

Strong stabilization implies weak stabilization (take β = succ α).

theorem FirstOrder.Language.equiv_implies_BFEquiv {L : Language} {M N : Type w} [L.Structure M] [L.Structure N] (e : L.Equiv M N) (α : Ordinal.{u_1}) (n : ℕ) (a : Fin n → M) : BFEquiv α n a (⇑e ∘ a)

An isomorphism induces BF-equivalence at all ordinal levels.

Stabilization Theory

The key insight is that for countable structures, the BFEquiv equivalence classes form a refining sequence of partitions on tuples. Since there are only countably many tuples, this sequence must stabilize before ω₁.

Partition Argument: For each α, BFEquiv α defines an equivalence relation on pairs (a, N, b) where a is an n-tuple from M and b is an n-tuple from some countable N. As α increases, this relation becomes finer (more distinguishing). But a decreasing chain of partitions on a countable set has cardinality at most ω, so must stabilize at some countable ordinal.

Key Properties of Stabilization:

1. If StabilizesForTuples M α n, then BFEquiv α n a b ↔ BFEquiv β n a b for all β ≥ α
2. StabilizesCompletely allows the back-and-forth to close: witnesses at level α stay at level α
3. This resolves the quantifier swap issue: we don't need ω, just any stable ordinal

Note: StabilizesForTuples for a single tuple size n does NOT propagate to higher ordinals without also having stabilization for (n+1)-tuples. This is because BFEquiv at successor levels involves forth/back which creates tuples of size (n+1).

The correct approach is to use StabilizesCompletely which ensures all tuple sizes stabilize simultaneously. See BFEquiv_upgrade_at_stabilization.

def FirstOrder.Language.SelfStabilizesCompletely {L : Language} (M : Type w) [L.Structure M] (α : Ordinal.{u_1}) : Prop

Self-stabilization: BFEquiv α on n-tuples from M vs M equals BFEquiv (succ α) for all n. This is weaker than StabilizesCompletely which requires the iff to hold for all countable N, not just M itself.

Equations

• FirstOrder.Language.SelfStabilizesCompletely M α = ∀ (n : ℕ) (a a' : Fin n → M), FirstOrder.Language.BFEquiv α n a a' ↔ FirstOrder.Language.BFEquiv (Order.succ α) n a a'

theorem FirstOrder.Language.BFEquiv_upgrade_at_stabilization {L : Language} {M N : Type w} [L.Structure M] [L.Structure N] [Countable N] {α : Ordinal.{u_1}} (hstab : StabilizesCompletely M α) {n : ℕ} {a : Fin n → M} {b : Fin n → N} (h : BFEquiv α n a b) (β : Ordinal.{u_1}) (hβ : α ≤ β) : BFEquiv β n a b

At a complete stabilization ordinal, BFEquiv upgrades to all higher ordinals. This is the key lemma that resolves the quantifier swap problem.

The proof proceeds by ordinal induction on β. The key insight is that at stabilization, forth/back witnesses stay at level α, so we can upgrade them along with the base BFEquiv.

theorem FirstOrder.Language.StabilizesCompletely.toStrongStabilizesForTuples {L : Language} {M : Type w} [L.Structure M] {α : Ordinal.{u_1}} (hstab : StabilizesCompletely M α) (n : ℕ) : StrongStabilizesForTuples M α n

StabilizesCompletely implies StrongStabilizesForTuples for all tuple sizes. This is the key property that allows upgrading BFEquiv to arbitrary higher ordinals. This is essentially a restatement of BFEquiv_upgrade_at_stabilization in terms of StrongStabilizesForTuples.

theorem FirstOrder.Language.StabilizesForTuples.downward_propagation {L : Language} {M : Type w} [L.Structure M] {α : Ordinal.{u_1}} {n : ℕ} (hstab : StabilizesForTuples M α (n + 1)) : StabilizesForTuples M (Order.succ α) n

Downward propagation: If (n+1)-tuples have full stabilization at α, then n-tuples have full stabilization at succ α.

The key insight: BFEquiv (succ(succ α)) n a b requires BFEquiv (succ α) n a b plus forth/back at level succ α. The forth/back at succ α involves BFEquiv (succ α) (n+1), which by the (n+1)-stabilization hypothesis equals BFEquiv α (n+1). But BFEquiv (succ α) n a b already implies forth/back involving BFEquiv α (n+1) (from the succ definition). So the additional forth/back at succ α adds no new information, giving the iff.

theorem FirstOrder.Language.exists_complete_self_stabilization {L : Language} (M : Type w) [L.Structure M] [Countable M] : ∃ α < Ordinal.omega 1, SelfStabilizesCompletely M α

For countable M, there exists α < ω₁ where all tuple sizes self-stabilize (BFEquiv α n a a' ↔ BFEquiv (succ α) n a a' for all n and all a, a' : Fin n → M).

Proof idea: For each triple (n, a, a'), the sequence α ↦ BFEquiv α n a a' is antitone (by BFEquiv.monotone). Define the "change ordinal" as sInf {γ | ¬BFEquiv γ n a a'} when this set is nonempty; this is the ordinal where the truth value permanently drops from True to False. For α past the change ordinal, both BFEquiv α and BFEquiv (succ α) are False, so the iff holds. If the change ordinal does not exist (BFEquiv is True everywhere) or is ≥ ω₁, then for any α < ω₁ with succ α < ω₁, both sides are True.

Take globalStab = sup of all change ordinals that are < ω₁ (one per triple). By countability of the sigma type and regularity of ω₁, globalStab < ω₁. At globalStab, for each triple, either the change ordinal is ≤ globalStab (both sides False) or > globalStab (both sides True since succ globalStab < ω₁).

Countable intersection and BFEquiv-to-PotentialIso lemmas

theorem FirstOrder.Language.nonempty_iInter_of_antitone_of_nonempty {X : Type u_1} [Countable X] (S : Ordinal.{0} → Set X) (hAnti : Antitone S) (hNonempty : ∀ α < Ordinal.omega 1, (S α).Nonempty) : (⋂ α ∈ Set.Iio (Ordinal.omega 1), S α).Nonempty

A decreasing ω₁-chain of nonempty subsets of a countable type has nonempty intersection.

More precisely: if S : Ordinal → Set X where X is countable, S is antitone (S α ⊇ S β for α ≤ β), and each S α is nonempty for α < ω₁, then ⋂ α < ω₁, S α is nonempty.

Proof: For each x ∈ S 0, define d(x) = sInf {α | x ∉ S α} (the "departure ordinal"). If all d(x) < ω₁, then sup {d(x)} < ω₁ by regularity of ω₁ and countability of X. Let γ = sup {d(x)}. Then S γ = ∅ (every element has departed), contradicting nonemptiness. So some x has d(x) ≥ ω₁, meaning x ∈ S α for all α < ω₁.

theorem FirstOrder.Language.BFEquiv_below_omega1_implies_potentialIso {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] [Countable M] {N : Type w} [L.Structure N] [Countable N] (h : ∀ α < Ordinal.omega 1, BFEquiv α 0 Fin.elim0 Fin.elim0) : Nonempty (L.PotentialIso M N)

If two countable structures are BF-equivalent at all ordinal levels below ω₁ (for the empty tuple), then there exists a potential isomorphism between them, and hence they are isomorphic.

Proof: Define the family F = {(k, a, b) | ∀ α < ω₁, BFEquiv α k a b}. This family contains the empty tuple (by hypothesis) and is compatible (BFEquiv 0 gives SameAtomicType). For the forth property: given (k, a, b) ∈ F and m : M, for each α < ω₁, from BFEquiv (succ α) k a b (since succ α < ω₁ by regularity), BFEquiv.forth gives n'_α with BFEquiv α (k+1) (snoc a m) (snoc b n'_α). The sets S_α = {n' ∈ N | BFEquiv α (k+1) (snoc a m) (snoc b n')} form a decreasing chain (by BFEquiv.monotone) of nonempty subsets of the countable type N. By nonempty_iInter_of_antitone_of_nonempty, ∃ n' in the intersection, giving BFEquiv α (k+1) (snoc a m) (snoc b n') for all α < ω₁. The back property is symmetric.

The result then follows from PotentialIso.countable_toEquiv.

theorem FirstOrder.Language.BFEquiv_below_omega1_implies_iso {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] [Countable M] {N : Type w} [L.Structure N] [Countable N] (h : ∀ α < Ordinal.omega 1, BFEquiv α 0 Fin.elim0 Fin.elim0) : Nonempty (L.Equiv M N)

Corollary: If BFEquiv at all levels below ω₁ for empty tuples between countable structures, then they are isomorphic. Combines BFEquiv_below_omega1_implies_potentialIso with PotentialIso.countable_toEquiv.

Refinement Descent Lemmas

These lemmas decompose refinement failures at n-tuples into refinement failures at (n+1)-tuples at strictly smaller ordinals. They are the key infrastructure for proving per_tuple_stabilization_below_omega1 without relying on the FormulaCode bridge.

theorem FirstOrder.Language.refinement_descent_succ {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {n : ℕ} {a : Fin n → M} {b : Fin n → N} {δ : Ordinal.{u_1}} (hBF : BFEquiv (Order.succ δ) n a b) (hNotBF : ¬BFEquiv (Order.succ (Order.succ δ)) n a b) : ∃ (m : M) (n' : N), BFEquiv δ (n + 1) (Fin.snoc a m) (Fin.snoc b n') ∧ ¬BFEquiv (Order.succ δ) (n + 1) (Fin.snoc a m) (Fin.snoc b n')

At a successor refinement ordinal succ δ, the failure of BFEquiv (succ(succ δ)) (while BFEquiv (succ δ) holds) produces a refinement at the (n+1)-tuple level at ordinal δ.

The proof is by contradiction: if every (n+1)-extension with BFEquiv δ also satisfies BFEquiv (succ δ), then we can rebuild BFEquiv (succ(succ δ)) from the forth/back witnesses at level δ (which come from BFEquiv (succ δ)), contradicting the hypothesis.

theorem FirstOrder.Language.exists_refinement_between {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {n : ℕ} {a : Fin n → M} {b : Fin n → N} {δ α : Ordinal.{u_1}} (hδα : δ < α) (hBFδ : BFEquiv δ n a b) (hNotBFα : ¬BFEquiv α n a b) : ∃ (ε : Ordinal.{u_1}), δ ≤ ε ∧ ε < α ∧ BFEquiv ε n a b ∧ ¬BFEquiv (Order.succ ε) n a b

If BFEquiv holds at δ but fails at α (with δ < α), there exists a refinement ordinal ε ∈ [δ, α) where BFEquiv ε holds but BFEquiv (succ ε) fails.

This follows from well-foundedness of ordinals: the first failure ordinal above δ must be a successor (limits can't be first failures, since BFEquiv at a limit is the conjunction of all lower levels).

theorem FirstOrder.Language.refinement_descent_limit {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {n : ℕ} {a : Fin n → M} {b : Fin n → N} {α : Ordinal.{u_1}} (hα_limit : Order.IsSuccLimit α) (hBF : BFEquiv α n a b) (hNotBF : ¬BFEquiv (Order.succ α) n a b) : ∃ (m : M) (n' : N), ∃ ε < α, BFEquiv ε (n + 1) (Fin.snoc a m) (Fin.snoc b n') ∧ ¬BFEquiv (Order.succ ε) (n + 1) (Fin.snoc a m) (Fin.snoc b n')

At a limit refinement ordinal α (BFEquiv α holds but BFEquiv (succ α) fails), the forth/back failure at level α generates refinement ordinals below α for extensions.

The proof decomposes ¬BFEquiv (succ α) into forth or back failure at level α, then uses exists_refinement_between to find a successor refinement ordinal for the extension.

theorem FirstOrder.Language.refinement_descent {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {n : ℕ} {a : Fin n → M} {b : Fin n → N} {ε : Ordinal.{u_1}} (hε : 0 < ε) (hBF : BFEquiv ε n a b) (hNotBF : ¬BFEquiv (Order.succ ε) n a b) : ∃ (m : M) (n' : N), ∃ ε' < ε, BFEquiv ε' (n + 1) (Fin.snoc a m) (Fin.snoc b n') ∧ ¬BFEquiv (Order.succ ε') (n + 1) (Fin.snoc a m) (Fin.snoc b n')

Combined refinement descent: at any refinement ordinal ε > 0 (BFEquiv ε holds but BFEquiv (succ ε) fails), the descent produces an extension tuple with a TRUE refinement witness: BFEquiv ε' ∧ ¬BFEquiv (succ ε') with ε' < ε.

Combines refinement_descent_succ (successor ε) and refinement_descent_limit (limit ε) into one lemma.

Conditional Pipeline (Code-free approach)

The counting hypothesis captures the key content that each refinement set is countable. This decouples the Scott analysis pipeline from the FormulaCode bridge (agree_codes_implies_BFEquiv), which has a known gap. All downstream results (per_tuple_stabilization_below_omega1_of, exists_complete_stabilization_of, scottRank_le_implies_stabilizesCompletely_of) hold conditional on this hypothesis.

The hypothesis is mathematically true: each refinement step corresponds to a split in the formula-type partition, and countable structures admit only countably many such splits. A full formal proof requires either a code-based bridge or a direct game-theoretic counting argument.

def FirstOrder.Language.CountableRefinementHypothesis (L : Language) [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] : Prop

Counting hypothesis for per-tuple stabilization.

For a countable structure M in a countable relational language, the set of ordinals below ω₁ where BFEquiv refinement occurs for a fixed tuple is countable.

This encapsulates the deep counting argument: each refinement step corresponds to a split in the formula-type partition, and countable structures admit only countably many such splits.

Boundary: This is the sole non-trivial hypothesis in the Scott analysis pipeline. All other reasoning (descent lemmas, stabilization from countability, Scott rank bounds) is fully formalized.

Equations

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

theorem FirstOrder.Language.per_tuple_stabilization_below_omega1_of {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (hcount : L.CountableRefinementHypothesis) {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, conditional on CountableRefinementHypothesis.

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

Complete stabilization, conditional on CountableRefinementHypothesis.

theorem FirstOrder.Language.BFEquiv_stabilization_implies_equiv {L : Language} [L.IsRelational] {M N : Type w} [L.Structure M] [L.Structure N] [Countable M] [Countable N] {α : Ordinal.{u_1}} (hstab : StabilizesCompletely M α) (h : BFEquiv α 0 Fin.elim0 Fin.elim0) : Nonempty (L.Equiv M N)

At a complete stabilization ordinal, BFEquiv0 implies isomorphism for countable structures. This is the corrected version of BFEquiv_omega_implies_equiv.

noncomputable def FirstOrder.Language.stabilizationOrdinal {L : Language} (M : Type w) [L.Structure M] [Countable M] : Ordinal.{0}

The stabilization ordinal for a structure M: the least ordinal where the Scott analysis stabilizes. We fix the ordinal universe to 0 for consistency with our BFEquiv definitions.

Equations

• FirstOrder.Language.stabilizationOrdinal M = sInf {α : Ordinal.{0} | FirstOrder.Language.StabilizesAt M α}

noncomputable def FirstOrder.Language.scottSentence {L : Language} [Countable ((l : ℕ) × L.Relations l)] (M : Type w) [L.Structure M] [Countable M] : L.Formulaω (Fin 0)

The Scott sentence of a countable structure M in a relational countable language.

A sentence is a formula with no free variables, which corresponds to Formulaω (Fin 0) since Fin 0 is empty.

Equations

• FirstOrder.Language.scottSentence M = FirstOrder.Language.scottFormula Fin.elim0 (FirstOrder.Language.stabilizationOrdinal M)

def FirstOrder.Language.Formulaω.realize_as_sentence {L : Language} (φ : L.Formulaω (Fin 0)) (N : Type w) [L.Structure N] : Prop

Realize a formula with no free variables as a sentence in a structure.

Equations

• φ.realize_as_sentence N = φ.Realize Fin.elim0

theorem FirstOrder.Language.Formulaω.realize_as_sentence_iff_toSentenceω {L : Language} (φ : L.Formulaω (Fin 0)) (N : Type w) [L.Structure N] : φ.realize_as_sentence N ↔ φ.toSentenceω.Realize N

Bridge between realize_as_sentence and Sentenceω.Realize via toSentenceω.

Conditional Scott Sentence Pipeline

Variants of the entire Scott sentence chain, conditional on CountableRefinementHypothesis. The same scottSentence definition is used; only the proof that it characterizes isomorphism is rebuilt.

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

Conditional variant of exists_stabilization.

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

Conditional variant of stabilizationOrdinal_lt_omega1'.

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

Conditional variant of stabilizationOrdinal_stabilizes.

theorem FirstOrder.Language.scottSentence_characterizes_of {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (hcount : L.CountableRefinementHypothesis) (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)

Conditional Scott sentence characterization: variant of scottSentence_characterizes, conditional on CountableRefinementHypothesis.

A countable structure N satisfies the Scott sentence of M iff M ≅ N. Uses the same scottSentence M definition; only the proof is rebuilt through the conditional pipeline.

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

A countable structure satisfies its own Scott sentence.

theorem FirstOrder.Language.scottSentence_realizes_implies_equiv_of {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (hcount : L.CountableRefinementHypothesis) (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)

If N realizes the Scott sentence of M, then M ≅ N.

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

Isomorphic countable structures satisfy each other's Scott sentences.