Finite-Carrier Counting via Permutation Orbits #
This file proves that for structures on Fin n, isomorphism is the orbit
equivalence relation of Equiv.Perm (Fin n), which is Borel (finite union of
graphs of continuous maps). Combined with the existing ℕ-tier result, this
gives a counting dichotomy for all countable models.
Main Definitions #
isoSetoidOn: Isomorphism setoid onModelsOfOn (α := Fin n) φ.AllCodedIsoClasses: Disjoint union of iso classes across all carrier tiers.
Main Results #
iso_iff_orbit: Isomorphism ofFin n-structures = orbit ofSym(Fin n).isoSetoidOn_measurableSet: The isomorphism relation onFin n-models is Borel.counting_fin_models_dichotomy: Per-tier counting dichotomy.allCodedIsoClasses_dichotomy: Combined counting dichotomy for all countable models.
Permutation action on finite-carrier structure space #
Equiv.Perm (Fin n) acts on StructureSpaceOn L (Fin n) by relabeling:
(σ • c) ⟨R, v⟩ = c ⟨R, σ.symm ∘ v⟩.
Equations
- One or more equations did not get rendered due to their size.
Equations
- FirstOrder.Language.permMulAction n = { toSMul := FirstOrder.Language.permSmul n, mul_smul := ⋯, one_smul := ⋯ }
Isomorphism = orbit equivalence #
Two Fin n-structures are L-isomorphic iff they lie in the same Sym(Fin n) orbit.
Isomorphism setoid on finite-carrier models #
The ambient isomorphism relation at carrier Fin n: two codes are related iff the
structures they decode on Fin n are L-isomorphic. Stated on all of
StructureSpaceOn L (Fin n), with no reference to any sentence.
This mirrors structureIsoSetoid at the ℕ tier, and for the same reason: perfectness of a set
of codes must be a property of the ambient space, not of whichever refinement was chosen to make
one model class Polish.
Equations
- L.structureIsoSetoidOn n = { r := fun (c₁ c₂ : L.StructureSpaceOn (Fin n)) => Nonempty (L.Equiv (Fin n) (Fin n)), iseqv := ⋯ }
Instances For
The isomorphism setoid on models of φ with carrier Fin n: the ambient relation restricted
along the subtype inclusion. That is its definition, not a theorem about it.
Equations
Instances For
Membership in the pulled-back relation is membership in the ambient one.
φ has a perfect set of pairwise non-isomorphic models with carrier Fin n.
The finite tier is not decoration: an infinite language can have continuum-many Fin n models
while having no ℕ-models at all, so a counting dichotomy that only spoke about ℕ-models would
miss that case entirely.
Equations
Instances For
The ambient half of the finite-tier route: a Cantor antichain on the model class in the
ambient topology gives a perfect set of pairwise non-isomorphic Fin n-models.
StructureSpaceOn L (Fin n) is metrizable but carries no chosen metric, so the T2Space instance
that HasCantorAntichainOn.hasPerfectAntichainOn needs is produced here rather than assumed; the
topology is unchanged, so the hypothesis still applies.
The bridge to the quotient: a perfect set of pairwise non-isomorphic Fin n-models gives
continuum-many isomorphism classes at that tier.
Mirrors the ℕ-tier bridge and for the same reason: the antichain lives in the ambient space
while the quotient is over the subtype, so the transversal is transported through the inclusion —
which is what isoSetoidOn being a comap licenses.
Isomorphism relation is Borel on finite carriers #
Each orbit map c ↦ σ • c is continuous on StructureSpaceOn L (Fin n).
The isomorphism relation on Fin n-models is measurable.
It equals ⋃ σ : Perm(Fin n), graph(σ • ·), a finite union of closed sets.
Per-tier counting dichotomy #
Per-tier counting dichotomy: for each n, the iso classes among Fin n-models
of φ are either ≤ ℵ₀ or = 2^ℵ₀. Does NOT need bounded Scott height.
Combined counting theorem #
The type of all coded isomorphism classes across all carrier tiers: ℕ-models plus Fin n-models for each n.
Equations
Instances For
The finite tiers, summed: their disjoint union has at most ℵ₀ * bound classes whenever
each single tier has at most bound.
There are countably many tiers, so this is the whole of the cardinal arithmetic the counting
theorems need on the finite side. Stated once because three of them need it at two different
bounds (ℵ₀ and continuum).
Counting dichotomy for all countable models with bounded Scott height.
The type AllCodedIsoClasses φ faithfully represents all isomorphism classes of
countable models of φ (via the bridge theorems codeModel, iso_of_codeModel_eq,
codeModel_surjective).
This theorem states the dichotomy on its cardinality.
Bridge theorems: coded classes represent all countable models #
Map a countable model of φ to its coded iso class.
Uses finite_or_infinite to dispatch to the ℕ or Fin n tier.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Models mapping to the same coded class are L-isomorphic.
The proof composes: M ≃[L] carrier (from encodeViaEquiv_iso), the carrier-carrier
L-isomorphism (extracted from the quotient equality in h), and carrier ≃[L] N
(from encodeViaEquiv_iso).
Every coded class is realized by some countable model.