Fragments of L_{ω₁ω}

A fragment is a set of L_{ω₁ω} formulas without free variables, each tagged by its number of bound-variable slots, that is closed under taking constructor components: both sides of an implication, the body of a universal quantifier, and every member of a countable conjunction or disjunction. In this syntax, where bound variables are slots, the component relation is the subformula relation.

A fragment is not required to contain any atomic formula. Consequently the fragment generated by a countable set of formulas is countable over every language, however many symbols it has: each member is reached from a generator by a finite path of component steps, each indexed by a natural number. Closure under the formation of formulas is a separate condition, not imposed here.

Main definitions

• FirstOrder.Language.Fragment: fragments of L_{ω₁ω}, with their SetLike and complete lattice structure, meets being intersections and joins unions.
• FirstOrder.Language.Fragment.GeneratedFrom: reachability from a set of formulas by component steps.
• FirstOrder.Language.Fragment.generated: the least fragment containing a set of formulas.
• FirstOrder.Language.Fragment.ofSentence, FirstOrder.Language.Fragment.ofTheory: the fragments generated by a sentence and by a set of sentences.

Main results

• FirstOrder.Language.Fragment.generated_le_iff and FirstOrder.Language.Fragment.gc: the generated fragment is the least fragment containing its generators.
• FirstOrder.Language.Fragment.generated_countable: a countable set generates a countable fragment, with no hypothesis on the language.

References

• D. Marker, Lectures on Infinitary Model Theory, Cambridge University Press, 2016, Chapter 1.
• Ported from cameronfreer/infinitary-logic at commit 518a366cba97b1ae8c4dc64a297a396939bc3e0b, InfinitaryLogic/Lomega1omega/Fragment.lean.
• Divergences from that source: fragments form a complete lattice, built from arbitrary intersections, rather than carrying only a top element, binary meets and an order; the generated fragment is characterized by a Galois connection; the fragments of a sentence and of a theory are named ofSentence and ofTheory.

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

A fragment of L_{ω₁ω}: a set of formulas without free variables, tagged by their number of bound-variable slots, closed under taking constructor components. No atomic formula is required to belong.

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

  The formulas of the fragment, tagged by their number of bound-variable slots.

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

  The antecedent of a member implication is a member.

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

  The consequent of a member implication is a member.

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

  The body of a member universal quantification is a member.

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

  Every conjunct of a member countable conjunction is a member.

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

  Every disjunct of a member countable disjunction is a member.

@[instance_reducible]

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

@[simp]

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

The underlying set of a fragment is its coercion.

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

Membership in a fragment is membership in its underlying set.

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

Fragments with the same members are equal.

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

Closure under components

theorem FirstOrder.Language.Fragment.imp_left_mem {L : Language} (A : L.Fragment) {n : ℕ} {φ ψ : L.BoundedFormulaω Empty n} (h : ⟨n, BoundedFormulaInf.imp φ ψ⟩ ∈ A) : ⟨n, φ⟩ ∈ A

The antecedent of a member implication is a member.

theorem FirstOrder.Language.Fragment.imp_right_mem {L : Language} (A : L.Fragment) {n : ℕ} {φ ψ : L.BoundedFormulaω Empty n} (h : ⟨n, BoundedFormulaInf.imp φ ψ⟩ ∈ A) : ⟨n, ψ⟩ ∈ A

The consequent of a member implication is a member.

theorem FirstOrder.Language.Fragment.all_mem {L : Language} (A : L.Fragment) {n : ℕ} {φ : L.BoundedFormulaω Empty (n + 1)} (h : ⟨n, BoundedFormulaInf.all φ⟩ ∈ A) : ⟨n + 1, φ⟩ ∈ A

The body of a member universal quantification is a member.

theorem FirstOrder.Language.Fragment.iInf_mem {L : Language} (A : L.Fragment) {n : ℕ} {φs : ℕ → L.BoundedFormulaω Empty n} (h : ⟨n, BoundedFormulaInf.iInf φs⟩ ∈ A) (k : ℕ) : ⟨n, φs k⟩ ∈ A

Every conjunct of a member countable conjunction is a member.

theorem FirstOrder.Language.Fragment.iSup_mem {L : Language} (A : L.Fragment) {n : ℕ} {φs : ℕ → L.BoundedFormulaω Empty n} (h : ⟨n, BoundedFormulaInf.iSup φs⟩ ∈ A) (k : ℕ) : ⟨n, φs k⟩ ∈ A

Every disjunct of a member countable disjunction is a member.

The complete lattice of fragments

@[instance_reducible]

instance FirstOrder.Language.Fragment.instPartialOrder {L : Language} : PartialOrder L.Fragment

Fragments are ordered by inclusion of their underlying sets.

@[instance_reducible]

instance FirstOrder.Language.Fragment.instInfSet {L : Language} : InfSet L.Fragment

The intersection of a family of fragments is a fragment.

@[simp]

theorem FirstOrder.Language.Fragment.coe_sInf {L : Language} (𝒜 : Set L.Fragment) : ↑(sInf 𝒜) = ⋂ A ∈ 𝒜, ↑A

The underlying set of the meet of a family of fragments is the intersection.

@[simp]

theorem FirstOrder.Language.Fragment.mem_sInf {L : Language} {𝒜 : Set L.Fragment} {p : (n : ℕ) × L.BoundedFormulaω Empty n} : p ∈ sInf 𝒜 ↔ ∀ A ∈ 𝒜, p ∈ A

A formula belongs to the meet of a family of fragments exactly when it belongs to each.

@[instance_reducible]

instance FirstOrder.Language.Fragment.instCompleteLattice {L : Language} : CompleteLattice L.Fragment

Fragments form a complete lattice, whose meets are intersections.

@[simp]

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

Every formula belongs to the top fragment.

@[simp]

theorem FirstOrder.Language.Fragment.coe_top {L : Language} : ↑⊤ = Set.univ

The underlying set of the top fragment is the set of all formulas.

@[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

A formula belongs to the meet of two fragments exactly when it belongs to both.

@[simp]

theorem FirstOrder.Language.Fragment.coe_inf {L : Language} (A B : L.Fragment) : ↑(A ⊓ B) = ↑A ∩ ↑B

The underlying set of the meet of two fragments is the intersection.

@[simp]

theorem FirstOrder.Language.Fragment.coe_sSup {L : Language} (𝒜 : Set L.Fragment) : ↑(sSup 𝒜) = ⋃ A ∈ 𝒜, ↑A

The underlying set of the join of a family of fragments is the union: a union of component-closed sets is component-closed.

@[simp]

theorem FirstOrder.Language.Fragment.mem_sSup {L : Language} {𝒜 : Set L.Fragment} {p : (n : ℕ) × L.BoundedFormulaω Empty n} : p ∈ sSup 𝒜 ↔ ∃ A ∈ 𝒜, p ∈ A

A formula belongs to the join of a family of fragments exactly when it belongs to one of them.

@[simp]

theorem FirstOrder.Language.Fragment.mem_sup {L : Language} {A B : L.Fragment} {p : (n : ℕ) × L.BoundedFormulaω Empty n} : p ∈ A ⊔ B ↔ p ∈ A ∨ p ∈ B

A formula belongs to the join of two fragments exactly when it belongs to one of them.

@[simp]

theorem FirstOrder.Language.Fragment.coe_sup {L : Language} (A B : L.Fragment) : ↑(A ⊔ B) = ↑A ∪ ↑B

The underlying set of the join of two fragments is the union.

@[simp]

theorem FirstOrder.Language.Fragment.notMem_bot {L : Language} (p : (n : ℕ) × L.BoundedFormulaω Empty n) : p ∉ ⊥

No formula belongs to the bottom fragment.

@[simp]

theorem FirstOrder.Language.Fragment.coe_bot {L : Language} : ↑⊥ = ∅

The underlying set of the bottom fragment is empty.

Generated fragments

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

Reachability from a set S of formulas by finitely many component steps.

• base {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {p : (n : ℕ) × L.BoundedFormulaω Empty n} (h : p ∈ S) : GeneratedFrom S p

  Every generator is reachable.

• imp_left {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {n : ℕ} {φ ψ : L.BoundedFormulaω Empty n} : GeneratedFrom S ⟨n, BoundedFormulaInf.imp φ ψ⟩ → GeneratedFrom S ⟨n, φ⟩

  The antecedent of a reachable implication is reachable.

• imp_right {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {n : ℕ} {φ ψ : L.BoundedFormulaω Empty n} : GeneratedFrom S ⟨n, BoundedFormulaInf.imp φ ψ⟩ → GeneratedFrom S ⟨n, ψ⟩

  The consequent of a reachable implication is reachable.

• all_body {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {n : ℕ} {φ : L.BoundedFormulaω Empty (n + 1)} : GeneratedFrom S ⟨n, BoundedFormulaInf.all φ⟩ → GeneratedFrom S ⟨n + 1, φ⟩

  The body of a reachable universal quantification is reachable.

• iInf_comp {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {n : ℕ} {φs : ℕ → L.BoundedFormulaω Empty n} (k : ℕ) : GeneratedFrom S ⟨n, BoundedFormulaInf.iInf φs⟩ → GeneratedFrom S ⟨n, φs k⟩

  Every conjunct of a reachable countable conjunction is reachable.

• iSup_comp {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {n : ℕ} {φs : ℕ → L.BoundedFormulaω Empty n} (k : ℕ) : GeneratedFrom S ⟨n, BoundedFormulaInf.iSup φs⟩ → GeneratedFrom S ⟨n, φs k⟩

  Every disjunct of a reachable countable disjunction is reachable.

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

The fragment generated by a set of formulas: the formulas reachable from it by component steps.

@[simp]

theorem FirstOrder.Language.Fragment.mem_generated {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {p : (n : ℕ) × L.BoundedFormulaω Empty n} : p ∈ generated S ↔ GeneratedFrom S p

Membership in the generated fragment is reachability by component steps.

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

The generators belong to the generated fragment.

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

Leastness. The fragment generated by S lies below a fragment exactly when S does.

theorem FirstOrder.Language.Fragment.gc {L : Language} : GaloisConnection generated SetLike.coe

Generation and the underlying set form a Galois connection.

theorem FirstOrder.Language.Fragment.generated_mono {L : Language} {S T : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (h : S ⊆ T) : generated S ≤ generated T

The generated fragment is monotone in its generators.

@[simp]

theorem FirstOrder.Language.Fragment.generated_coe {L : Language} (A : L.Fragment) : generated ↑A = A

A fragment generates itself.

Countability

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

Countability. A countable set of formulas generates a countable fragment, over any language: every member is reached from a generator along a finite list of component steps, each coded by a pair of natural numbers.

The fragments of a sentence and of a theory

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

The fragment generated by a sentence.

theorem FirstOrder.Language.Fragment.ofSentence_def {L : Language} (φ : L.Sentenceω) : ofSentence φ = generated {⟨0, φ⟩}

The fragment of a sentence is the fragment generated by the sentence.

theorem FirstOrder.Language.Fragment.ofSentence_le_iff {L : Language} {φ : L.Sentenceω} {A : L.Fragment} : ofSentence φ ≤ A ↔ ⟨0, φ⟩ ∈ A

The fragment of a sentence lies below a fragment exactly when the sentence belongs to it.

theorem FirstOrder.Language.Fragment.mem_ofSentence {L : Language} (φ : L.Sentenceω) : ⟨0, φ⟩ ∈ ofSentence φ

A sentence belongs to the fragment it generates.

theorem FirstOrder.Language.Fragment.ofSentence_countable {L : Language} (φ : L.Sentenceω) : (↑(ofSentence φ)).Countable

The fragment generated by a sentence is countable, over any language.

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

The fragment generated by a set of sentences.

theorem FirstOrder.Language.Fragment.ofTheory_def {L : Language} (T : Set L.Sentenceω) : ofTheory T = generated ((fun (φ : L.BoundedFormulaω Empty 0) => ⟨0, φ⟩) '' T)

The fragment of a set of sentences is the fragment generated by its sentences.

theorem FirstOrder.Language.Fragment.ofTheory_le_iff {L : Language} {T : Set L.Sentenceω} {A : L.Fragment} : ofTheory T ≤ A ↔ ∀ φ ∈ T, ⟨0, φ⟩ ∈ A

The fragment of a set of sentences lies below a fragment exactly when each of the sentences belongs to it.

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

Every sentence of a set belongs to the fragment it generates.

theorem FirstOrder.Language.Fragment.ofTheory_mono {L : Language} {T T' : Set L.Sentenceω} (h : T ⊆ T') : ofTheory T ≤ ofTheory T'

The fragment of a set of sentences is monotone in the set.

@[simp]

theorem FirstOrder.Language.Fragment.ofTheory_singleton {L : Language} (φ : L.Sentenceω) : ofTheory {φ} = ofSentence φ

The fragment of a single sentence, as a set of sentences, is the fragment of the sentence.

theorem FirstOrder.Language.Fragment.ofTheory_countable {L : Language} {T : Set L.Sentenceω} (hT : T.Countable) : (↑(ofTheory T)).Countable

A countable set of sentences generates a countable fragment, over any language.

Arity slices

def FirstOrder.Language.Fragment.slice {L : Language} (A : L.Fragment) (n : ℕ) : Set (L.BoundedFormulaω Empty n)

The formulas of A with exactly n bound-variable slots.

@[simp]

theorem FirstOrder.Language.Fragment.mem_slice {L : Language} {A : L.Fragment} {n : ℕ} {φ : L.BoundedFormulaω Empty n} : φ ∈ A.slice n ↔ ⟨n, φ⟩ ∈ A

Membership in an arity slice is membership of the tagged formula in the fragment.

theorem FirstOrder.Language.Fragment.slice_mono {L : Language} {A B : L.Fragment} (hAB : A ≤ B) (n : ℕ) : A.slice n ⊆ B.slice n

Inclusion of fragments induces inclusion of each arity slice. The corresponding map on slice subtypes is Set.inclusion (slice_mono hAB n).

theorem FirstOrder.Language.Fragment.slice_countable {L : Language} {A : L.Fragment} (hA : (↑A).Countable) (n : ℕ) : (A.slice n).Countable

Every arity slice of a countable fragment is countable.