Pointed fragment types

The realized type of a finite tuple in a structure, relative to a fragment F, is the truth assignment on the arity slice of F:

• Fragment.slice F n — the formulas of F at arity n, as a subtype of the existing syntax. No new syntax of types, no enumeration, and the empty slice is admitted.
• Fragment.realizedType F M a : F.slice n → Bool — which members of the slice the tuple a satisfies. At arity zero this is the truth of each sentence of F in M (realizedType_zero).
• Restriction along an inclusion of fragments is precomposition with the slice map (realizedType_le), and an isomorphism transports pointed types on the nose (realizedType_equiv).

Determining covers

Set.countable_image_of_determining_cover is the counting kernel: if countably many descriptions cover a selected set, and any two points satisfying the same description have the same invariant, the invariant takes countably many values on the set. The proof is representative-free: each description contributes a subsingleton image, and coverage puts the image inside their countable union. Descriptions may overlap. Nothing about the cover is assumed beyond coverage and determination: no measurability, no disjointness, no selector.

Reindexing need not preserve fragment membership: the reindexed formula can be built from the existing operations (openBounds, mapFreeVars, relabel), but Fragment has no reindexing closure. realizedType_reindex transports types through a supplied slice map satisfying the semantic reindexing identity; it asserts nothing about membership.

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

theorem Set.countable_image_of_determining_cover {X : Type u_1} {T : Type u_2} {E : Type u_3} [Countable E] (t : X → T) (S : Set X) (P : E → X → Prop) (cover : ∀ x ∈ S, ∃ (e : E), P e x) (det : ∀ (e : E), ∀ x ∈ S, ∀ y ∈ S, P e x → P e y → t x = t y) : (t '' S).Countable

Counting through a determining cover. Countably many descriptions P e cover S, and any two points of S satisfying the same description have the same value of t; then t takes countably many values on S. Representative-free: each description contributes a subsingleton image.

def FirstOrder.Language.Fragment.slice {L : Language} (F : L.Fragment) (n : ℕ) : Type (max u v)

The arity-n slice of a fragment: its members at arity n, as a subtype of the syntax.

Equations

• F.slice n = { φ : L.BoundedFormulaω Empty n // ⟨n, φ⟩ ∈ F }

def FirstOrder.Language.Fragment.sliceMap {L : Language} {F G : L.Fragment} (h : F ≤ G) (n : ℕ) : F.slice n → G.slice n

The slice map of an inclusion of fragments.

Equations

• FirstOrder.Language.Fragment.sliceMap h n φ = ⟨↑φ, ⋯⟩

noncomputable def FirstOrder.Language.Fragment.realizedType {L : Language} (F : L.Fragment) (M : Type w) [L.Structure M] {n : ℕ} (a : Fin n → M) : F.slice n → Bool

The realized F-type of a tuple a in M: the truth assignment on the arity slice.

Equations

• F.realizedType M a φ = decide ((↑φ).Realize Empty.elim a)

theorem FirstOrder.Language.Fragment.realizedType_apply_iff {L : Language} (F : L.Fragment) (M : Type w) [L.Structure M] {n : ℕ} (a : Fin n → M) (φ : F.slice n) : F.realizedType M a φ = true ↔ (↑φ).Realize Empty.elim a

theorem FirstOrder.Language.Fragment.realizedType_zero {L : Language} (F : L.Fragment) (M : Type w) [L.Structure M] (φ : F.slice 0) : F.realizedType M Fin.elim0 φ = true ↔ Sentenceω.Realize (↑φ) M

At arity zero the realized type is the truth of each sentence of F.

theorem FirstOrder.Language.Fragment.realizedType_le {L : Language} {F G : L.Fragment} (h : F ≤ G) (M : Type w) [L.Structure M] {n : ℕ} (a : Fin n → M) : F.realizedType M a = G.realizedType M a ∘ sliceMap h n

Restriction along an inclusion of fragments is precomposition with the slice map.

theorem FirstOrder.Language.Fragment.realizedType_equiv {L : Language} (F : L.Fragment) {M N : Type w} [L.Structure M] [L.Structure N] (e : L.Equiv M N) {n : ℕ} (a : Fin n → M) : F.realizedType N (⇑e ∘ a) = F.realizedType M a

Isomorphism invariance: an isomorphism transports pointed types on the nose.

theorem FirstOrder.Language.Fragment.realizedType_reindex {L : Language} (F : L.Fragment) (M : Type w) [L.Structure M] {m n : ℕ} (σ : Fin m → Fin n) (ρ : F.slice m → F.slice n) (hρ : ∀ (φ : F.slice m) (a : Fin n → M), (↑(ρ φ)).Realize Empty.elim a ↔ (↑φ).Realize Empty.elim (a ∘ σ)) (a : Fin n → M) : F.realizedType M (a ∘ σ) = F.realizedType M a ∘ ρ

Reindexing need not preserve fragment membership. This lemma transports types between two slices of the same F through a supplied slice map ρ satisfying the semantic reindexing identity hρ for σ : Fin m → Fin n: the type of a ∘ σ is the type of a read through ρ. Whether the reindexed formulas belong to F is exactly what ρ supplies.