Formation-closed fragments of L_{ω₁ω}

A fragment of L_{ω₁ω} is only required to be closed under taking components. A formation-closed fragment is also closed under forming formulas: it contains every atomic formula and ⊥ at every arity, and it is closed under implication, universal quantification and relabelling of bound positions (BoundedFormulaInf.mapBound, which includes weakening BoundedFormulaInf.castLE). Formation-closed fragments play the role of the fragments of Marker's Lectures on Infinitary Model Theory; they are the fragments over which consistency properties built from satisfiable theories and the omitting types theorem are set up, since forming the negation, the existential closure or a relabelling of a member must stay inside the fragment.

Marker's fragments are also closed under a formal negation and under substitution of terms. The syntax here has no formal negation: ¬φ is φ.imp ⊥, so closure under implication and containing ⊥ already give closure under negation. Closure under substitution of terms does not follow from the other conditions (substituting into a countable conjunction of members need not give a member), and it is not imposed because nothing built on formation-closed fragments here uses it.

Unlike a fragment, a formation-closed fragment determines the size of the language: every function and relation symbol occurs in an atomic member. So a formation-closed fragment has at least as many members as there are function symbols, and at least as many as there are relation symbols, and the formation closure of a countable set is countable exactly over languages with countably many function and relation symbols. A formation-closed fragment is also infinite, whatever the language: formulas are tagged with their arity, so the members ⊥ at different arities are distinct.

Main definitions

• FirstOrder.Language.Fragment.FormationClosed: a fragment containing the atomic formulas and ⊥ and closed under implication, universal quantification and relabelling.
• FirstOrder.Language.Fragment.formationClosure: the least formation-closed fragment containing a set of formulas.

Main results

• FirstOrder.Language.Fragment.FormationClosed.not_mem_iff, FirstOrder.Language.Fragment.FormationClosed.ex_mem, FirstOrder.Language.Fragment.FormationClosed.alls_mem and their companions: the derived connectives and quantifier closures of members are members.
• FirstOrder.Language.Fragment.FormationClosed.negationClosed and FirstOrder.Language.Fragment.negationClosure_le_formationClosure: a formation-closed fragment is negation-closed, so the negation closure lies below the formation closure.
• FirstOrder.Language.Fragment.formationClosure_le_iff: leastness of the formation closure.
• FirstOrder.Language.Fragment.formationClosure_countable: over a language with countably many function and relation symbols, a countable set has a countable formation closure.
• FirstOrder.Language.Fragment.FormationClosed.aleph0_le_mk: a formation-closed fragment is infinite.
• FirstOrder.Language.Fragment.FormationClosed.lift_mk_functions_le and FirstOrder.Language.Fragment.FormationClosed.lift_mk_relations_le: a formation-closed fragment has at least as many members as there are function symbols, and as there are relation symbols.
• FirstOrder.Language.Fragment.FormationClosed.countable_functions and FirstOrder.Language.Fragment.FormationClosed.countable_relations: conversely, a countable formation-closed fragment forces countably many function and relation symbols.
• FirstOrder.Language.BoundedFormulaInf.countable_setOf_isAtomic: over a countable language and countably many free variables, there are countably many atomic formulas of each arity.

References

• D. Marker, Lectures on Infinitary Model Theory, Cambridge University Press, 2016, Chapter 1.

theorem FirstOrder.Language.BoundedFormulaInf.countable_setOf_isAtomic {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} [Countable α] [Countable ((l : ℕ) × L.Functions l)] [Countable ((l : ℕ) × L.Relations l)] : {φ : L.BoundedFormulaInf ι α n | φ.IsAtomic}.Countable

Over a language with countably many function and relation symbols and a countable type of free variables, there are countably many atomic formulas with n bound positions.

structure FirstOrder.Language.Fragment.FormationClosed {L : Language} (A : L.Fragment) : Prop

A fragment is formation-closed when it contains every atomic formula and ⊥ at every arity, and is closed under implication, universal quantification and relabelling of bound positions.

• bot_mem (n : ℕ) : ⟨n, ⊥⟩ ∈ A

  ⊥ is a member at every arity.

• atomic_mem {n : ℕ} {φ : L.BoundedFormulaω Empty n} (h : BoundedFormulaInf.IsAtomic φ) : ⟨n, φ⟩ ∈ A

  Every atomic formula is a member.

• imp_mem {n : ℕ} {φ ψ : L.BoundedFormulaω Empty n} : ⟨n, φ⟩ ∈ A → ⟨n, ψ⟩ ∈ A → ⟨n, BoundedFormulaInf.imp φ ψ⟩ ∈ A

  The implication between two members is a member.

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

  The universal quantification of a member over its last bound position is a member.

• mapBound_mem {m k : ℕ} {φ : L.BoundedFormulaω Empty m} (f : Fin m → Fin k) : ⟨m, φ⟩ ∈ A → ⟨k, BoundedFormulaInf.mapBound f φ⟩ ∈ A

  Relabelling the bound positions of a member gives a member.

@[simp]

theorem FirstOrder.Language.Fragment.FormationClosed.imp_mem_iff {L : Language} {A : L.Fragment} (hA : A.FormationClosed) {n : ℕ} {φ ψ : L.BoundedFormulaω Empty n} : ⟨n, BoundedFormulaInf.imp φ ψ⟩ ∈ A ↔ ⟨n, φ⟩ ∈ A ∧ ⟨n, ψ⟩ ∈ A

An implication belongs to a formation-closed fragment exactly when both sides do.

@[simp]

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

A universal quantification belongs to a formation-closed fragment exactly when its body does.

@[simp]

theorem FirstOrder.Language.Fragment.FormationClosed.not_mem_iff {L : Language} {A : L.Fragment} (hA : A.FormationClosed) {n : ℕ} {φ : L.BoundedFormulaω Empty n} : ⟨n, BoundedFormulaInf.not φ⟩ ∈ A ↔ ⟨n, φ⟩ ∈ A

A negation belongs to a formation-closed fragment exactly when the negated formula does.

theorem FirstOrder.Language.Fragment.FormationClosed.negationClosed {L : Language} {A : L.Fragment} (hA : A.FormationClosed) : A.NegationClosed

A formation-closed fragment is negation-closed.

@[simp]

theorem FirstOrder.Language.Fragment.FormationClosed.top_mem {L : Language} {A : L.Fragment} (hA : A.FormationClosed) (n : ℕ) : ⟨n, ⊤⟩ ∈ A

⊤ is a member of a formation-closed fragment at every arity.

@[simp]

theorem FirstOrder.Language.Fragment.FormationClosed.inf_mem_iff {L : Language} {A : L.Fragment} (hA : A.FormationClosed) {n : ℕ} {φ ψ : L.BoundedFormulaω Empty n} : ⟨n, φ ⊓ ψ⟩ ∈ A ↔ ⟨n, φ⟩ ∈ A ∧ ⟨n, ψ⟩ ∈ A

A conjunction belongs to a formation-closed fragment exactly when both conjuncts do.

theorem FirstOrder.Language.Fragment.FormationClosed.inf_mem {L : Language} {A : L.Fragment} (hA : A.FormationClosed) {n : ℕ} {φ ψ : L.BoundedFormulaω Empty n} (hφ : ⟨n, φ⟩ ∈ A) (hψ : ⟨n, ψ⟩ ∈ A) : ⟨n, φ ⊓ ψ⟩ ∈ A

The conjunction of two members of a formation-closed fragment is a member.

theorem FirstOrder.Language.Fragment.FormationClosed.foldr_inf_mem {L : Language} {A : L.Fragment} (hA : A.FormationClosed) {n : ℕ} (l : List (L.BoundedFormulaω Empty n)) (h : ∀ φ ∈ l, ⟨n, φ⟩ ∈ A) : ⟨n, List.foldr (fun (x1 x2 : L.BoundedFormulaω Empty n) => x1 ⊓ x2) ⊤ l⟩ ∈ A

A finite conjunction of members of a formation-closed fragment is a member.

@[simp]

theorem FirstOrder.Language.Fragment.FormationClosed.sup_mem_iff {L : Language} {A : L.Fragment} (hA : A.FormationClosed) {n : ℕ} {φ ψ : L.BoundedFormulaω Empty n} : ⟨n, φ ⊔ ψ⟩ ∈ A ↔ ⟨n, φ⟩ ∈ A ∧ ⟨n, ψ⟩ ∈ A

A disjunction belongs to a formation-closed fragment exactly when both disjuncts do.

theorem FirstOrder.Language.Fragment.FormationClosed.sup_mem {L : Language} {A : L.Fragment} (hA : A.FormationClosed) {n : ℕ} {φ ψ : L.BoundedFormulaω Empty n} (hφ : ⟨n, φ⟩ ∈ A) (hψ : ⟨n, ψ⟩ ∈ A) : ⟨n, φ ⊔ ψ⟩ ∈ A

The disjunction of two members of a formation-closed fragment is a member.

@[simp]

theorem FirstOrder.Language.Fragment.FormationClosed.iff_mem_iff {L : Language} {A : L.Fragment} (hA : A.FormationClosed) {n : ℕ} {φ ψ : L.BoundedFormulaω Empty n} : ⟨n, BoundedFormulaInf.iff φ ψ⟩ ∈ A ↔ ⟨n, φ⟩ ∈ A ∧ ⟨n, ψ⟩ ∈ A

A biconditional belongs to a formation-closed fragment exactly when both sides do.

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

The biconditional of two members of a formation-closed fragment is a member.

@[simp]

theorem FirstOrder.Language.Fragment.FormationClosed.ex_mem_iff {L : Language} {A : L.Fragment} (hA : A.FormationClosed) {n : ℕ} {φ : L.BoundedFormulaω Empty (n + 1)} : ⟨n, BoundedFormulaInf.ex φ⟩ ∈ A ↔ ⟨n + 1, φ⟩ ∈ A

An existential quantification belongs to a formation-closed fragment exactly when its body does.

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

The existential quantification of a member of a formation-closed fragment is a member.

theorem FirstOrder.Language.Fragment.FormationClosed.alls_mem {L : Language} {A : L.Fragment} (hA : A.FormationClosed) {n : ℕ} {φ : L.BoundedFormulaω Empty n} (h : ⟨n, φ⟩ ∈ A) : ⟨0, BoundedFormulaInf.alls φ⟩ ∈ A

The universal closure of a member of a formation-closed fragment is a member.

theorem FirstOrder.Language.Fragment.FormationClosed.exs_mem {L : Language} {A : L.Fragment} (hA : A.FormationClosed) {n : ℕ} {φ : L.BoundedFormulaω Empty n} (h : ⟨n, φ⟩ ∈ A) : ⟨0, BoundedFormulaInf.exs φ⟩ ∈ A

The existential closure of a member of a formation-closed fragment is a member.

theorem FirstOrder.Language.Fragment.FormationClosed.exsLast_mem {L : Language} {A : L.Fragment} (hA : A.FormationClosed) {n k : ℕ} {φ : L.BoundedFormulaω Empty (n + k)} (h : ⟨n + k, φ⟩ ∈ A) : ⟨n, BoundedFormulaInf.exsLast φ⟩ ∈ A

Existentially quantifying the last positions of a member leaves a member.

theorem FirstOrder.Language.Fragment.FormationClosed.castLE_mem {L : Language} {A : L.Fragment} (hA : A.FormationClosed) {n m : ℕ} {φ : L.BoundedFormulaω Empty m} (hmn : m ≤ n) (h : ⟨m, φ⟩ ∈ A) : ⟨n, BoundedFormulaInf.castLE hmn φ⟩ ∈ A

Weakening a member of a formation-closed fragment to more bound positions gives a member.

theorem FirstOrder.Language.Fragment.FormationClosed.aleph0_le_mk {L : Language} {A : L.Fragment} (hA : A.FormationClosed) : Cardinal.aleph0 ≤ Cardinal.mk ↥A

A formation-closed fragment is infinite. It contains ⊥ at every arity, and these members are distinct because each formula is tagged with its arity.

theorem FirstOrder.Language.Fragment.FormationClosed.lift_mk_functions_le {L : Language} {A : L.Fragment} (hA : A.FormationClosed) : Cardinal.lift.{v, u} (Cardinal.mk ((l : ℕ) × L.Functions l)) ≤ Cardinal.mk ↥A

The function symbols are absorbed by a formation-closed fragment. There are at most as many function symbols as members: a symbol f of arity l is recovered from the atomic member f(x₀, …, xₗ₋₁) = f(x₀, …, xₗ₋₁).

theorem FirstOrder.Language.Fragment.FormationClosed.countable_functions {L : Language} {A : L.Fragment} (hA : A.FormationClosed) (hc : (↑A).Countable) : Countable ((l : ℕ) × L.Functions l)

A countable formation-closed fragment forces countably many function symbols: each occurs in an atomic member.

theorem FirstOrder.Language.Fragment.FormationClosed.lift_mk_relations_le {L : Language} {A : L.Fragment} (hA : A.FormationClosed) : Cardinal.lift.{u, v} (Cardinal.mk ((l : ℕ) × L.Relations l)) ≤ Cardinal.mk ↥A

The relation symbols are absorbed by a formation-closed fragment. There are at most as many relation symbols as members: a symbol R of arity l is recovered from the atomic member R(x₀, …, xₗ₋₁).

theorem FirstOrder.Language.Fragment.FormationClosed.countable_relations {L : Language} {A : L.Fragment} (hA : A.FormationClosed) (hc : (↑A).Countable) : Countable ((l : ℕ) × L.Relations l)

A countable formation-closed fragment forces countably many relation symbols: each occurs in an atomic member.

theorem FirstOrder.Language.Fragment.formationClosed_top {L : Language} : ⊤.FormationClosed

The top fragment, of all formulas, is formation-closed.

theorem FirstOrder.Language.Fragment.FormationClosed.sInf {L : Language} {𝒜 : Set L.Fragment} (h : ∀ A ∈ 𝒜, A.FormationClosed) : (InfSet.sInf 𝒜).FormationClosed

An intersection of formation-closed fragments is formation-closed.

theorem FirstOrder.Language.Fragment.FormationClosed.inf {L : Language} {A B : L.Fragment} (hA : A.FormationClosed) (hB : B.FormationClosed) : (A ⊓ B).FormationClosed

The intersection of two formation-closed fragments is formation-closed.

The formation closure

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

The formation closure of a set of formulas: the least formation-closed fragment containing it.

theorem FirstOrder.Language.Fragment.mem_formationClosure {L : Language} {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} {p : (n : ℕ) × L.BoundedFormulaω Empty n} : p ∈ formationClosure S ↔ ∀ (A : L.Fragment), A.FormationClosed → S ⊆ ↑A → p ∈ A

A formula belongs to the formation closure of S exactly when it belongs to every formation-closed fragment containing S.

theorem FirstOrder.Language.Fragment.formationClosed_formationClosure {L : Language} (S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) : (formationClosure S).FormationClosed

The formation closure is formation-closed.

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

A set of formulas lies in its formation closure.

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

Leastness. The formation closure of S lies below a formation-closed fragment exactly when S does.

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

The formation closure is monotone.

theorem FirstOrder.Language.Fragment.generated_le_formationClosure {L : Language} (S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) : generated S ≤ formationClosure S

The fragment generated by S lies below its formation closure.

theorem FirstOrder.Language.Fragment.negationClosure_le_formationClosure {L : Language} (S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) : negationClosure S ≤ formationClosure S

The negation closure of S lies below its formation closure.

theorem FirstOrder.Language.Fragment.FormationClosed.formationClosure_eq {L : Language} {A : L.Fragment} (hA : A.FormationClosed) : formationClosure ↑A = A

A formation-closed fragment is its own formation closure.

Countability of the formation closure

The formation closure of a countable set is the union of countably many countable stages: start from the set, the atomic formulas and ⊥ at every arity, and at each stage add the implications, universal quantifications and relabellings of members of the previous stage, closing under components.

theorem FirstOrder.Language.Fragment.formationClosure_countable {L : Language} [Countable ((l : ℕ) × L.Functions l)] [Countable ((l : ℕ) × L.Relations l)] {S : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (hS : S.Countable) : (↑(formationClosure S)).Countable

Countability. Over a language with countably many function and relation symbols, the formation closure of a countable set of formulas is countable.