Back-and-forth levels are model classes

For a configuration c on a countable carrier V, in a relational language with countably many relation symbols, and a countable ordinal α, the sentence c.scottSentenceAtLevel α is the canonical Scott formula scottFormula of the empty tuple of the structure decoded from c, read as a sentence. A structure satisfies it exactly when its empty tuple is back-and-forth equivalent to that of c at depth α. Hence the α-class {d | bfEquivSetoid L V α c d} of c is the model class of c.scottSentenceAtLevel α, and the model class depends only on that class.

So below ω₁ every back-and-forth class of configurations is cut out by a single sentence of L_{ω₁ω}. Sentence cuts of a model class therefore include its cuts by level classes, which is what lets counting arguments split a class of countable models along a back-and-forth level using only sentences, as in the analysis of minimal counterexamples to Vaught's conjecture.

Main definitions

• TauCeti.RelationalConfiguration.scottSentenceAtLevel c α: the Scott formula at level α of the empty tuple of the structure decoded from c, as a sentence.

Main results

• TauCeti.RelationalConfiguration.realize_scottSentenceAtLevel: below ω₁, a structure of any cardinality, in any universe, satisfies c.scottSentenceAtLevel α exactly when its empty tuple is back-and-forth equivalent at depth α to that of c.
• TauCeti.RelationalConfiguration.modelsOf_scottSentenceAtLevel: below ω₁, the model class of c.scottSentenceAtLevel α on the carrier of c is the bfEquivSetoid L V α-class of c.
• TauCeti.RelationalConfiguration.modelsOf_scottSentenceAtLevel_eq_iff: two configurations have the same level-α model class exactly when they are α-equivalent.

References

• Antonio Montalbán, Computable Structure Theory: Beyond the Arithmetic, Part 2, Lemma XII.5 (level classes are defined by sentences), here in the one-element back-and-forth convention of TauCeti.BFEquiv.
• The statement follows modelsOf_scottSentenceAt in Cameron Freer's cameronfreer/infinitary-logic at checkpoint 518a366cba97b1ae8c4dc64a297a396939bc3e0b, InfinitaryLogic/Descriptive/MinimallyUncountable.lean (Apache-2.0).

noncomputable def TauCeti.RelationalConfiguration.scottSentenceAtLevel {L : FirstOrder.Language} [L.IsRelational] [Countable ((k : ℕ) × L.Relations k)] {V : Type w} [Countable V] (c : RelationalConfiguration L V) (α : Ordinal.{o}) : L.Sentenceω

The Scott sentence at level α of a configuration c: the canonical Scott formula at level α of the empty tuple of the structure decoded from c, read as a sentence. Below ω₁ its models are the structures back-and-forth equivalent to c at depth α.

theorem TauCeti.RelationalConfiguration.scottSentenceAtLevel_def {L : FirstOrder.Language} [L.IsRelational] [Countable ((k : ℕ) × L.Relations k)] {V : Type w} [Countable V] (c : RelationalConfiguration L V) (α : Ordinal.{o}) : c.scottSentenceAtLevel α = scottFormula Fin.elim0 α

The Scott sentence at level α of c is the Scott formula of the empty tuple of the decoded structure.

@[simp]

theorem TauCeti.RelationalConfiguration.realize_scottSentenceAtLevel {L : FirstOrder.Language} [L.IsRelational] [Countable ((k : ℕ) × L.Relations k)] {V : Type w} [Countable V] (c : RelationalConfiguration L V) {α : Ordinal.{o}} (hα : α < Ordinal.omega 1) (N : Type w') [L.Structure N] : FirstOrder.Language.SentenceInf.Realize (c.scottSentenceAtLevel α) N ↔ BFEquiv α 0 Fin.elim0 Fin.elim0

Below ω₁, a structure of any cardinality, in any universe, satisfies the Scott sentence at level α of c exactly when its empty tuple is back-and-forth equivalent at depth α to that of the structure decoded from c.

theorem TauCeti.RelationalConfiguration.mem_modelsOf_scottSentenceAtLevel {L : FirstOrder.Language} [L.IsRelational] [Countable ((k : ℕ) × L.Relations k)] {V : Type w} [Countable V] (c : RelationalConfiguration L V) {α : Ordinal.{o}} (hα : α < Ordinal.omega 1) {W : Type w'} {d : RelationalConfiguration L W} : d ∈ modelsOf (c.scottSentenceAtLevel α) ↔ BFEquiv α 0 Fin.elim0 Fin.elim0

Below ω₁, a configuration on any carrier lies in the model class of the Scott sentence at level α of c exactly when the empty tuples of the two decoded structures are back-and-forth equivalent at depth α.

theorem TauCeti.RelationalConfiguration.modelsOf_scottSentenceAtLevel {L : FirstOrder.Language} [L.IsRelational] [Countable ((k : ℕ) × L.Relations k)] {V : Type w} [Countable V] (c : RelationalConfiguration L V) {α : Ordinal.{o}} (hα : α < Ordinal.omega 1) : modelsOf (c.scottSentenceAtLevel α) = {d : RelationalConfiguration L V | (bfEquivSetoid L V α) c d}

Level classes are model classes. Below ω₁, the configurations on V satisfying the Scott sentence at level α of c are exactly those α-equivalent to c.

theorem TauCeti.RelationalConfiguration.self_mem_modelsOf_scottSentenceAtLevel {L : FirstOrder.Language} [L.IsRelational] [Countable ((k : ℕ) × L.Relations k)] {V : Type w} [Countable V] (c : RelationalConfiguration L V) {α : Ordinal.{o}} (hα : α < Ordinal.omega 1) : c ∈ modelsOf (c.scottSentenceAtLevel α)

Below ω₁, a configuration satisfies its own Scott sentence at level α.

theorem TauCeti.RelationalConfiguration.modelsOf_scottSentenceAtLevel_eq_iff {L : FirstOrder.Language} [L.IsRelational] [Countable ((k : ℕ) × L.Relations k)] {V : Type w} [Countable V] {c d : RelationalConfiguration L V} {α : Ordinal.{o}} (hα : α < Ordinal.omega 1) : modelsOf (c.scottSentenceAtLevel α) = modelsOf (d.scottSentenceAtLevel α) ↔ (bfEquivSetoid L V α) c d

Below ω₁, two configurations on V have the same level-α model class exactly when they are α-equivalent, so the model class of c.scottSentenceAtLevel α depends exactly on the α-class of c.