Quantifier-free interpretations

An interpretation is quantifier-free when its domain and relation formulas are quantifier-free. Such interpretations preserve quantifier-free formulas under pullback and compose. This is a syntactic property, distinct from the single-input-literal restriction of a projection.

The lemmas closing quantifier-freeness goals for the formula constructors of Mathlib, the combinators of Complexity.Logics.FirstOrder.Basic and interpretations are registered in the Aesop rule set FirstOrder, used by the tactic fo_qf.

Main definitions

• Cslib.Logic.FO.Interpretation.IsQF: quantifier-free domain and relation definitions.

Main results

• Cslib.Logic.FO.Interpretation.IsQF.onFormula: pullback preserves quantifier-freeness.
• Cslib.Logic.FO.Interpretation.IsQF.comp: quantifier-free interpretations compose.
• Cslib.Logic.FO.isAtomic_varEq, Cslib.Logic.FO.isAtomic_rel₁, Cslib.Logic.FO.isAtomic_rel₂, Cslib.Logic.FO.isQF_atVar: the atomic combinators are atomic or quantifier-free.

References

• N. Immerman, Descriptive Complexity

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

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

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

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

theorem FirstOrder.Language.BoundedFormula.IsQF.iff {L : Language} {α : Type u_1} {n : ℕ} {φ ψ : L.BoundedFormula α n} (hφ : φ.IsQF) (hψ : ψ.IsQF) : (φ.iff ψ).IsQF

A biimplication of quantifier-free formulas is quantifier-free.

theorem FirstOrder.Language.BoundedFormula.IsQF.ite {L : Language} {α : Type u_1} {n : ℕ} {P : Prop} [Decidable P] {φ ψ : L.BoundedFormula α n} (hφ : φ.IsQF) (hψ : ψ.IsQF) : (if P then φ else ψ).IsQF

A conditional between quantifier-free formulas is quantifier-free.

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

Mapping relation and function symbols preserves quantifier-freeness.

theorem FirstOrder.Language.BoundedFormula.IsQF.onFormula {L : Language} {L' : Language} {α : Type u_1} {φ : L.Formula α} (h : IsQF φ) (f : L →ᴸ L') : IsQF (f.onFormula φ)

Mapping relation and function symbols of a formula preserves quantifier-freeness.

theorem FirstOrder.Language.BoundedFormula.isAtomic_rel₁ {L : Language} {α : Type u_1} {n : ℕ} (r : L.Relations 1) (t : L.Term (α ⊕ Fin n)) : (r.boundedFormula₁ t).IsAtomic

theorem FirstOrder.Language.BoundedFormula.isAtomic_rel₂ {L : Language} {α : Type u_1} {n : ℕ} (r : L.Relations 2) (t₁ t₂ : L.Term (α ⊕ Fin n)) : (r.boundedFormula₂ t₁ t₂).IsAtomic

theorem FirstOrder.Language.Formula.isAtomic_equal {L : Language} {α : Type u_1} (t₁ t₂ : L.Term α) : BoundedFormula.IsAtomic (t₁.equal t₂)

theorem FirstOrder.Language.Formula.isAtomic_rel {L : Language} {α : Type u_1} {n : ℕ} (R : L.Relations n) (ts : Fin n → L.Term α) : BoundedFormula.IsAtomic (R.formula ts)

theorem FirstOrder.Language.Formula.isAtomic_rel₁ {L : Language} {α : Type u_1} (r : L.Relations 1) (t : L.Term α) : BoundedFormula.IsAtomic (r.formula₁ t)

theorem FirstOrder.Language.Formula.isAtomic_rel₂ {L : Language} {α : Type u_1} (r : L.Relations 2) (t₁ t₂ : L.Term α) : BoundedFormula.IsAtomic (r.formula₂ t₁ t₂)

theorem FirstOrder.Language.Formula.isQF_relabel {L : Language} {α : Type u_1} {β : Type u_2} {φ : L.Formula α} (h : BoundedFormula.IsQF φ) (g : α → β) : BoundedFormula.IsQF (relabel g φ)

Relabeling the variables of a quantifier-free formula gives a quantifier-free formula.

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

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

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

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

Quantifier-free combinators

theorem Cslib.Logic.FO.isAtomic_varEq {L : FirstOrder.Language} {V : Type u_1} (u w : V) : FirstOrder.Language.BoundedFormula.IsAtomic (varEq u w)

Equality of two variables is atomic.

theorem Cslib.Logic.FO.isAtomic_rel₁ {L : FirstOrder.Language} {V : Type u_1} (r : L.Relations 1) (u : V) : FirstOrder.Language.BoundedFormula.IsAtomic (rel₁ r u)

A unary relation symbol applied to a variable is atomic.

theorem Cslib.Logic.FO.isAtomic_rel₂ {L : FirstOrder.Language} {V : Type u_1} (r : L.Relations 2) (u w : V) : FirstOrder.Language.BoundedFormula.IsAtomic (rel₂ r u w)

A binary relation symbol applied to two variables is atomic.

theorem Cslib.Logic.FO.isAtomic_lt {L : FirstOrder.Language} {V : Type u_1} (r : L.Relations 2) (u w : V) : FirstOrder.Language.BoundedFormula.IsAtomic (lt r u w)

theorem Cslib.Logic.FO.isQF_le {L : FirstOrder.Language} {V : Type u_1} (r : L.Relations 2) (u w : V) : FirstOrder.Language.BoundedFormula.IsQF (le r u w)

theorem Cslib.Logic.FO.isQF_atVar {L : FirstOrder.Language} {V : Type u_1} {φ : L.Formula (Fin 1)} (h : FirstOrder.Language.BoundedFormula.IsQF φ) (u : V) : FirstOrder.Language.BoundedFormula.IsQF (atVar φ u)

Relabeling a quantifier-free formula to a variable keeps it quantifier-free.

structure Cslib.Logic.FO.Interpretation.IsQF {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} (I : Interpretation L L' ι) : Prop

Quantifier-free interpretations have both a quantifier-free domain and quantifier-free relation definitions. This permits arbitrary Boolean combinations of input relations.

• domain : FirstOrder.Language.BoundedFormula.IsQF I.domain

  The domain introduces no quantifiers.

• rel {n : ℕ} (R : L'.Relations n) : FirstOrder.Language.BoundedFormula.IsQF (I.rel R)

  No relation definition introduces quantifiers.

theorem Cslib.Logic.FO.Interpretation.IsQF.onBoundedFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {α : Type u_3} [Finite ι] [L'.IsRelational] {I : Interpretation L L' ι} (hI : I.IsQF) {n : ℕ} {φ : L'.BoundedFormula α n} (hφ : φ.IsQF) : FirstOrder.Language.BoundedFormula.IsQF (I.onBoundedFormula φ)

theorem Cslib.Logic.FO.Interpretation.IsQF.onFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {α : Type u_3} [Finite ι] [L'.IsRelational] {I : Interpretation L L' ι} (hI : I.IsQF) {φ : L'.Formula α} (hφ : FirstOrder.Language.BoundedFormula.IsQF φ) : FirstOrder.Language.BoundedFormula.IsQF (I.onFormula φ)

Quantifier-free interpretations preserve quantifier-free formulas under pullback.

theorem Cslib.Logic.FO.Interpretation.isQF_id (L : FirstOrder.Language) : (Interpretation.id L).IsQF

theorem Cslib.Logic.FO.Interpretation.IsQF.comp {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {ι : Type u_1} {κ : Type u_2} [Finite ι] [Finite κ] [L'.IsRelational] {J : Interpretation L' L'' κ} {I : Interpretation L L' ι} (hJ : J.IsQF) (hI : I.IsQF) : (J.comp I).IsQF

Quantifier-free interpretations compose, including their relativized domains.