Isolating ranks and the stratification of isomorphism classes #
An isolating rank assigns a countable ordinal to each relational configuration on ℕ,
is invariant under isomorphism, and isolates a configuration's isomorphism class at its rank.
Isolation is one-sided: equivalence at the rank of c decides isomorphism with c.
Any larger isomorphism-invariant countable rank is again isolating, so the contract does not
determine the rank: on a set meeting uncountably many isomorphism classes, every isolating rank
lies below one that is unbounded below ω₁ there.
The Scott height of the decoded structure is an isolating rank. Isolating ranks therefore exist for every relational language, and the stratification bound below needs no rank as input.
For an arbitrary set K of configurations, the rank descends to its isomorphism classes.
The classes of rank α inject into the back-and-forth classes of K at level α.
Consequently, if every countable level has at most ℵ₁ classes, then K meets at most
ℵ₁ isomorphism classes. In particular this holds when all these levels are countable.
No definability or invariance of K, and no countability of the language, is required.
Countably many isomorphism classes also give a countable bound on every isolating rank, so
isomorphism within K is then back-and-forth equivalence at a single countable level.
Finally, if the structures decoded from K are small level by level (TauCeti.BFSmall), then
every countable level of K has countably many classes, so K meets at most ℵ₁ isomorphism
classes.
Main results #
TauCeti.IsIsolatingRank.mk_isoClasses_le_aleph_one: the stratification bound for a given isolating rank.TauCeti.IsIsolatingRank.exists_unbounded_of_not_countable: an isolating rank can always be raised to one that is unbounded on a set meeting uncountably many classes.TauCeti.IsIsolatingRank.exists_comap_isoSetoid_eq_bfEquivSetoid: on a set meeting countably many isomorphism classes, isomorphism is back-and-forth equivalence at one countable level.TauCeti.isIsolatingRank_scottHeight: the Scott height is an isolating rank.TauCeti.mk_isoClasses_le_aleph_one_of_countable_levels: countable levels give at mostℵ₁isomorphism classes, with no rank in the statement.TauCeti.BFSmall.mk_isoClasses_le_aleph_one: level-by-level smallness of the decoded structures gives at mostℵ₁isomorphism classes.
References #
The isolating-rank contract is adapted from Cameron Freer's cameronfreer/infinitary-logic,
InfinitaryLogic/Descriptive/ScatteredCounting.lean (checkpoint 518a366, Apache-2.0).
The stratification bound is adapted from mk_isoSetoid_subtype_le_aleph_one in
InfinitaryLogic/ModelTheory/MorleyCounting.lean at the same checkpoint, replacing Scott height
with any isolating rank. The raising of an isolating rank to an unbounded one follows
IsIsolatingRank.exists_unbounded_of_not_countable in ScatteredCounting.lean, and the bound
from level-by-level smallness follows mk_representedIn_le_aleph_one_of_bfSmall in
InfinitaryLogic/ModelTheory/BFSmallCounting.lean, both at the same checkpoint; there the rank
instance is a stabilization ordinal rather than the Scott height. For Morley's counting argument,
see Antonio Montalbán, Computable Structure Theory: Beyond the Arithmetic, Chapter XII.
A countable, isomorphism-invariant rank that isolates each configuration's isomorphism class at its own back-and-forth level. It need not be the least such level.
- iso_invariant ⦃c d : RelationalConfiguration L ℕ⦄ : (RelationalConfiguration.isoSetoid L ℕ) c d → ρ c = ρ d
Isomorphic configurations have equal ranks.
Every rank is a countable ordinal.
- isolates ⦃c d : RelationalConfiguration L ℕ⦄ : (RelationalConfiguration.bfEquivSetoid L ℕ (ρ c)) c d → (RelationalConfiguration.isoSetoid L ℕ) c d
Back-and-forth equivalence at the rank of the first configuration decides isomorphism.
Instances For
An isomorphism-invariant rank induced on the isomorphism classes represented in K.
Instances For
The induced rank still takes only countable values.
Isolation holds at every level at or above the rank of the first configuration.
Raising an isolating rank to an invariant countable rank preserves isolation.
The contract does not bound the rank. On a set K meeting uncountably many isomorphism
classes, every isolating rank lies below an isolating rank that takes values at or above every
countable ordinal on K.
On a set where the rank is bounded by α, isomorphism equals equivalence at level α.
No definability or invariance of the set is needed.
A rank stratum of isomorphism classes injects into the quotient at that level. This is the step that makes it possible to count classes stratum by stratum.
If every countable level of K has at most ℵ₁ classes, then K meets at most ℵ₁
isomorphism classes. The set K need not be Borel or isomorphism invariant.
Countably many classes at each countable back-and-forth level give at most ℵ₁
isomorphism classes, for any isolating rank.
Countably many isomorphism classes bound every invariant countable rank strictly below one countable ordinal. Neither isolation nor smallness of the levels is required.
On a set meeting countably many isomorphism classes, isomorphism is back-and-forth equivalence at a single countable level. The set itself may be uncountable.
The Scott height as an isolating rank #
The Scott height is an isolating rank. The Scott height of the structure decoded from a
configuration on ℕ is invariant under isomorphism and countable, and back-and-forth
equivalence of the empty tuples at the Scott height of c decides isomorphism with c.
Every relational language has an isolating rank on its configurations on ℕ.
The stratification bound. If every countable back-and-forth level of a set K of
configurations on ℕ has countably many classes, then K meets at most ℵ₁ isomorphism
classes. The set K need not be Borel or isomorphism invariant, and the language need not be
countable.
Level-by-level smallness bounds the isomorphism classes. If the structures decoded from a
set K of configurations on ℕ are small level by level (TauCeti.BFSmall), then K meets at
most ℵ₁ isomorphism classes.