Pointed fragment spectra of coded classes

For a fragment F, an arity n, and a class C of coded structures, the realized spectrum Fragment.typeSpectrum F n C is the set of F-types of n-tuples of naturals in members of C, counted across the whole class: two members realizing the same type contribute one point.

• Fragment.pointedType F c a — the realized type at a tuple of a coded structure.
• pointedType_iso — pointed isomorphism invariance: an isomorphism of codes transports the type of a to the type of e ∘ a.
• pointedType_zero_eq_sentenceTheory — arity zero recovers the sentence interface.
• typeSpectrum_countable_of_determining_cover — the counting theorem: if a countable family of descriptions covers the pointed structures of C and any two pointed structures of C satisfying the same description have the same F-type, the spectrum is countable. Descriptions may overlap, need not belong to F, and carry no measurability.
• typeSpectrum_singleton_countable, typeSpectrum_isoClass — one code, hence one isomorphism class, realizes countably many types at every arity: the countably many tuples of one structure. This is the per-model count that the counting theorem is not.
• measurableSet_pointedRealize, measurable_pointedType — joint measurability in the code and the tuple, a countable union over tuples of fixed-tuple measurability.
• typeSpectrum_countable_iff_encoded — the Cantor encoding through an enumeration of the slice is a comparison theorem, secondary to the intrinsic slice-indexed type.

Empty slices, empty fragments, empty classes, and repeated coordinates are all admitted; the regression guard scripts/check_fragment_spectrum_regressions.lean exercises them. No isomorphism-invariance of C is assumed anywhere. The relation between countable spectra at every arity and thinness (scatteredness) is outside this module: the arity-zero direction follows from the sentence-spectrum characterization, and the pointed-to-unpointed bridge is a separate theorem.

Classical background: fragment types are Marker, Lectures on Infinitary Model Theory (Cambridge, 2016), Definition 2.2.19, and the Borel pointed-type map his Lemma 3.3.2; the spectrum over a class and the determining-cover packaging are as implemented here.

noncomputable def FirstOrder.Language.Fragment.pointedType {L : Language} [L.IsRelational] (F : L.Fragment) (c : L.StructureSpace) {n : ℕ} (a : Fin n → ℕ) : F.slice n → Bool

The realized F-type of a tuple of naturals in a coded structure.

Equations

• F.pointedType c a = F.realizedType ℕ a

theorem FirstOrder.Language.Fragment.pointedType_apply_iff {L : Language} [L.IsRelational] (F : L.Fragment) (c : L.StructureSpace) {n : ℕ} (a : Fin n → ℕ) (φ : F.slice n) : F.pointedType c a φ = true ↔ c ∈ ModelsOfBounded (↑φ) Empty.elim a

theorem FirstOrder.Language.Fragment.pointedType_iso {L : Language} [L.IsRelational] (F : L.Fragment) {c d : L.StructureSpace} (e : L.Equiv ℕ ℕ) {n : ℕ} (a : Fin n → ℕ) : F.pointedType d (⇑e ∘ a) = F.pointedType c a

Pointed isomorphism invariance on codes.

theorem FirstOrder.Language.Fragment.pointedType_zero_eq_sentenceTheory {L : Language} [L.IsRelational] (F : L.Fragment) (θ : ℕ → L.Sentenceω) (hθ : ∀ (k : ℕ), ⟨0, θ k⟩ ∈ F) (c : L.StructureSpace) : sentenceTheory θ c = fun (k : ℕ) => F.pointedType c Fin.elim0 ⟨θ k, ⋯⟩

Arity zero is the sentence interface: a sentence list inside F has the truth sequence read off the arity-zero pointed type.

The spectrum

def FirstOrder.Language.Fragment.typeSpectrum {L : Language} [L.IsRelational] (F : L.Fragment) (n : ℕ) (C : Set L.StructureSpace) : Set (F.slice n → Bool)

The realized spectrum of F at arity n on a class C: the types of all n-tuples of all members, counted across the class.

Equations

• F.typeSpectrum n C = (fun (p : L.StructureSpace × (Fin n → ℕ)) => F.pointedType p.1 p.2) '' C ×ˢ Set.univ

theorem FirstOrder.Language.Fragment.mem_typeSpectrum {L : Language} [L.IsRelational] {F : L.Fragment} {n : ℕ} {C : Set L.StructureSpace} {t : F.slice n → Bool} : t ∈ F.typeSpectrum n C ↔ ∃ c ∈ C, ∃ (a : Fin n → ℕ), F.pointedType c a = t

theorem FirstOrder.Language.Fragment.typeSpectrum_empty {L : Language} [L.IsRelational] (F : L.Fragment) (n : ℕ) : F.typeSpectrum n ∅ = ∅

theorem FirstOrder.Language.Fragment.typeSpectrum_mono {L : Language} [L.IsRelational] (F : L.Fragment) (n : ℕ) {C D : Set L.StructureSpace} (h : C ⊆ D) : F.typeSpectrum n C ⊆ F.typeSpectrum n D

theorem FirstOrder.Language.Fragment.typeSpectrum_singleton_countable {L : Language} [L.IsRelational] (F : L.Fragment) (n : ℕ) (c : L.StructureSpace) : (F.typeSpectrum n {c}).Countable

One code realizes countably many types: the countably many tuples of one structure. This is the per-model count, not the counting theorem.

theorem FirstOrder.Language.Fragment.typeSpectrum_isoClass {L : Language} [L.IsRelational] (F : L.Fragment) (n : ℕ) (c : L.StructureSpace) : F.typeSpectrum n {d : L.StructureSpace | L.structureIsoSetoid c d} = F.typeSpectrum n {c}

The spectrum of an isomorphism class is the spectrum of any representative.

theorem FirstOrder.Language.Fragment.typeSpectrum_isoClass_countable {L : Language} [L.IsRelational] (F : L.Fragment) (n : ℕ) (c : L.StructureSpace) : (F.typeSpectrum n {d : L.StructureSpace | L.structureIsoSetoid c d}).Countable

The counting theorem

theorem FirstOrder.Language.Fragment.typeSpectrum_countable_of_determining_cover {L : Language} [L.IsRelational] (F : L.Fragment) {n : ℕ} (C : Set L.StructureSpace) {E : Type u_1} [Countable E] (χ : E → L.BoundedFormulaω Empty n) (cover : ∀ c ∈ C, ∀ (a : Fin n → ℕ), ∃ (e : E), c ∈ ModelsOfBounded (χ e) Empty.elim a) (det : ∀ (e : E), ∀ c ∈ C, ∀ d ∈ C, ∀ (a b : Fin n → ℕ), c ∈ ModelsOfBounded (χ e) Empty.elim a → d ∈ ModelsOfBounded (χ e) Empty.elim b → ∀ (φ : F.slice n), c ∈ ModelsOfBounded (↑φ) Empty.elim a ↔ d ∈ ModelsOfBounded (↑φ) Empty.elim b) : (F.typeSpectrum n C).Countable

Countable spectrum from a determining cover. A countable family of descriptions χ e (formulas of arity n, not necessarily in F) covers the pointed structures of C, and any two pointed structures of C satisfying the same description agree on every member of the slice; then the realized spectrum of F at arity n on C is countable. Overlapping descriptions and repeated tuple coordinates are admitted; no measurability of the cover is used.

Joint measurability in the code and the tuple

theorem FirstOrder.Language.Fragment.measurableSet_pointedRealize {L : Language} [L.IsRelational] {n : ℕ} (φ : L.BoundedFormulaω Empty n) : MeasurableSet {p : L.StructureSpace × (Fin n → ℕ) | p.1 ∈ ModelsOfBounded φ Empty.elim p.2}

theorem FirstOrder.Language.Fragment.measurable_pointedType {L : Language} [L.IsRelational] (F : L.Fragment) (n : ℕ) : Measurable fun (p : L.StructureSpace × (Fin n → ℕ)) => F.pointedType p.1 p.2

The pointed type is jointly measurable in the code and the tuple.

The Cantor encoding, as a comparison

theorem FirstOrder.Language.Fragment.typeSpectrum_countable_iff_encoded {L : Language} [L.IsRelational] (F : L.Fragment) (n : ℕ) (C : Set L.StructureSpace) (s : ℕ → F.slice n) (hs : Function.Surjective s) : (F.typeSpectrum n C).Countable ↔ ((fun (t : F.slice n → Bool) => t ∘ s) '' F.typeSpectrum n C).Countable

The Cantor encoding is secondary. Through a surjective enumeration of the slice, the spectrum is countable iff its encoded image in Cantor space is: the encoding is injective on types. The surjection ℕ → F.slice n excludes an empty slice from this particular comparison; the intrinsic API above handles empty slices directly, and no padded encoding is needed.