Scott sentences at stabilizing levels

scottSentenceAt M α conjoins the Scott approximation of the empty tuple with the universal closures of all tuple-upgrade implications from level α to level α + 1. At a countable internally stabilizing level, the original structure satisfies this sentence. In every model, the pairs related at level α form a tuple back-and-forth system, and therefore agree at all ordinal levels. The realizing structure need not be countable.

scottSentence M uses the least internal stabilization ordinal. Its construction and the back-and-forth conclusion are independent of the subsequent passage from a system to an isomorphism between countable structures.

Isomorphic copies satisfy these sentences by invariance of infinitary satisfaction. This supplies the isomorphism-to-satisfaction direction of their characterization.

The construction is due to Dana Scott, Logic with denumerably long formulas and finite strings of quantifiers (1965). Unlike the empty-tuple approximation called scottSentenceAt in Cameron Freer's cameronfreer/infinitary-logic, InfinitaryLogic/Scott/Formula.lean at checkpoint 9f82bd572af2d79a043c6bc3f1b745f14e0bcaa4, this sentence includes the tuple-upgrade clauses.

noncomputable def TauCeti.scottSentenceAt {L : FirstOrder.Language} [Countable ((k : ℕ) × L.Relations k)] (M : Type w) [L.Structure M] [Countable M] (α : Ordinal.{o}) : L.Sentenceω

The empty-tuple Scott approximation together with universal tuple-upgrade implications. At a countable internally stabilizing level it describes a back-and-forth class of structures.

theorem TauCeti.scottSentenceAt_def {L : FirstOrder.Language} [Countable ((k : ℕ) × L.Relations k)] (M : Type w) [L.Structure M] [Countable M] (α : Ordinal.{o}) : scottSentenceAt M α = scottFormula Fin.elim0 α ⊓ FirstOrder.Language.BoundedFormulaInf.iInfAlong (IndexCoding.ofEncodableWith (Encodable.ofCountable ((n : ℕ) × (Fin n → M)))) fun (p : (n : ℕ) × (Fin n → M)) => (FirstOrder.Language.BoundedFormulaInf.imp (scottFormula p.snd α) (scottFormula p.snd (α + 1))).alls

The defining conjunction of the empty-tuple approximation and the tuple-upgrade clauses.

@[simp]

theorem TauCeti.realize_scottSentenceAt {L : FirstOrder.Language} [Countable ((k : ℕ) × L.Relations k)] (M : Type w) [L.Structure M] [Countable M] [L.IsRelational] {N : Type w'} [L.Structure N] {α : Ordinal.{o}} (hα : α < Ordinal.omega 1) : FirstOrder.Language.SentenceInf.Realize (scottSentenceAt M α) N ↔ BFEquiv α 0 Fin.elim0 Fin.elim0 ∧ ∀ (n : ℕ) (a : Fin n → M) (b : Fin n → N), BFEquiv α n a b → BFEquiv (α + 1) n a b

Satisfaction says that the empty tuples agree at α and that every matching tuple can be upgraded to α + 1. This characterization holds for models of any cardinality.

theorem TauCeti.realize_scottSentenceAt_self {L : FirstOrder.Language} [Countable ((k : ℕ) × L.Relations k)] (M : Type w) [L.Structure M] [Countable M] [L.IsRelational] {α : Ordinal.{o}} (hα : α < Ordinal.omega 1) (hs : SelfStabilizesCompletely M α) : FirstOrder.Language.SentenceInf.Realize (scottSentenceAt M α) M

A countable structure satisfies the Scott sentence at each countable internally stabilizing level.

theorem TauCeti.isTupleBFSystem_of_realize_scottSentenceAt {L : FirstOrder.Language} [Countable ((k : ℕ) × L.Relations k)] (M : Type w) [L.Structure M] [Countable M] [L.IsRelational] {N : Type w'} [L.Structure N] {α : Ordinal.{o}} (hα : α < Ordinal.omega 1) (h : FirstOrder.Language.SentenceInf.Realize (scottSentenceAt M α) N) : IsTupleBFSystem {p : (n : ℕ) × (Fin n → M) × (Fin n → N) | BFEquiv α p.fst p.snd.1 p.snd.2}

In any model of a Scott sentence, the tuples matching at its level form a back-and-forth system. No countability or internal-stabilization hypothesis on the model is needed.

noncomputable def TauCeti.scottSentence {L : FirstOrder.Language} [Countable ((k : ℕ) × L.Relations k)] (M : Type w) [L.Structure M] [Countable M] [L.IsRelational] : L.Sentenceω

The Scott sentence using the least internal stabilization ordinal of the structure.

theorem TauCeti.scottSentence_def {L : FirstOrder.Language} [Countable ((k : ℕ) × L.Relations k)] (M : Type w) [L.Structure M] [Countable M] [L.IsRelational] : scottSentence M = scottSentenceAt M (selfStabilizationOrdinal M)

The canonical Scott sentence uses the least internal stabilization level.

@[simp]

theorem TauCeti.realize_scottSentence_self {L : FirstOrder.Language} [Countable ((k : ℕ) × L.Relations k)] (M : Type w) [L.Structure M] [Countable M] [L.IsRelational] : FirstOrder.Language.SentenceInf.Realize (scottSentence M) M

Every countable structure satisfies its canonical Scott sentence.

theorem TauCeti.bfEquiv_of_realize_scottSentence {L : FirstOrder.Language} [Countable ((k : ℕ) × L.Relations k)] (M : Type w) [L.Structure M] [Countable M] [L.IsRelational] {N : Type w'} [L.Structure N] (h : FirstOrder.Language.SentenceInf.Realize (scottSentence M) N) (β : Ordinal.{o'}) : BFEquiv β 0 Fin.elim0 Fin.elim0

A model of the canonical Scott sentence agrees with the original structure at every ordinal back-and-forth level. The ordinal universe is independent of the structure universes.

theorem FirstOrder.Language.Equiv.realize_scottSentenceAt {L : Language} [L.IsRelational] [Countable ((k : ℕ) × L.Relations k)] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [Countable M] (e : L.Equiv M N) {α : Ordinal.{o}} (hα : α < Ordinal.omega 1) (hs : TauCeti.SelfStabilizesCompletely M α) : SentenceInf.Realize (TauCeti.scottSentenceAt M α) N

Every isomorphic copy satisfies the Scott sentence at a countable internally stabilizing level of the original structure.

theorem FirstOrder.Language.Equiv.realize_scottSentence {L : Language} [L.IsRelational] [Countable ((k : ℕ) × L.Relations k)] {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [Countable M] (e : L.Equiv M N) : SentenceInf.Realize (TauCeti.scottSentence M) N

Every isomorphic copy of a countable structure satisfies its canonical Scott sentence.