Canonical Scott formulas

For a tuple a in a countable relational structure, scottFormula a α describes its back-and-forth class at every countable ordinal α. The realizing structure can have arbitrary cardinality and lie in an independent universe. The tuple occupies bound-variable slots.

At a successor the formula retains the previous approximation and requires matching one-element extensions in both directions. At a countable limit it conjoins all earlier approximations. The limit clause at uncountable ordinals is assigned the true formula; the characteristic theorem is asserted only below the first uncountable ordinal. These formulas are the ingredients for sentences characterizing countable structures.

The construction follows Dana Scott, Logic with denumerably long formulas and finite strings of quantifiers (1965), and Cameron Freer's cameronfreer/infinitary-logic, InfinitaryLogic/Scott/Formula.lean at checkpoint 9f82bd572af2d79a043c6bc3f1b745f14e0bcaa4. Here tuples occupy bound positions rather than free variables, and the ordinal universe is independent of the structure universes.

noncomputable def TauCeti.scottFormula {L : FirstOrder.Language} [Countable ((k : ℕ) × L.Relations k)] {M : Type w} [L.Structure M] [Countable M] {n : ℕ} (a : Fin n → M) (α : Ordinal.{o}) : L.BoundedFormulaω Empty n

The canonical Scott approximation of a tuple in a relational language. At countable ordinals it characterizes back-and-forth equivalence; uncountable limit stages are assigned the true formula. The construction uses equality and relation tests and is defined for every language.

@[simp]

theorem TauCeti.scottFormula_zero {L : FirstOrder.Language} [Countable ((k : ℕ) × L.Relations k)] {M : Type w} [L.Structure M] [Countable M] {n : ℕ} (a : Fin n → M) : scottFormula a 0 = atomicDiagram a

The zero approximation is the atomic diagram.

theorem TauCeti.scottFormula_add_one {L : FirstOrder.Language} [Countable ((k : ℕ) × L.Relations k)] {M : Type w} [L.Structure M] [Countable M] {n : ℕ} (a : Fin n → M) (α : Ordinal.{o}) : scottFormula a (α + 1) = scottFormula a α ⊓ ((FirstOrder.Language.BoundedFormulaInf.iInfAlong (IndexCoding.ofEncodableWith (Encodable.ofCountable M)) fun (x : M) => FirstOrder.Language.BoundedFormulaInf.ex (scottFormula (Fin.snoc a x) α)) ⊓ (FirstOrder.Language.BoundedFormulaInf.iSupAlong (IndexCoding.ofEncodableWith (Encodable.ofCountable M)) fun (x : M) => scottFormula (Fin.snoc a x) α).all)

A successor approximation retains the preceding formula and adds forth and back clauses.

theorem TauCeti.scottFormula_limit {L : FirstOrder.Language} [Countable ((k : ℕ) × L.Relations k)] {M : Type w} [L.Structure M] [Countable M] {n : ℕ} (a : Fin n → M) {α : Ordinal.{o}} (hlim : Order.IsSuccLimit α) (hα : α < Ordinal.omega 1) : scottFormula a α = FirstOrder.Language.BoundedFormulaInf.iInfAlong (IndexCoding.ofEncodableWith (Encodable.ofCountable ↑(Set.Iio α))) fun (β : ↑(Set.Iio α)) => scottFormula a ↑β

At a countable limit, the approximation conjoins all previous approximations.

@[simp]

theorem TauCeti.realize_scottFormula_iff_bfEquiv {L : FirstOrder.Language} [Countable ((k : ℕ) × L.Relations k)] {M : Type w} [L.Structure M] [Countable M] {n : ℕ} [L.IsRelational] {N : Type w'} [L.Structure N] (a : Fin n → M) (b : Fin n → N) {α : Ordinal.{o}} (hα : α < Ordinal.omega 1) : FirstOrder.Language.BoundedFormulaInf.Realize (scottFormula a α) Empty.elim b ↔ BFEquiv α n a b

A tuple in any structure satisfies the canonical Scott formula exactly when it is back-and-forth equivalent to the original tuple at that countable ordinal.