Named-variable binders for first-order formulas

Mathlib's quantifiers on BoundedFormula bind de Bruijn indices, and its closures of named free variables, Formula.iAlls and Formula.iExs, are noncomputable. This file closes a single named free variable computably, with realization through Function.update; the definitions are upstream candidates.

Main definitions

• FirstOrder.Language.Formula.all₁, FirstOrder.Language.Formula.ex₁: the universal and existential closures of one named free variable.
• FirstOrder.Language.Formula.toSentence: a formula with no free variables, as a sentence.

Main results

• FirstOrder.Language.Formula.realize_all₁, FirstOrder.Language.Formula.realize_ex₁: a closure is realized when its body is at every, or some, update of the valuation; realizeAt_all₁ and realizeAt_ex₁ are the same at an index of a family of structures.

def FirstOrder.Language.Formula.all₁ {L : Language} {α : Type u_1} [DecidableEq α] (n : α) (φ : L.Formula α) : L.Formula α

Universally close the named free variable n: relabel it to the bound variable and quantify. Computable, unlike mathlib's Formula.iAlls.

Equations

• FirstOrder.Language.Formula.all₁ n φ = (FirstOrder.Language.BoundedFormula.relabel (Function.update Sum.inl n (Sum.inr 0)) φ).all

def FirstOrder.Language.Formula.ex₁ {L : Language} {α : Type u_1} [DecidableEq α] (n : α) (φ : L.Formula α) : L.Formula α

Existentially close the named free variable n. Computable, unlike mathlib's Formula.iExs.

Equations

• FirstOrder.Language.Formula.ex₁ n φ = (FirstOrder.Language.BoundedFormula.relabel (Function.update Sum.inl n (Sum.inr 0)) φ).ex

theorem FirstOrder.Language.Formula.realize_relabel_update {L : Language} {α : Type u_1} [DecidableEq α] {M : Type u_2} [L.Structure M] (n : α) (φ : L.Formula α) (v : α → M) (x : M) : (BoundedFormula.relabel (Function.update Sum.inl n (Sum.inr 0)) φ).Realize v (Fin.snoc default x) ↔ φ.Realize (Function.update v n x)

Relabeling n to the bound variable and supplying x for it is updating the valuation at n.

@[simp]

theorem FirstOrder.Language.Formula.realize_all₁ {L : Language} {α : Type u_1} [DecidableEq α] {M : Type u_2} [L.Structure M] {n : α} {φ : L.Formula α} {v : α → M} : (all₁ n φ).Realize v ↔ ∀ (x : M), φ.Realize (Function.update v n x)

@[simp]

theorem FirstOrder.Language.Formula.realize_ex₁ {L : Language} {α : Type u_1} [DecidableEq α] {M : Type u_2} [L.Structure M] {n : α} {φ : L.Formula α} {v : α → M} : (ex₁ n φ).Realize v ↔ ∃ (x : M), φ.Realize (Function.update v n x)

def FirstOrder.Language.Formula.toSentence {L : Language} {α : Type u_1} [DecidableEq α] (φ : L.Formula α) (h : BoundedFormula.freeVarFinset φ = ∅) : L.Sentence

A formula with no occurring free variables, as a sentence.

Equations

• φ.toSentence h = FirstOrder.Language.BoundedFormula.restrictFreeVar φ fun (x : ↥(FirstOrder.Language.BoundedFormula.freeVarFinset φ)) => absurd ⋯ ⋯

theorem FirstOrder.Language.Formula.realize_toSentence {L : Language} {α : Type u_1} [DecidableEq α] {M : Type u_2} [L.Structure M] (φ : L.Formula α) (h : BoundedFormula.freeVarFinset φ = ∅) (v : α → M) : M ⊨ φ.toSentence h ↔ φ.Realize v

@[simp]

theorem FirstOrder.Language.Formula.realizeAt_all₁ {L : Language} {α : Type u_1} [DecidableEq α] {W : Type u_2} {M : Type u_3} (interp : W → L.Structure M) (w : W) (v : α → M) (n : α) (φ : L.Formula α) : (all₁ n φ).RealizeAt interp w v ↔ ∀ (x : M), φ.RealizeAt interp w (Function.update v n x)

@[simp]

theorem FirstOrder.Language.Formula.realizeAt_ex₁ {L : Language} {α : Type u_1} [DecidableEq α] {W : Type u_2} {M : Type u_3} (interp : W → L.Structure M) (w : W) (v : α → M) (n : α) (φ : L.Formula α) : (ex₁ n φ).RealizeAt interp w v ↔ ∃ (x : M), φ.RealizeAt interp w (Function.update v n x)