From DRT to predicate logic

This file translates each DRS into a mathlib FirstOrder.Language.Formula and proves that the translation's Realize coincides with Embedding.Verifies — [KR93]'s §1.5 reduction of the DRS language to first-order logic (cf. [Mus96]). The universe of a sub-DRS is existentially closed (closeExists, via Formula.iExs); the antecedent of a ⇒ is universally closed (closeForall, via Formula.iAlls).

Main declarations

• DRS.toFormula, Condition.toFormula: the translation into L.Formula V.
• DRS.realize_toFormula: truth of a DRS matches its first-order translation's Realize.
• realize_closeExists, realize_closeForall: the universe-closure operators realize as ∃/∀ over embeddings extending v on the closed referents.

def DRT.splitOn {V : Type w} [DecidableEq V] (U : Finset V) : V → V ⊕ ↥U

Relabel the free referents V so that those in U move to the bound side {x // x ∈ U} (and the rest stay free) — the splitting iExs/iAlls quantify over. DecidableEq V is needed only for the x ∈ U test, not by iExs/iAlls.

Equations

• DRT.splitOn U x = if h : x ∈ U then Sum.inr ⟨x, h⟩ else Sum.inl x

noncomputable def DRT.closeExists {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (U : Finset V) (φ : L.Formula V) : L.Formula V

Existentially close the referents in U within a formula over free referents V (relabel via splitOn, then Formula.iExs).

Equations

• DRT.closeExists U φ = FirstOrder.Language.Formula.iExs (↥U) (FirstOrder.Language.Formula.relabel (DRT.splitOn U) φ)

noncomputable def DRT.closeForall {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (U : Finset V) (φ : L.Formula V) : L.Formula V

Universally close the referents in U (used for the antecedent of ⇒).

Equations

• DRT.closeForall U φ = FirstOrder.Language.Formula.iAlls (↥U) (FirstOrder.Language.Formula.relabel (DRT.splitOn U) φ)

@[irreducible]

noncomputable def DRT.Condition.toFormula {L : FirstOrder.Language} {V : Type w} [DecidableEq V] : Condition L V → L.Formula V

Translate a single DRS-condition to a formula: each sub-box's universe is existentially closed over the conjunction of its translated conditions; the antecedent of a ⇒ is universally closed instead (§1.5).

Equations

• One or more equations did not get rendered due to their size.
• (DRT.Condition.rel R args).toFormula = R.formula fun (i : Fin n) => FirstOrder.Language.var (args i)
• (DRT.Condition.eq a b).toFormula = (FirstOrder.Language.var a).equal (FirstOrder.Language.var b)
• (DRT.Condition.neg K).toFormula = (DRT.closeExists K.referents (List.foldr (fun (x1 x2 : L.Formula V) => x1 ⊓ x2) ⊤ (List.map DRT.Condition.toFormula K.conditions))).not

noncomputable def DRT.Condition.toFormulaAll {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (cs : List (Condition L V)) : L.Formula V

The conjunction of a list of translated conditions.

Equations

• DRT.Condition.toFormulaAll cs = List.foldr (fun (x1 x2 : L.Formula V) => x1 ⊓ x2) ⊤ (List.map DRT.Condition.toFormula cs)

noncomputable def DRT.DRS.bodyFormula {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : L.Formula V

The conjunction of a DRS's conditions, without closing its universe (the antecedent body of a ⇒).

Equations

• K.bodyFormula = DRT.Condition.toFormulaAll K.conditions

noncomputable def DRT.DRS.toFormula {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : L.Formula V

Translate a DRS to a first-order formula: existentially close the universe over the conjunction of the (translated) conditions (§1.5).

Equations

• K.toFormula = DRT.closeExists K.referents (DRT.Condition.toFormulaAll K.conditions)

theorem DRT.Condition.toFormulaAll_nil {L : FirstOrder.Language} {V : Type w} [DecidableEq V] : toFormulaAll [] = ⊤

theorem DRT.Condition.toFormulaAll_cons {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (c : Condition L V) (cs : List (Condition L V)) : toFormulaAll (c :: cs) = c.toFormula ⊓ toFormulaAll cs

theorem DRT.Condition.toFormula_neg {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : (neg K).toFormula = K.toFormula.not

theorem DRT.Condition.toFormula_imp {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (a c : DRS L V) : (imp a c).toFormula = closeForall a.referents (a.bodyFormula.imp c.toFormula)

theorem DRT.Condition.toFormula_dis {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (l r : DRS L V) : (dis l r).toFormula = l.toFormula ⊔ r.toFormula

Agreement of the translation with the bespoke semantics

theorem DRT.realize_closeExists {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (U : Finset V) (φ : L.Formula V) (v : V → M) : (closeExists U φ).Realize v ↔ ∃ (v' : V → M), (∀ x ∉ U, v' x = v x) ∧ φ.Realize v'

closeExists realizes as existential quantification over embeddings that extend v on U.

theorem DRT.realize_closeForall {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (U : Finset V) (φ : L.Formula V) (v : V → M) : (closeForall U φ).Realize v ↔ ∀ (v' : V → M), (∀ x ∉ U, v' x = v x) → φ.Realize v'

closeForall realizes as universal quantification over embeddings that extend v on U.

theorem DRT.Condition.realize_toFormula {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (c : Condition L V) (v : Embedding V M) : c.toFormula.Realize v ↔ v.VerifiesCondition c

A single condition's translation realizes as VerifiesCondition.

theorem DRT.Condition.realize_toFormulaAll {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (cs : List (Condition L V)) (v : Embedding V M) : (toFormulaAll cs).Realize v ↔ ∀ c ∈ cs, v.VerifiesCondition c

A list of conditions' conjoined translation realizes as the conjunction of their realizations.

theorem DRT.DRS.realize_bodyFormula {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (K : DRS L V) (v : Embedding V M) : K.bodyFormula.Realize v ↔ v.Verifies K

The open body of a DRS (its conditions, no universe closure) realizes as Verifies of the DRS (used for the antecedent of ⇒).

theorem DRT.DRS.realize_toFormula {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (K : DRS L V) (v : Embedding V M) : K.toFormula.Realize v ↔ ∃ (v' : Embedding V M), Box.Extends K v v' ∧ v'.Verifies K

DRT ⊆ FOL (§1.5): the translated formula's Realize coincides with the bespoke Embedding.Verifies. As toFormula existentially closes the universe, the correspondence is with an embedding v' extending v over K.referents.