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 on ModelsOfOn (α := Fin n) φ.
• AllCodedIsoClasses: Disjoint union of iso classes across all carrier tiers.

Main Results

• iso_iff_orbit: Isomorphism of Fin n-structures = orbit of Sym(Fin n).
• isoSetoidOn_measurableSet: The isomorphism relation on Fin 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

@[instance_reducible]

instance FirstOrder.Language.permSmul {L : Language} (n : ℕ) : SMul (Equiv.Perm (Fin n)) (L.StructureSpaceOn (Fin n))

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.

Isomorphism = orbit equivalence

theorem FirstOrder.Language.iso_iff_orbit {L : Language} [L.IsRelational] (n : ℕ) (c₁ c₂ : L.StructureSpaceOn (Fin n)) : Nonempty (L.Equiv (Fin n) (Fin n)) ↔ ∃ (σ : Equiv.Perm (Fin n)), σ • c₁ = c₂

Two Fin n-structures are L-isomorphic iff they lie in the same Sym(Fin n) orbit.

Isomorphism setoid on finite-carrier models

def FirstOrder.Language.isoSetoidOn {L : Language} [L.IsRelational] (φ : L.Sentenceω) (n : ℕ) : Setoid ↑(ModelsOfOn φ)

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

• FirstOrder.Language.isoSetoidOn φ n = Setoid.comap Subtype.val (FirstOrder.Language.structureIsoSetoidOn✝ L n)

Isomorphism relation is Borel on finite carriers

Per-tier counting dichotomy

theorem FirstOrder.Language.counting_fin_models_dichotomy {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (silver : SilverBurgessDichotomy) (φ : L.Sentenceω) (n : ℕ) : Cardinal.mk (Quotient (isoSetoidOn φ n)) ≤ Cardinal.aleph0 ∨ Cardinal.mk (Quotient (isoSetoidOn φ n)) = Cardinal.continuum

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

def FirstOrder.Language.AllCodedIsoClasses {L : Language} [L.IsRelational] (φ : L.Sentenceω) : Type v

The type of all coded isomorphism classes across all carrier tiers: ℕ-models plus Fin n-models for each n.

Equations

• FirstOrder.Language.AllCodedIsoClasses φ = (Quotient (FirstOrder.Language.isoSetoid φ) ⊕ (n : ℕ) × Quotient (FirstOrder.Language.isoSetoidOn φ n))

theorem FirstOrder.Language.mk_sigma_isoSetoidOn_le {L : Language} [L.IsRelational] (φ : L.Sentenceω) (bound : Cardinal.{v}) (hle : ∀ (n : ℕ), Cardinal.mk (Quotient (isoSetoidOn φ n)) ≤ bound) : Cardinal.mk ((n : ℕ) × Quotient (isoSetoidOn φ n)) ≤ Cardinal.aleph0 * bound

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).

Bridge theorems: coded classes represent all countable models