Fragments of L_{ω₁ω}

The foundational fragment interface of issue #13, per the frozen audit (docs/fragments-audit.md): a fragment is an arity-indexed set of formulas over Empty free variables (parameters enter semantically, through tuples), closed under CONSTRUCTOR COMPONENTS only — the direction every induction (A-elementarity, Tarski–Vaught, Löwenheim–Skolem, chain unions) consumes. Deliberately absent, per the audit: atomic-formula membership (would force countable fragments to have countable languages), formation closure under countable connectives (destroys countability), syntactic substitution closure (subsumed by semantic parameters), and formal-negation closure (an NNF concern, #14).

This is therefore not a fragment in the sense of Gao, Invariant Descriptive Set Theory (CRC Press, 2009), Definition 11.2.3, which contains the first-order formulas and is closed under Boolean operations, quantification and changes of variables. Results stated for such fragments — the fragment logic topology of Gao's Theorem 11.4.1, for instance — do not apply to a component-closed Fragment unless those closure hypotheses are supplied separately.

structure FirstOrder.Language.Fragment (L : Language) : Type (max u v)

A fragment: an arity-indexed set of L_{ω₁ω}-formulas closed under constructor components.

• toSet : Set ((n : ℕ) × L.BoundedFormulaω Empty n)

  The member formulas, tagged by arity.

• imp_left_mem {n : ℕ} {φ ψ : L.BoundedFormulaω Empty n} : ⟨n, φ.imp ψ⟩ ∈ self.toSet → ⟨n, φ⟩ ∈ self.toSet

  Component closure: the antecedent of a member implication.

• imp_right_mem {n : ℕ} {φ ψ : L.BoundedFormulaω Empty n} : ⟨n, φ.imp ψ⟩ ∈ self.toSet → ⟨n, ψ⟩ ∈ self.toSet

  Component closure: the consequent of a member implication.

• all_mem {n : ℕ} {φ : L.BoundedFormulaω Empty (n + 1)} : ⟨n, φ.all⟩ ∈ self.toSet → ⟨n + 1, φ⟩ ∈ self.toSet

  Component closure: the body of a member universal.

• iInf_mem {n : ℕ} {φs : ℕ → L.BoundedFormulaω Empty n} : ⟨n, BoundedFormulaω.iInf φs⟩ ∈ self.toSet → ∀ (k : ℕ), ⟨n, φs k⟩ ∈ self.toSet

  Component closure: every component of a member countable conjunction.

• iSup_mem {n : ℕ} {φs : ℕ → L.BoundedFormulaω Empty n} : ⟨n, BoundedFormulaω.iSup φs⟩ ∈ self.toSet → ∀ (k : ℕ), ⟨n, φs k⟩ ∈ self.toSet

  Component closure: every component of a member countable disjunction.

@[instance_reducible]

instance FirstOrder.Language.Fragment.instMembershipSigmaNatBoundedFormulaωEmpty {L : Language} : Membership ((n : ℕ) × L.BoundedFormulaω Empty n) L.Fragment

Equations

• FirstOrder.Language.Fragment.instMembershipSigmaNatBoundedFormulaωEmpty = { mem := fun (A : L.Fragment) (p : (n : ℕ) × L.BoundedFormulaω Empty n) => p ∈ A.toSet }

theorem FirstOrder.Language.Fragment.mem_def {L : Language} {A : L.Fragment} {p : (n : ℕ) × L.BoundedFormulaω Empty n} : p ∈ A ↔ p ∈ A.toSet

def FirstOrder.Language.Fragment.top {L : Language} : L.Fragment

The full fragment: every formula.

Equations

• FirstOrder.Language.Fragment.top = { toSet := Set.univ, imp_left_mem := ⋯, imp_right_mem := ⋯, all_mem := ⋯, iInf_mem := ⋯, iSup_mem := ⋯ }

def FirstOrder.Language.Fragment.inter {L : Language} (A B : L.Fragment) : L.Fragment

Fragments are closed under intersection.

Equations

• A.inter B = { toSet := A.toSet ∩ B.toSet, imp_left_mem := ⋯, imp_right_mem := ⋯, all_mem := ⋯, iInf_mem := ⋯, iSup_mem := ⋯ }

Generated fragments

inductive FirstOrder.Language.Fragment.GeneratedFrom {L : Language} (S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) : (n : ℕ) × L.BoundedFormulaω Empty n → Prop

The component-closure of a set of formulas, as an inductive reachability predicate.

• base {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {p : (n : ℕ) × L.BoundedFormulaω Empty n} (h : p ∈ S) : GeneratedFrom S p
• imp_left {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {n : ℕ} {φ ψ : L.BoundedFormulaω Empty n} : GeneratedFrom S ⟨n, φ.imp ψ⟩ → GeneratedFrom S ⟨n, φ⟩
• imp_right {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {n : ℕ} {φ ψ : L.BoundedFormulaω Empty n} : GeneratedFrom S ⟨n, φ.imp ψ⟩ → GeneratedFrom S ⟨n, ψ⟩
• all_body {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {n : ℕ} {φ : L.BoundedFormulaω Empty (n + 1)} : GeneratedFrom S ⟨n, φ.all⟩ → GeneratedFrom S ⟨n + 1, φ⟩
• iInf_comp {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {n : ℕ} {φs : ℕ → L.BoundedFormulaω Empty n} (k : ℕ) : GeneratedFrom S ⟨n, BoundedFormulaω.iInf φs⟩ → GeneratedFrom S ⟨n, φs k⟩
• iSup_comp {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {n : ℕ} {φs : ℕ → L.BoundedFormulaω Empty n} (k : ℕ) : GeneratedFrom S ⟨n, BoundedFormulaω.iSup φs⟩ → GeneratedFrom S ⟨n, φs k⟩

def FirstOrder.Language.Fragment.generated {L : Language} (S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) : L.Fragment

The generated fragment: the smallest fragment containing S.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.Fragment.subset_generated {L : Language} (S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) : S ⊆ (generated S).toSet

Set and order API

Minimal by design: SetLike, extensionality, and the order the generated/inter/top constructions already induce. Not a complete lattice — no consumer needs arbitrary suprema, and a speculative one would have to justify closure of unions, which fails.

@[instance_reducible]

instance FirstOrder.Language.Fragment.instSetLikeSigmaNatBoundedFormulaωEmpty {L : Language} : SetLike L.Fragment ((n : ℕ) × L.BoundedFormulaω Empty n)

Equations

• FirstOrder.Language.Fragment.instSetLikeSigmaNatBoundedFormulaωEmpty = { coe := fun (A : L.Fragment) => A.toSet, coe_injective := ⋯ }

theorem FirstOrder.Language.Fragment.ext {L : Language} {A B : L.Fragment} (h : ∀ (p : (n : ℕ) × L.BoundedFormulaω Empty n), p ∈ A ↔ p ∈ B) : A = B

theorem FirstOrder.Language.Fragment.ext_iff {L : Language} {A B : L.Fragment} : A = B ↔ ∀ (p : (n : ℕ) × L.BoundedFormulaω Empty n), p ∈ A ↔ p ∈ B

@[simp]

theorem FirstOrder.Language.Fragment.coe_toSet {L : Language} (A : L.Fragment) : ↑A = A.toSet

@[instance_reducible]

instance FirstOrder.Language.Fragment.instLE {L : Language} : LE L.Fragment

Equations

• FirstOrder.Language.Fragment.instLE = { le := fun (A B : L.Fragment) => A.toSet ⊆ B.toSet }

theorem FirstOrder.Language.Fragment.le_def {L : Language} {A B : L.Fragment} : A ≤ B ↔ ∀ p ∈ A, p ∈ B

@[instance_reducible]

instance FirstOrder.Language.Fragment.instTop {L : Language} : Top L.Fragment

Equations

• FirstOrder.Language.Fragment.instTop = { top := FirstOrder.Language.Fragment.top }

@[simp]

theorem FirstOrder.Language.Fragment.mem_top {L : Language} (p : (n : ℕ) × L.BoundedFormulaω Empty n) : p ∈ ⊤

@[instance_reducible]

instance FirstOrder.Language.Fragment.instMin {L : Language} : Min L.Fragment

Equations

• FirstOrder.Language.Fragment.instMin = { min := FirstOrder.Language.Fragment.inter }

@[simp]

theorem FirstOrder.Language.Fragment.mem_inf {L : Language} {A B : L.Fragment} {p : (n : ℕ) × L.BoundedFormulaω Empty n} : p ∈ A ⊓ B ↔ p ∈ A ∧ p ∈ B

theorem FirstOrder.Language.Fragment.generated_le {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {A : L.Fragment} (hSA : S ⊆ A.toSet) : (generated S).toSet ⊆ A.toSet

The generated fragment is the smallest one containing S.

theorem FirstOrder.Language.Fragment.generated_le_iff {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {A : L.Fragment} : generated S ≤ A ↔ S ⊆ ↑A

The Galois-style characterization: generated is left adjoint to the forgetful map to sets. This is the form consumers want — it replaces subset_generated/generated_le pairs at call sites.

Countability of generated fragments: the component-path encoding

def FirstOrder.Language.Fragment.componentStep {L : Language} : (n : ℕ) × L.BoundedFormulaω Empty n → ℕ × ℕ → Option ((n : ℕ) × L.BoundedFormulaω Empty n)

One component step, coded by a pair (tag, index).

Equations

• FirstOrder.Language.Fragment.componentStep ⟨n, FirstOrder.Language.BoundedFormulaInf.imp φ ψ⟩ (0, snd) = some ⟨n, φ⟩
• FirstOrder.Language.Fragment.componentStep ⟨n, FirstOrder.Language.BoundedFormulaInf.imp φ ψ⟩ (1, snd) = some ⟨n, ψ⟩
• FirstOrder.Language.Fragment.componentStep ⟨n, FirstOrder.Language.BoundedFormulaInf.all φ⟩ (2, snd) = some ⟨n + 1, φ⟩
• FirstOrder.Language.Fragment.componentStep ⟨n, FirstOrder.Language.BoundedFormulaInf.iInf φs⟩ (3, k) = some ⟨n, φs k⟩
• FirstOrder.Language.Fragment.componentStep ⟨n, FirstOrder.Language.BoundedFormulaInf.iSup φs⟩ (4, k) = some ⟨n, φs k⟩
• FirstOrder.Language.Fragment.componentStep x✝¹ x✝ = none

def FirstOrder.Language.Fragment.componentPath {L : Language} (p : (n : ℕ) × L.BoundedFormulaω Empty n) : List (ℕ × ℕ) → Option ((n : ℕ) × L.BoundedFormulaω Empty n)

Iterated component steps along a list of codes.

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.Fragment.componentPath p [] = some p

theorem FirstOrder.Language.Fragment.componentPath_append {L : Language} (p : (n : ℕ) × L.BoundedFormulaω Empty n) (l₁ l₂ : List (ℕ × ℕ)) : componentPath p (l₁ ++ l₂) = (componentPath p l₁).bind fun (x : (n : ℕ) × L.BoundedFormulaω Empty n) => componentPath x l₂

theorem FirstOrder.Language.Fragment.GeneratedFrom.of_componentStep {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {q p : (n : ℕ) × L.BoundedFormulaω Empty n} {c : ℕ × ℕ} (hq : GeneratedFrom S q) (h : componentStep q c = some p) : GeneratedFrom S p

A single step lands inside the generated set.

theorem FirstOrder.Language.Fragment.generatedFrom_iff_path {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {p : (n : ℕ) × L.BoundedFormulaω Empty n} : GeneratedFrom S p ↔ ∃ s ∈ S, ∃ (l : List (ℕ × ℕ)), componentPath s l = some p

The path characterization: the generated fragment is exactly what is reachable from S by finitely many coded component steps.

theorem FirstOrder.Language.Fragment.generated_countable {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (hS : S.Countable) : (generated S).toSet.Countable

Countability: the fragment generated by a countable set is countable.

def FirstOrder.Language.Fragment.generatedSentence {L : Language} (φ : L.Sentenceω) : L.Fragment

The generated fragment of a single sentence — countable, no hypotheses.

Equations

• FirstOrder.Language.Fragment.generatedSentence φ = FirstOrder.Language.Fragment.generated {⟨0, φ⟩}

theorem FirstOrder.Language.Fragment.generatedSentence_countable {L : Language} (φ : L.Sentenceω) : (generatedSentence φ).toSet.Countable

theorem FirstOrder.Language.Fragment.mem_generatedSentence {L : Language} (φ : L.Sentenceω) : ⟨0, φ⟩ ∈ (generatedSentence φ).toSet

def FirstOrder.Language.Fragment.generatedTheory {L : Language} (T : Set L.Sentenceω) : L.Fragment

The generated fragment of a COUNTABLE theory (the sentence case is automatic; theory countability is an assumption, per the audit).

Equations

• FirstOrder.Language.Fragment.generatedTheory T = FirstOrder.Language.Fragment.generated ((fun (φ : L.BoundedFormulaω Empty 0) => ⟨0, φ⟩) '' T)

theorem FirstOrder.Language.Fragment.generatedTheory_countable {L : Language} {T : Set L.Sentenceω} (hT : T.Countable) : (generatedTheory T).toSet.Countable

theorem FirstOrder.Language.Fragment.mem_generatedTheory {L : Language} {T : Set L.Sentenceω} {φ : L.Sentenceω} (h : φ ∈ T) : ⟨0, φ⟩ ∈ (generatedTheory T).toSet