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)

theorem FirstOrder.Language.canonicalScottSentence_iff_potentialIso_of {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (hcount : L.CountableRefinementHypothesis) {M : Type w} [L.Structure M] [Countable M] {N : Type w} [L.Structure N] [Countable N] : (canonicalScottSentence M).realize_as_sentence N ↔ Nonempty (L.PotentialIso M N)

Conditional variant of canonicalScottSentence_iff_potentialIso.

theorem FirstOrder.Language.canonicalScottSentence_characterizes_of {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (hcount : L.CountableRefinementHypothesis) {M : Type w} [L.Structure M] [Countable M] {N : Type w} [L.Structure N] [Countable N] : (canonicalScottSentence M).realize_as_sentence N ↔ Nonempty (L.Equiv M N)

Conditional variant of canonicalScottSentence_characterizes.

theorem FirstOrder.Language.canonicalScottSentence_equiv_scottSentence_of {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (hcount : L.CountableRefinementHypothesis) {M : Type w} [L.Structure M] [Countable M] {N : Type w} [L.Structure N] [Countable N] : (canonicalScottSentence M).realize_as_sentence N ↔ (scottSentence M).realize_as_sentence N

Conditional variant of canonicalScottSentence_equiv_scottSentence.

theorem FirstOrder.Language.canonicalScottSentence_qrank_of {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (hcount : L.CountableRefinementHypothesis) (M : Type w) [L.Structure M] [Countable M] : (canonicalScottSentence M).qrank ≤ scottHeight M + Ordinal.omega0

Conditional variant of canonicalScottSentence_qrank.

theorem FirstOrder.Language.canonicalScottSentence_iff_potentialIso {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {M : Type w} [L.Structure M] [Countable M] {N : Type w} [L.Structure N] [Countable N] : (canonicalScottSentence M).realize_as_sentence N ↔ Nonempty (L.PotentialIso M N)

The canonical Scott sentence characterizes potential isomorphism.

theorem FirstOrder.Language.canonicalScottSentence_characterizes {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {M : Type w} [L.Structure M] [Countable M] {N : Type w} [L.Structure N] [Countable N] : (canonicalScottSentence M).realize_as_sentence N ↔ Nonempty (L.Equiv M N)

For countable structures, the canonical Scott sentence characterizes isomorphism.

theorem FirstOrder.Language.canonicalScottSentence_equiv_scottSentence {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {M : Type w} [L.Structure M] [Countable M] {N : Type w} [L.Structure N] [Countable N] : (canonicalScottSentence M).realize_as_sentence N ↔ (scottSentence M).realize_as_sentence N

The canonical Scott sentence is semantically equivalent to the standard Scott sentence.

theorem FirstOrder.Language.canonicalScottSentence_qrank {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (M : Type w) [L.Structure M] [Countable M] : (canonicalScottSentence M).qrank ≤ scottHeight M + Ordinal.omega0

The quantifier rank of the canonical Scott sentence is bounded.