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

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 }

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

Countability of generated fragments: the component-path encoding

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