Back-and-forth scattered sets of configurations

A set K of relational configurations on ℕ is back-and-forth scattered when, at every countable back-and-forth level α, it meets only countably many α-classes. These are classes of the level restricted to K, not individual configurations: K itself may be uncountable. The notion is monotone, and a set meeting countably many isomorphism classes is scattered, since isomorphism refines every level. Scatteredness can be checked through observations: maps with countably many values on K at each level, equal values forcing equivalence at that level.

Scatteredness is what makes an isolating rank count isomorphism classes exactly. On a scattered set, each rank stratum of the isomorphism classes injects into a countable level quotient, so it is countable. Hence a scattered set meets at most ℵ₁ isomorphism classes (the stratification bound TauCeti.IsIsolatingRank.mk_isoClasses_le_aleph_one_of_countable_levels, applied to TauCeti.BFScattered.countable_quotient), exactly ℵ₁ when it meets uncountably many, and countably many exactly when the rank is bounded below ω₁ on it. In particular, whether a rank is bounded on a scattered set does not depend on which isolating rank is used.

The definition, observation criterion, and rank-counting results assume no definability or invariance of K and no countability of the language. In a language with countably many relation symbols of each arity, any thin Borel set K of configurations on ℕ—one containing no nonempty perfect set of pairwise non-isomorphic configurations—is back-and-forth scattered (TauCeti.BFScattered.of_isThinOn), still without assuming isomorphism invariance of K, by the one-level Silver dichotomy.

Main definitions

• TauCeti.BFScattered K: K meets countably many classes at every countable level.

Main results

• TauCeti.bfScattered_iff_countable_image: the image form of scatteredness.
• TauCeti.BFScattered.mono: subsets of scattered sets are scattered.
• TauCeti.BFScattered.of_countable_isoClasses: countably many isomorphism classes give a scattered set.
• TauCeti.bfScattered_of_observation: scatteredness from observations at each level.
• TauCeti.BFScattered.of_isThinOn: a thin Borel set of configurations on ℕ is scattered.
• TauCeti.IsIsolatingRank.countable_rankOnIsoClasses_preimage: on a scattered set, every rank stratum of the isomorphism classes is countable.
• TauCeti.IsIsolatingRank.mk_isoClasses_eq_aleph_one: a scattered set meeting uncountably many isomorphism classes meets exactly ℵ₁ of them.
• TauCeti.IsIsolatingRank.countable_isoClasses_iff_bounded: a scattered set meets countably many isomorphism classes exactly when the rank is bounded below ω₁ on it.
• TauCeti.IsIsolatingRank.exists_rank_bound_iff: on a scattered set, any two isolating ranks are bounded together.

References

• J. H. Silver, Counting the number of equivalence classes of Borel and coanalytic equivalence relations, Annals of Mathematical Logic 18 (1980), 1–28.
• David Marker, Lectures on Infinitary Model Theory, Cambridge University Press, 2016, the chapter on Vaught counterexamples (scattered sentences).
• Antonio Montalbán, Computable Structure Theory: Beyond the Arithmetic, Part 2, Chapter XII, §XII.1 (scattered and unbounded sentences).
• Back-and-forth scatteredness and the counting of scattered classes are also formalized in Cameron Freer's cameronfreer/infinitary-logic, InfinitaryLogic/Descriptive/BFScattered.lean, InfinitaryLogic/Descriptive/ScatteredCounting.lean, and InfinitaryLogic/Conditional/MorleyPerfect.lean (checkpoint 518a366, Apache-2.0). The statements here are for an arbitrary isolating rank and discharge Silver's theorem unconditionally.

def TauCeti.BFScattered {L : FirstOrder.Language} [L.IsRelational] (K : Set (RelationalConfiguration L ℕ)) : Prop

A set K of configurations on ℕ is back-and-forth scattered when, at every countable level α, the restriction of bfEquivSetoid L ℕ α to K has countably many classes. The set K itself may be uncountable.

theorem TauCeti.bfScattered_iff {L : FirstOrder.Language} [L.IsRelational] {K : Set (RelationalConfiguration L ℕ)} : BFScattered K ↔ ∀ α < Ordinal.omega 1, Countable (Quotient (Setoid.comap Subtype.val (RelationalConfiguration.bfEquivSetoid L ℕ α)))

Unfolding lemma for TauCeti.BFScattered.

theorem TauCeti.bfScattered_iff_countable_image {L : FirstOrder.Language} [L.IsRelational] {K : Set (RelationalConfiguration L ℕ)} : BFScattered K ↔ ∀ α < Ordinal.omega 1, (Quotient.mk (RelationalConfiguration.bfEquivSetoid L ℕ α) '' K).Countable

A set is scattered exactly when it meets countably many classes of every countable level.

theorem TauCeti.BFScattered.countable_quotient {L : FirstOrder.Language} [L.IsRelational] {K : Set (RelationalConfiguration L ℕ)} (hK : BFScattered K) {α : Ordinal.{0}} (hα : α < Ordinal.omega 1) : Countable (Quotient (Setoid.comap Subtype.val (RelationalConfiguration.bfEquivSetoid L ℕ α)))

A scattered set has countably many classes at each countable level.

theorem TauCeti.BFScattered.mono {L : FirstOrder.Language} [L.IsRelational] {K C : Set (RelationalConfiguration L ℕ)} (hKC : K ⊆ C) (hC : BFScattered C) : BFScattered K

Subsets of scattered sets are scattered.

theorem TauCeti.BFScattered.of_countable_isoClasses {L : FirstOrder.Language} [L.IsRelational] {K : Set (RelationalConfiguration L ℕ)} [Countable (Quotient (Setoid.comap Subtype.val (RelationalConfiguration.isoSetoid L ℕ)))] : BFScattered K

A set meeting countably many isomorphism classes is scattered: isomorphism refines every back-and-forth level.

theorem TauCeti.bfScattered_of_observation {L : FirstOrder.Language} [L.IsRelational] {K : Set (RelationalConfiguration L ℕ)} {β : Ordinal.{0} → Type u_1} (obs : (α : Ordinal.{0}) → ↑K → β α) (hcount : ∀ α < Ordinal.omega 1, (Set.range (obs α)).Countable) (hobs : ∀ α < Ordinal.omega 1, ∀ (c d : ↑K), obs α c = obs α d → (RelationalConfiguration.bfEquivSetoid L ℕ α) ↑c ↑d) : BFScattered K

Scatteredness from observations. Suppose that at each countable level α an observation obs α on the members of K takes countably many values, and members with equal observations are α-equivalent. Then K is scattered.

theorem TauCeti.BFScattered.of_isThinOn {L : FirstOrder.Language} [L.IsRelational] {K : Set (RelationalConfiguration L ℕ)} [∀ (n : ℕ), Countable (L.Relations n)] (hK : MeasurableSet K) (h : (RelationalConfiguration.isoSetoid L ℕ).IsThinOn K) : BFScattered K

Thin Borel sets are back-and-forth scattered. In a relational language with countably many relation symbols of each arity, any Borel set K of configurations on ℕ that carries no nonempty perfect set of pairwise non-isomorphic configurations is back-and-forth scattered. No isomorphism invariance of K is required.

theorem TauCeti.IsIsolatingRank.countable_rankOnIsoClasses_preimage {L : FirstOrder.Language} [L.IsRelational] {K : Set (RelationalConfiguration L ℕ)} {ρ : RelationalConfiguration L ℕ → Ordinal.{0}} (h : IsIsolatingRank ρ) (hK : BFScattered K) (α : Ordinal.{0}) : (rankOnIsoClasses ⋯ K ⁻¹' {α}).Countable

On a scattered set, every rank stratum of the isomorphism classes is countable: it injects into the level quotient at that rank.

theorem TauCeti.IsIsolatingRank.mk_isoClasses_eq_aleph_one {L : FirstOrder.Language} [L.IsRelational] {K : Set (RelationalConfiguration L ℕ)} {ρ : RelationalConfiguration L ℕ → Ordinal.{0}} (h : IsIsolatingRank ρ) (hK : BFScattered K) [Uncountable (Quotient (Setoid.comap Subtype.val (RelationalConfiguration.isoSetoid L ℕ)))] : Cardinal.mk (Quotient (Setoid.comap Subtype.val (RelationalConfiguration.isoSetoid L ℕ))) = Cardinal.aleph 1

A scattered set meeting uncountably many isomorphism classes meets exactly ℵ₁ of them.

theorem TauCeti.IsIsolatingRank.countable_isoClasses_iff_bounded {L : FirstOrder.Language} [L.IsRelational] {K : Set (RelationalConfiguration L ℕ)} {ρ : RelationalConfiguration L ℕ → Ordinal.{0}} (h : IsIsolatingRank ρ) (hK : BFScattered K) : Countable (Quotient (Setoid.comap Subtype.val (RelationalConfiguration.isoSetoid L ℕ))) ↔ ∃ β < Ordinal.omega 1, ∀ c ∈ K, ρ c < β

A scattered set meets countably many isomorphism classes exactly when the isolating rank is bounded on it by a countable ordinal.

theorem TauCeti.IsIsolatingRank.exists_rank_bound_iff {L : FirstOrder.Language} [L.IsRelational] {K : Set (RelationalConfiguration L ℕ)} {ρ σ : RelationalConfiguration L ℕ → Ordinal.{0}} (hρ : IsIsolatingRank ρ) (hσ : IsIsolatingRank σ) (hK : BFScattered K) : (∃ β < Ordinal.omega 1, ∀ c ∈ K, ρ c < β) ↔ ∃ β < Ordinal.omega 1, ∀ c ∈ K, σ c < β

On a scattered set, two isolating ranks are bounded below ω₁ together.