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:
- High enough BF-equivalence (with the empty tuple) implies
IsExtensionPairin both directions. IsExtensionPairin both directions between countable structures implies isomorphism (using mathlib'sequiv_between_cg).- The Scott formula at the stabilization ordinal captures exactly this.
Helper definitions to reduce repetition #
BFEquiv at the empty tuple level. This is the key semantic predicate for Scott sentences.
Equations
Instances For
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.2) [inst : L.Structure N] [Countable N], FirstOrder.Language.BFEquiv0 M N α ↔ Nonempty (L.Equiv M N)
Instances For
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.
Instances For
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
Instances For
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:
- If StabilizesForTuples M α n, then BFEquiv α n a b ↔ BFEquiv β n a b for all β ≥ α
- StabilizesCompletely allows the back-and-forth to close: witnesses at level α stay at level α
- 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.
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'
Instances For
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.
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 #
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.
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.
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.
Instances For
Per-tuple stabilization, conditional on CountableRefinementHypothesis.
Complete stabilization, conditional on CountableRefinementHypothesis.
At a complete stabilization ordinal, BFEquiv0 implies isomorphism for countable structures. This is the corrected version of BFEquiv_omega_implies_equiv.
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
Instances For
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
Instances For
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.
Conditional variant of exists_stabilization.
Conditional variant of stabilizationOrdinal_lt_omega1'.
Conditional variant of stabilizationOrdinal_stabilizes.
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.