Models of Scott sentences are potentially isomorphic

The tuple system supplied by a Scott sentence yields a back-and-forth system of finitely generated partial equivalences. This conclusion applies to models of arbitrary cardinality, not just countable models. It is the potential-isomorphism step in Dana Scott's Logic with denumerably long formulas and finite strings of quantifiers (1965).

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

Every model of the Scott sentence at a countable level is potentially isomorphic to the original structure. Neither internal stabilization nor countability of the model is needed.

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

Every model of the canonical Scott sentence is potentially isomorphic to the original structure, even when the model is uncountable.