Extension spectra and level-by-level counting of back-and-forth classes #
Fix a family of structures M i, i : ι, of a relational language L. At an ordinal depth α
and an arity n, back-and-forth equivalence is the equivalence relation bfTupleSetoid L M α n on
the pointed tuples ⟨i, a⟩ with a : Fin n → M i, comparing tuples across all members of the
family (see TauCeti.ModelTheory.BackAndForth.Equivalence).
The depth-α extension spectrum of a pointed tuple ⟨i, a⟩ is the set of depth-α classes
of its one-point extensions ⟨i, snoc a m⟩, m : M i. Two pointed tuples are equivalent at depth
α + 1 exactly when they are equivalent at depth α and have the same extension spectrum. So the
classes at depth α + 1 inject into pairs of a class at depth α and a realized extension
spectrum, which bounds their number.
BFSmall L M collects three local conditions on the family: countably many classes of tuples at
depth 0, countably many realized extension spectra at every countable depth, and isolation of
each countable limit depth by the depths below it (Setoid.IsolatedBy). Together they give
countably many classes of tuples at every countable depth and every arity. This is the
level-by-level analysis that bounds the number of isomorphism classes of a family of countable
structures through its back-and-forth levels.
Neither of the first and last conditions is automatic. At depth 0 a tuple is classified by its
atomic type, a set of atomic formulas, so with infinitely many relation symbols there can be
continuum many classes. At a limit depth λ, countably many classes at every depth below λ do not
bound the classes at λ: a class at λ is a coherent choice of classes below λ, and a countable
product of countable sets can have the size of the continuum. Isolation is the hypothesis that
closes this gap.
Main definitions #
TauCeti.bfExtensionSpectrum L M α n x: the depth-αclasses of the one-point extensions ofx;TauCeti.bfExtensionSpectra L M α n: the realized spectra.TauCeti.BFSmall L M: the three local smallness conditions.
Main results #
TauCeti.bfTupleSetoid_add_one_iff: equivalence at depthα + 1is equivalence at depthαtogether with equality of extension spectra.TauCeti.mk_quotient_bfTupleSetoid_add_one_le: the classes at depthα + 1number at most the classes at depthαtimes the realized spectra;TauCeti.countable_quotient_bfTupleSetoid_add_oneandTauCeti.mk_quotient_bfTupleSetoid_add_one_le_of_letransfer countability and any infinite bound, such asℵ₁, one level up.TauCeti.BFSmall.countable_quotient: underBFSmall, countably many classes at every depth belowω₁and every arity.
References #
- The successor step and the smallness conditions follow Cameron Freer's
cameronfreer/infinitary-logicat commit518a366cba97b1ae8c4dc64a297a396939bc3e0b,InfinitaryLogic/ModelTheory/BFExtensionSpectrum.leanandInfinitaryLogic/ModelTheory/BFSmallCounting.lean(Apache-2.0). - Divergences from that source: the tuples range over an arbitrary family of structures rather than over coded models of a sentence, the ordinal universe of the setoids and spectra is arbitrary, and the successor bound is stated for any infinite cardinal.
The depth-α extension spectrum of a pointed tuple x = ⟨i, a⟩: the depth-α classes of
its one-point extensions ⟨i, snoc a m⟩, for m : M i.
Instances For
The realized extension spectra at depth α of the pointed n-tuples of the family.
Instances For
The class of a pointed (n + 1)-tuple lies in the extension spectrum of x exactly when the
tuple is equivalent to a one-point extension of x.
One extension spectrum is contained in another exactly when the forth condition of the
back-and-forth step holds: every one-point extension of x is matched by one of y.
The successor step. Two pointed tuples are equivalent at depth α + 1 exactly when they
are equivalent at depth α and have the same depth-α extension spectrum.
The classes at depth α + 1 inject into pairs of a class at depth α and a realized
extension spectrum.
The classes at depth α + 1 number at most the classes at depth α times the realized
extension spectra at depth α.
Countable transfer at a successor. Countably many classes and countably many realized
extension spectra at depth α give countably many classes at depth α + 1.
Cardinal transfer at a successor. If the classes and the realized extension spectra at
depth α number at most an infinite cardinal κ, such as ℵ₁, so do the classes at depth
α + 1.
Level-by-level smallness of a family of structures, with depths in Ordinal.{0}:
countably many classes of n-tuples at depth 0, countably many realized extension spectra at
every depth below ω₁, and, at every limit depth below ω₁, isolation of the classes by the
depths below it.
- zero (n : ℕ) : Countable (Quotient (bfTupleSetoid L M 0 n))
Countably many classes of
n-tuples at depth0, for every arityn. - add_one {α : Ordinal.{0}} (hα : α < Ordinal.omega 1) (n : ℕ) : (bfExtensionSpectra L M α n).Countable
Countably many realized extension spectra at every depth below
ω₁and every arity. - limit {α : Ordinal.{0}} (hα : α < Ordinal.omega 1) (hlim : Order.IsSuccLimit α) (n : ℕ) : (bfTupleSetoid L M α n).IsolatedBy fun (β : ↑(Set.Iio α)) => bfTupleSetoid L M (↑β) n
At a limit depth below
ω₁, every pointed tuple is pinned, up to equivalence at the limit depth, by its class at some smaller depth.
Instances For
Countably many classes at every countable depth. Under BFSmall, back-and-forth
equivalence at any depth below ω₁ has countably many classes of n-tuples, for every arity
n.