Complexity and realization of first-order formulas

Mathlib's FirstOrder.Language.BoundedFormula.iSup and FirstOrder.Language.BoundedFormula.iInf form the disjunction and conjunction of a finite family of formulas. This file shows that both are quantifier-free when every member of the family is.

In an algebraic language, every atomic formula holds in a subsingleton structure: atomic formulas can only assert equality of terms.

Translating a formula along a language homomorphism (FirstOrder.Language.LHom.onBoundedFormula) keeps it atomic, quantifier-free or universal, and quantifying all bound variables of a universal formula (FirstOrder.Language.BoundedFormula.alls) gives a universal formula. These let universal sentences of a language be read in an extension by constants.

theorem FirstOrder.Language.BoundedFormula.IsQF.iSup {L : Language} {α : Type u_1} {β : Type u_2} {n : ℕ} [Finite β] {f : β → L.BoundedFormula α n} (hf : ∀ (b : β), (f b).IsQF) : (BoundedFormula.iSup f).IsQF

A finite disjunction of quantifier-free formulas is quantifier-free.

theorem FirstOrder.Language.BoundedFormula.IsQF.iInf {L : Language} {α : Type u_1} {β : Type u_2} {n : ℕ} [Finite β] {f : β → L.BoundedFormula α n} (hf : ∀ (b : β), (f b).IsQF) : (BoundedFormula.iInf f).IsQF

A finite conjunction of quantifier-free formulas is quantifier-free.

theorem FirstOrder.Language.BoundedFormula.realize_of_isAtomic_subsingleton {L : Language} [L.IsAlgebraic] {G : Type u_1} {α : Type u_2} [Subsingleton G] [L.Structure G] {n : ℕ} {φ : L.BoundedFormula α n} (hφ : φ.IsAtomic) (v : α → G) (xs : Fin n → G) : φ.Realize v xs

Every atomic formula over an algebraic language holds in a subsingleton structure.

theorem FirstOrder.Language.BoundedFormula.IsAtomic.onBoundedFormula {L : Language} {L' : Language} {α : Type u_1} {n : ℕ} {φ : L.BoundedFormula α n} (h : φ.IsAtomic) (ϕ : L →ᴸ L') : (ϕ.onBoundedFormula φ).IsAtomic

Translating an atomic formula along a language homomorphism gives an atomic formula.

theorem FirstOrder.Language.BoundedFormula.IsQF.onBoundedFormula {L : Language} {L' : Language} {α : Type u_1} {n : ℕ} {φ : L.BoundedFormula α n} (h : φ.IsQF) (ϕ : L →ᴸ L') : (ϕ.onBoundedFormula φ).IsQF

Translating a quantifier-free formula along a language homomorphism gives a quantifier-free formula.

theorem FirstOrder.Language.BoundedFormula.IsUniversal.onBoundedFormula {L : Language} {L' : Language} {α : Type u_1} {n : ℕ} {φ : L.BoundedFormula α n} (h : φ.IsUniversal) (ϕ : L →ᴸ L') : (ϕ.onBoundedFormula φ).IsUniversal

Translating a universal formula along a language homomorphism gives a universal formula.

theorem FirstOrder.Language.BoundedFormula.IsUniversal.alls {L : Language} {α : Type u_1} {n : ℕ} {φ : L.BoundedFormula α n} (h : φ.IsUniversal) : IsUniversal φ.alls

Universally quantifying all bound variables of a universal formula gives a universal formula.