Computable named-variable binders for first-order formulas

Mathlib quantification on BoundedFormula is de Bruijn; formalizations whose formulas carry named free variables (trace indices in Semantics/Composition/Reduction.lean, QBSML variables in Core/Logic/Modal/QBSML/Properties.lean) need to close a single named variable. Formula.all₁ / Formula.ex₁ do so computably (unlike mathlib's Formula.iAlls / iExs), with realization phrased via Function.update. Upstream candidates.

Main declarations

• FirstOrder.Language.Formula.all₁ / ex₁ — close the named free variable n universally / existentially.
• realize_all₁ / realize_ex₁ — realization via Function.update.
• toSentence / realize_toSentence — a formula with no occurring free variables, as a sentence.

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

Universally close the named free variable n. Computable, unlike mathlib's Formula.iAlls.

Equations

• FirstOrder.Language.Formula.all₁ n φ = (FirstOrder.Language.BoundedFormula.relabel (FirstOrder.Language.Formula.toBound✝ n) φ).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 (FirstOrder.Language.Formula.toBound✝ n) φ).ex

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)

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