Back-and-forth levels of relational configurations

For a relational language L and an ordinal α, two configurations on a carrier V are α-equivalent when the empty tuples of their decoded structures are back-and-forth equivalent at depth α. This is the setoid TauCeti.RelationalConfiguration.bfEquivSetoid L V α. The levels decrease as α grows, each one is coarser than isomorphism, and on a countable carrier their intersection over all ordinals is isomorphism, by Scott's back-and-forth argument.

On a countable carrier, in a vocabulary with countably many relation symbols of each arity, every countable level is Borel: back-and-forth equivalence of any two tuples at a depth α < ω₁ is a Borel condition on the pair of configurations. Level zero is a countable conjunction of atomic tests, a successor quantifies over the countably many one-point extensions, and a limit below ω₁ is a countable conjunction of earlier levels. These levels stratify isomorphism into Borel equivalence relations, which is what descriptive dichotomies such as Silver's theorem consume when counting the countable models of an infinitary sentence.

Main definitions

• TauCeti.RelationalConfiguration.bfEquivSetoid L V α — back-and-forth equivalence at depth α of the decoded structures, as a setoid on the configurations on V.

Main results

• TauCeti.RelationalConfiguration.bfEquivSetoid_anti — the levels decrease with α;
• TauCeti.RelationalConfiguration.bfEquivSetoid_lift — lifting α across universes leaves bfEquivSetoid unchanged;
• TauCeti.RelationalConfiguration.isoSetoid_le_bfEquivSetoid — isomorphic configurations are equivalent at every level;
• TauCeti.RelationalConfiguration.isoSetoid_iff_bfEquivSetoid_of_isEmpty — on an empty carrier, every back-and-forth level coincides with isomorphism;
• TauCeti.RelationalConfiguration.isoSetoid_iff_forall_bfEquivSetoid — on a countable carrier, isomorphism is equivalence at every level;
• TauCeti.RelationalConfiguration.measurableSet_setOf_bfEquiv and TauCeti.RelationalConfiguration.measurableSet_setOf_bfEquivSetoid — below ω₁, back-and-forth equivalence of tuples, and hence each level, has Borel graph;
• TauCeti.RelationalConfiguration.exists_limit_of_bfEquiv_chain — a chain of configurations on ℕ whose consecutive members are equivalent at depth α i + ω, for a monotone α, has a limit configuration equivalent to its i-th member at depth α i.

References

• David Marker, Lectures on Infinitary Model Theory, the chapter on the space of countable models.
• Antonio Montalbán, Computable Structure Theory: Beyond the Arithmetic, Chapter XII.
• The back-and-forth setoid on codes also appears in Cameron Freer's cameronfreer/infinitary-logic, InfinitaryLogic/ModelTheory/MorleyCounting.lean.

theorem TauCeti.RelationalConfiguration.measurableSet_setOf_bfEquiv {L : FirstOrder.Language} [L.IsRelational] {V : Type w} [Countable V] [∀ (n : ℕ), Countable (L.Relations n)] {α : Ordinal.{o}} (hα : α < Ordinal.omega 1) {n : ℕ} (a b : Fin n → V) : MeasurableSet {p : RelationalConfiguration L V × RelationalConfiguration L V | BFEquiv α n a b}

Below ω₁, on a countable carrier and in a vocabulary with countably many relation symbols of each arity, back-and-forth equivalence at depth α of two fixed tuples is a Borel condition on the pair of decoded configurations.

def TauCeti.RelationalConfiguration.bfEquivSetoid (L : FirstOrder.Language) [L.IsRelational] (V : Type w) (α : Ordinal.{o}) : Setoid (RelationalConfiguration L V)

Back-and-forth equivalence at depth α, as a setoid on the configurations on V: two configurations are related when the empty tuples of their decoded structures are back-and-forth equivalent at depth α.

theorem TauCeti.RelationalConfiguration.bfEquivSetoid_apply {L : FirstOrder.Language} [L.IsRelational] {V : Type w} {α : Ordinal.{o}} {c d : RelationalConfiguration L V} : (bfEquivSetoid L V α) c d ↔ BFEquiv α 0 Fin.elim0 Fin.elim0

Two configurations are α-equivalent exactly when the empty tuples of their decoded structures are back-and-forth equivalent at depth α.

theorem TauCeti.RelationalConfiguration.bfEquivSetoid_anti {L : FirstOrder.Language} [L.IsRelational] {V : Type w} : Antitone (bfEquivSetoid L V)

The back-and-forth levels decrease: equivalence at a level implies equivalence at every lower level.

@[simp]

theorem TauCeti.RelationalConfiguration.bfEquivSetoid_lift {L : FirstOrder.Language} [L.IsRelational] {V : Type w} (α : Ordinal.{o}) : bfEquivSetoid L V (Ordinal.lift.{o', o} α) = bfEquivSetoid L V α

Lifting the ordinal depth across universes does not change bfEquivSetoid.

theorem TauCeti.RelationalConfiguration.isoSetoid_le_bfEquivSetoid {L : FirstOrder.Language} [L.IsRelational] {V : Type w} (α : Ordinal.{o}) : isoSetoid L V ≤ bfEquivSetoid L V α

Isomorphic configurations are equivalent at every back-and-forth level.

theorem TauCeti.RelationalConfiguration.eq_of_bfEquivSetoid_zero {L : FirstOrder.Language} [L.IsRelational] {V : Type w} [IsEmpty V] {c d : RelationalConfiguration L V} (h : (bfEquivSetoid L V 0) c d) : c = d

On an empty carrier, configurations that agree at back-and-forth level zero are equal.

theorem TauCeti.RelationalConfiguration.isoSetoid_iff_bfEquivSetoid_of_isEmpty {L : FirstOrder.Language} [L.IsRelational] {V : Type w} [IsEmpty V] {α : Ordinal.{o}} {c d : RelationalConfiguration L V} : (isoSetoid L V) c d ↔ (bfEquivSetoid L V α) c d

On an empty carrier, every back-and-forth level coincides with isomorphism.

theorem TauCeti.RelationalConfiguration.isoSetoid_iff_forall_bfEquivSetoid {L : FirstOrder.Language} [L.IsRelational] {V : Type w} [Countable V] {c d : RelationalConfiguration L V} : (isoSetoid L V) c d ↔ ∀ (α : Ordinal.{w}), (bfEquivSetoid L V α) c d

On a countable carrier, two configurations are isomorphic exactly when they are equivalent at every back-and-forth level. This is Scott's back-and-forth argument for the decoded structures.

theorem TauCeti.RelationalConfiguration.measurableSet_setOf_bfEquivSetoid {L : FirstOrder.Language} [L.IsRelational] {V : Type w} [Countable V] [∀ (n : ℕ), Countable (L.Relations n)] {α : Ordinal.{o}} (hα : α < Ordinal.omega 1) : MeasurableSet {p : RelationalConfiguration L V × RelationalConfiguration L V | (bfEquivSetoid L V α) p.1 p.2}

Below ω₁, on a countable carrier and in a vocabulary with countably many relation symbols of each arity, each back-and-forth level has Borel graph.

theorem TauCeti.RelationalConfiguration.exists_limit_of_bfEquiv_chain {L : FirstOrder.Language} [L.IsRelational] {c : ℕ → RelationalConfiguration L ℕ} {α : ℕ → Ordinal.{o}} (hα : Monotone α) (h : ∀ (i : ℕ), (bfEquivSetoid L ℕ (α i + Ordinal.omega0)) (c i) (c (i + 1))) : ∃ (d : RelationalConfiguration L ℕ), ∀ (i : ℕ), (bfEquivSetoid L ℕ (α i)) d (c i)

The limit of a back-and-forth chain of configurations. If α is monotone and bfEquivSetoid (α i + ω) relates c i and c (i + 1) for every i, then some configuration on ℕ is related to every c i by bfEquivSetoid (α i).