Documentation

InfinitaryLogic.Descriptive.FiniteCarrier

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 #

Main Results #

Permutation action on finite-carrier structure space #

source
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.
source
@[simp]
theorem FirstOrder.Language.perm_smul_apply {L : Language} (n : ℕ) (σ : Equiv.Perm (Fin n)) (c : L.StructureSpaceOn (Fin n)) (R : (l : ℕ) × L.Relations l) (v : Fin R.fst → Fin n) :
(σ • c) ⟨R, v⟩ = c ⟨R, ⇑(_root_.Equiv.symm σ) ∘ v⟩
source
instance FirstOrder.Language.permMulAction {L : Language} (n : ℕ) :
MulAction (Equiv.Perm (Fin n)) (L.StructureSpaceOn (Fin n))
Equations

Isomorphism = orbit equivalence #

source
theorem FirstOrder.Language.iso_iff_orbit {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (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 #

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

The isomorphism setoid on models of φ with carrier Fin n.

Equations
Instances For

    Isomorphism relation is Borel on finite carriers #

    source
    theorem FirstOrder.Language.continuous_perm_smul {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (n : ℕ) (σ : Equiv.Perm (Fin n)) :
    Continuous fun (c : L.StructureSpaceOn (Fin n)) => σ • c

    Each orbit map c ↦ σ • c is continuous on StructureSpaceOn L (Fin n).

    source
    theorem FirstOrder.Language.isoSetoidOn_measurableSet {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (φ : L.Sentenceω) (n : ℕ) :
    MeasurableSet {p : ↑(ModelsOfOn φ) × ↑(ModelsOfOn φ) | (isoSetoidOn φ n) p.1 p.2}

    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 #

    source
    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 #

    source
    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
    Instances For
      source
      theorem FirstOrder.Language.allCodedIsoClasses_dichotomy {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (silver : SilverBurgessDichotomy) {φ : L.Sentenceω} {α : Ordinal.{0}} (hα : α < Ordinal.omega 1) (hbound : ∀ (M : Type) [inst : L.Structure M] [inst_1 : Countable M], φ.Realize M → scottHeight M ≤ α) :
      Cardinal.mk (AllCodedIsoClasses φ) ≤ Cardinal.aleph0 ∨ Cardinal.mk (AllCodedIsoClasses φ) = Cardinal.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 #

      source
      noncomputable def FirstOrder.Language.codeModel {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {φ : L.Sentenceω} {M : Type} [L.Structure M] [Countable M] (hφ : φ.Realize M) :
      AllCodedIsoClasses φ

      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
        source
        theorem FirstOrder.Language.codeModel_eq_of_iso {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {φ : L.Sentenceω} {M N : Type} [L.Structure M] [L.Structure N] [Countable M] [Countable N] (hφM : φ.Realize M) (hφN : φ.Realize N) (e : L.Equiv M N) :
        codeModel hφM = codeModel hφN

        L-isomorphic countable models map to the same coded class.

        source
        theorem FirstOrder.Language.iso_of_codeModel_eq {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {φ : L.Sentenceω} {M N : Type} [L.Structure M] [L.Structure N] [Countable M] [Countable N] (hφM : φ.Realize M) (hφN : φ.Realize N) (h : codeModel hφM = codeModel hφN) :
        Nonempty (L.Equiv M N)

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

        source
        theorem FirstOrder.Language.codeModel_surjective {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {φ : L.Sentenceω} (q : AllCodedIsoClasses φ) :
        ∃ (M : Type) (x : L.Structure M) (x_1 : Countable M) (hφ : φ.Realize M), codeModel hφ = q

        Every coded class is realized by some countable model.