The Scott completion and categoricity (issue #17 chunks 5.2–6)

The canonical Scott sentence of a countable structure — whose scottHeight supplies COMPLETE STABILIZATION — characterizes its ARBITRARY models up to back-and-forth equivalence at every ordinal (realize_canonicalScottSentence_iff_bfEquiv_all, via the arbitrary-target stabilization kernel). Consequences, in order:

• any two models of the canonical sentence are pairwise BFEquiv at every level (transitivity through the countable source), hence potentially isomorphic, hence L_∞ω-equivalent at every branching carrier (PotentialIso.infEquivAt). L_ω₁ω-equivalence is then the carrier-ℕ case, not a separate result reached by an embedding: L.Sentenceω is L.SentenceInf ℕ, so LomegaEquiv and InfEquivAt L ℕ are the same proposition;
• Lomega1omegaComplete — the repository-level completeness predicate — holds for the canonical Scott sentence (lomega1omegaComplete_canonicalScottSentenceω), DERIVED from the semantic equivalence, never the reverse;
• the unconditional complete-subclass intermediate (exists_complete_sentence_of_lomega1omegaSmall): every small model of φ satisfies a complete sentence entailing φ — its own companion's Scott sentence;
• the categoricity payoff (exists_complete_kCategorical_of_hasArbLargeModels): if φ has arbitrarily large models and is κ-categorical, some complete ψ ⊨ φ has a model of size exactly κ and is ITSELF κ-categorical.

Everything is for countable relational vocabularies ([L.IsRelational], [Countable (Σ l, L.Relations l)]), inherited from the Scott/Karp stack per the frozen audit.

Chunk 5.2: the arbitrary-model characterization

Chunk 5.3: semantic completeness first, syntactic completeness after

def FirstOrder.Language.Lomega1omegaComplete {L : Language} (ψ : L.Sentenceω) : Prop

Repository-level completeness: a sentence is L_ω₁ω-complete when it decides every Sentenceω across its models.

Equations

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

theorem FirstOrder.Language.exists_complete_sentence_of_lomega1omegaSmall {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {M : Type} [L.Structure M] (hsmall : Lomega1omegaSmall M) {φ : L.Sentenceω} (hφ : φ.Realize M) : ∃ (ψ : L.Sentenceω), Lomega1omegaComplete ψ ∧ ψ.Realize M ∧ ∀ (P : Type) (x : L.Structure P), ψ.Realize P → φ.Realize P

The unconditional complete-subclass intermediate (issue #17 chunk 5 endpoint): every small model of φ satisfies a complete sentence entailing φ — its own countable companion's canonical Scott sentence.

Chunk 6: the categoricity payoff

def FirstOrder.Language.KCategorical {L : Language} (φ : L.Sentenceω) (κ : Cardinal.{0}) : Prop

κ-categoricity of a sentence: all κ-sized models are isomorphic.

Equations

• FirstOrder.Language.KCategorical φ κ = ∀ (P Q : Type) (x : L.Structure P) (x_1 : L.Structure Q), φ.Realize P → φ.Realize Q → Cardinal.mk P = κ → Cardinal.mk Q = κ → Nonempty (L.Equiv P Q)

theorem FirstOrder.Language.exists_complete_kCategorical_of_hasArbLargeModels {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {φ : L.Sentenceω} (hφarb : HasArbLargeModels φ) {κ : Cardinal.{0}} (hκ : Cardinal.aleph0 ≤ κ) (hcat : KCategorical φ κ) : ∃ (ψ : L.Sentenceω), Lomega1omegaComplete ψ ∧ (∀ (P : Type) (x : L.Structure P), ψ.Realize P → φ.Realize P) ∧ (∃ (P : Type) (x : L.Structure P), ψ.Realize P ∧ Cardinal.mk P = κ) ∧ KCategorical ψ κ

The categoricity payoff (issue #17 chunk 6): a κ-categorical sentence with arbitrarily large models admits a COMPLETE sentence entailing it, with a model of size exactly κ — and the complete sentence is itself κ-categorical.