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 L_∞ω-equivalent (PotentialIso_implies_LinfEquivW) and L_ω₁ω-equivalent;
• 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

theorem FirstOrder.Language.realize_canonicalScottSentence_iff_bfEquiv_all {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {N : Type} [L.Structure N] [Countable N] {P : Type} [L.Structure P] : (canonicalScottSentence N).realize_as_sentence P ↔ ∀ (β : Ordinal.{0}), BFEquiv β 0 Fin.elim0 Fin.elim0

Arbitrary models of the canonical Scott sentence are back-and-forth equivalent to the source at every ordinal — scottHeight supplies complete stabilization, and the arbitrary-target kernel upgrades it.

noncomputable def FirstOrder.Language.canonicalScottSentenceω {L : Language} [Countable ((l : ℕ) × L.Relations l)] (N : Type) [L.Structure N] [Countable N] : L.Sentenceω

The canonical Scott sentence in Sentenceω form.

Equations

• FirstOrder.Language.canonicalScottSentenceω N = FirstOrder.Language.BoundedFormulaω.relabel Sum.inr (FirstOrder.Language.canonicalScottSentence N)

theorem FirstOrder.Language.realize_canonicalScottSentenceω_iff {L : Language} [Countable ((l : ℕ) × L.Relations l)] {N : Type} [L.Structure N] [Countable N] {P : Type} [L.Structure P] : (canonicalScottSentenceω N).Realize P ↔ (canonicalScottSentence N).realize_as_sentence P

theorem FirstOrder.Language.realize_canonicalScottSentenceω_iff_bfEquiv_all {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {N : Type} [L.Structure N] [Countable N] {P : Type} [L.Structure P] : (canonicalScottSentenceω N).Realize P ↔ ∀ (β : Ordinal.{0}), BFEquiv β 0 Fin.elim0 Fin.elim0

theorem FirstOrder.Language.realize_canonicalScottSentenceω_self {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {N : Type} [L.Structure N] [Countable N] : (canonicalScottSentenceω N).Realize N

The source satisfies its own canonical Scott sentence.

Chunk 5.3: semantic completeness first, syntactic completeness after

theorem FirstOrder.Language.bfEquiv_all_of_realize_canonicalScottSentenceω_pair {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {N : Type} [L.Structure N] [Countable N] {P Q : Type} [L.Structure P] [L.Structure Q] (hP : (canonicalScottSentenceω N).Realize P) (hQ : (canonicalScottSentenceω N).Realize Q) (β : Ordinal.{0}) : BFEquiv β 0 Fin.elim0 Fin.elim0

Pairwise equivalence: any two models of the canonical Scott sentence are back-and-forth equivalent at every ordinal, by transitivity through the countable source.

theorem FirstOrder.Language.linfEquivW_of_realize_canonicalScottSentenceω_pair {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {N : Type} [L.Structure N] [Countable N] {P Q : Type} [L.Structure P] [L.Structure Q] (hP : (canonicalScottSentenceω N).Realize P) (hQ : (canonicalScottSentenceω N).Realize Q) : L.LinfEquivW P Q

Semantic L_∞ω-completeness: any two models of the canonical Scott sentence are L_∞ω-equivalent.

theorem FirstOrder.Language.lomegaEquiv_of_realize_canonicalScottSentenceω_pair {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {N : Type} [L.Structure N] [Countable N] {P Q : Type} [L.Structure P] [L.Structure Q] (hP : (canonicalScottSentenceω N).Realize P) (hQ : (canonicalScottSentenceω N).Realize Q) : L.LomegaEquiv P Q

L_ω₁ω-equivalence of any two models, via toLinf.

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.lomega1omegaComplete_canonicalScottSentenceω {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {N : Type} [L.Structure N] [Countable N] : Lomega1omegaComplete (canonicalScottSentenceω N)

The canonical Scott sentence is complete — derived from the semantic equivalence of its models, anchored at the source.

theorem FirstOrder.Language.canonicalScottSentenceω_entails {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {N : Type} [L.Structure N] [Countable N] {φ : L.Sentenceω} (hφ : φ.Realize N) {P : Type} [L.Structure P] (hP : (canonicalScottSentenceω N).Realize P) : φ.Realize P

Entailment: the canonical Scott sentence entails every sentence its source satisfies.

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.