From DRT to predicate logic: the DRS → first-order reduction

[KR93] (§1.5), [Mus96]

The "surprise" theorem of the whole development: the bespoke DRS box language is equivalent to ordinary first-order logic. We translate each DRS into a mathlib FirstOrder.Language.Formula and prove its Realize coincides with the bespoke DRS.Realize — Kamp & Reyle's §1.5 ("From DRT to Predicate Logic") and Muskens's "DRSs are already present in classical logic", now a Lean theorem (DRS.realize_toFormula) rather than an assertion.

The universe of a (sub-)DRS is existentially closed (closeExists, via mathlib's 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 — the agreement theorem: a DRS's bespoke truth 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) φ)

noncomputable def DRT.DRS.toFormula {L : FirstOrder.Language} {V : Type w} [DecidableEq V] : 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 ([KR93] §1.5).

Equations

• (DRT.DRS.mk U conds).toFormula = DRT.closeExists U (DRT.Condition.toFormulaAll conds)

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

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

Equations

• (DRT.DRS.mk U conds).bodyFormula = DRT.Condition.toFormulaAll conds

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.

Equations

• (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 = K.toFormula.not
• (DRT.Condition.imp a c).toFormula = DRT.closeForall a.referents (a.bodyFormula.imp c.toFormula)
• (DRT.Condition.dis l r).toFormula = l.toFormula ⊔ r.toFormula

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

The conjunction of a list of (translated) conditions. A List helper — the higher-order (cs.map Condition.toFormula).foldr (· ⊓ ·) ⊤ form fails the nested-inductive structural-recursion checker.

Equations

• DRT.Condition.toFormulaAll [] = ⊤
• DRT.Condition.toFormulaAll (c :: cs) = c.toFormula ⊓ DRT.Condition.toFormulaAll cs

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.DRS.realize_toFormula {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (K : DRS L V) (v : V → M) : K.toFormula.Realize v ↔ ∃ (v' : V → M), (∀ x ∉ K.referents, v' x = v x) ∧ Realize v' K

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

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

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

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

A single condition's translation realizes as Condition.Realize.

theorem DRT.realize_toFormulaAll {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (cs : List (Condition L V)) (v : V → M) : (Condition.toFormulaAll cs).Realize v ↔ Condition.RealizeAll v cs

A list of conditions' conjoined translation realizes as RealizeAll.