Canonical Scott Sentence

The canonical Scott sentence of a structure M is the Scott formula at Scott height level for the empty tuple. It is the "optimal" Scott sentence whose quantifier rank is minimized among Scott formulas.

Main Definitions

• canonicalScottSentence: The Scott formula at Scott height for the empty tuple.

Main Results

• canonicalScottSentence_iff_potentialIso: Characterizes potential isomorphism.
• canonicalScottSentence_characterizes: For countable structures, characterizes isomorphism.
• canonicalScottSentence_equiv_scottSentence: Semantically equivalent to the standard Scott sentence.
• canonicalScottSentence_qrank: Quantifier rank bounded by scottHeight + ω.

noncomputable def FirstOrder.Language.canonicalScottSentence {L : Language} [Countable ((l : ℕ) × L.Relations l)] (M : Type w) [L.Structure M] [Countable M] : L.Formulaω (Fin 0)

The canonical Scott sentence of a structure M, defined as the Scott formula at Scott height level for the empty tuple.

This is the "optimal" Scott sentence in the sense that its quantifier rank is minimized (among Scott formulas). It characterizes the structure up to potential isomorphism, and for countable structures, up to isomorphism.

Equations

• FirstOrder.Language.canonicalScottSentence M = FirstOrder.Language.scottFormula Fin.elim0 (FirstOrder.Language.scottHeight M)