Scott's isomorphism theorem

For a countable language, every countable structure M is characterized up to isomorphism among countable structures by a single Lω₁ω sentence.

For a countable relational language, the Scott sentence of M at any countable internally stabilizing level is such a sentence: it holds in a countable structure exactly when that structure is isomorphic to M. Its models are potentially isomorphic to M, and potential isomorphism between countable structures is isomorphism. Conversely, isomorphic copies satisfy it by invariance of infinitary satisfaction.

A language with function symbols reduces to its graph language L.graphLanguage, which is relational and has countably many relation symbols when L has countably many symbols. The back-translation of the Scott sentence of the graph expansion of M holds in a structure exactly when that Scott sentence holds in its graph expansion (FirstOrder.Language.BoundedFormulaInf.realize_backTranslate), and two structures are isomorphic exactly when their graph expansions are (FirstOrder.Language.nonempty_equiv_graphExpansion_iff).

The countability of the model cannot be dropped: models of the Scott sentence of any cardinality are only potentially isomorphic to M (TauCeti.potentialIso_of_realize_scottSentenceAt).

Main results

• TauCeti.realize_scottSentenceAt_iff: in a countable relational language, at a countable internally stabilizing level, the Scott sentence holds in a countable structure exactly when it is isomorphic to M.
• TauCeti.realize_scottSentence_iff: the same for the canonical Scott sentence.
• TauCeti.scott_isomorphism: Scott's isomorphism theorem, in a countable language every countable structure has an Lω₁ω sentence true in exactly the countable structures isomorphic to it.

References

• Dana Scott, Logic with denumerably long formulas and finite strings of quantifiers, in The Theory of Models, 1965.
• David Marker, Lectures on Infinitary Model Theory, Cambridge University Press, 2016.

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

At a countable internally stabilizing level, the Scott sentence of a countable structure M holds in a countable structure exactly when that structure is isomorphic to M.

@[simp]

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

The canonical Scott sentence of a countable structure M holds in a countable structure exactly when that structure is isomorphic to M.

theorem TauCeti.scott_isomorphism {L : FirstOrder.Language} [Countable ((k : ℕ) × L.Functions k)] [Countable ((k : ℕ) × L.Relations k)] (M : Type w) [L.Structure M] [Countable M] : ∃ (σ : L.Sentenceω), FirstOrder.Language.SentenceInf.Realize σ M ∧ ∀ (N : Type w') [inst : L.Structure N] [Countable N], FirstOrder.Language.SentenceInf.Realize σ N ↔ Nonempty (L.Equiv M N)

Scott's isomorphism theorem. In a countable language, every countable structure M has an Lω₁ω sentence that M satisfies and that holds in a countable structure, in any universe, exactly when that structure is isomorphic to M.

Function symbols are allowed: the sentence is the back-translation of the Scott sentence of the graph expansion of M.