Docs / Semantics / Dynamic / DRT / Translation

From DRT to predicate logic

import Linglib.Semantics.Dynamic.DRT.Translation · namespace DRT

This file translates each DRS into a FirstOrder.Language.Formula and proves that the translation is realized exactly when the DRS is verified. The universe of a sub-DRS is existentially closed (closeExists, via Formula.iExs), and the antecedent of a ⇒ universally (closeForall, via Formula.iAlls). The translation is correct for verification by total assignments, and so for truth in Kamp and Reyle's sense on proper DRSs that declare no referent twice.

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.
DRS.realize_toFormula_of_isProper: the translation of a proper DRS is realized iff some embedding verifies the DRS.

TODO

The translation of a proper DRS is closed (p. 138), so it is an L.Sentence and Def. 1.4.6's logical consequence is mathlib's ⊨ᵇ; this needs freeVarFinset lemmas for relabel, iExs and iAlls, which mathlib lacks.

References

Kamp & Reyle 1993, From Discourse to Logic formalized
Muskens 1996, Combining Montague semantics and discourse representation formalized

Declarations

L46–50

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

closeExists L52–55

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

L.Formula V

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

Built from

Used by DRS.toFormula, DRS.toFormula_eq, realize_closeExists

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

closeForall L57–59

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

L.Formula V

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

Built from

Used by Condition.toFormula, Condition.toFormula_imp, realize_closeForall

The translation of a DRS existentially closes its universe over the conjunction of its translated conditions (§1.5).

DRS.toFormula L66–69

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

DRS L V → L.Formula V

{ referents := U, conditions := cs }.toFormula = closeExists U (Condition.toFormulaAll cs)

Built from ,

Used by Condition.toFormula, DRS.toFormula_eq, Condition.toFormula_neg, Condition.toFormula_imp, Condition.toFormula_dis, DRS.realize_toFormula, DRS.realize_toFormula_of_isProper, DRS.isTrue_iff_realize_toFormula

Used in Semantics/Dynamic/DRT/Relational

The translation of a condition closes the universe of each sub-box existentially over the conjunction of its translated conditions, and that of the antecedent of a ⇒ universally (§1.5).

Condition.toFormula L70–78

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

Condition L V → L.Formula V

(Condition.atom a).toFormula = a.toFormula
(Condition.eq a b).toFormula = (FirstOrder.Language.var a).equal (FirstOrder.Language.var b)
(Condition.neg K).toFormula = K.toFormula.not
(Condition.imp { referents := Ua, conditions := ca } c).toFormula = closeForall Ua ((Condition.toFormulaAll ca).imp c.toFormula)
(Condition.dis l r).toFormula = l.toFormula ⊔ r.toFormula

Built from , ,

Used by Condition.toFormulaAll, Condition.toFormulaAll_cons, Condition.toFormula_neg, Condition.toFormula_imp, Condition.toFormula_dis, Condition.realize_toFormula

Correctness of the translation

The translation's Realize coincides with verification (§1.5). As toFormula existentially closes the universe, the correspondence is with an embedding v' extending v over K.referents.

theorem DRS.realize_toFormula L172–177

{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), K.Extends v v' ∧ VerifiesTotal v' K

Built from

The translation of a proper DRS is realized under any assignment iff some total assignment verifies the DRS in the total-assignment semantics VerifiesTotal. This is Kamp and Reyle's truth (Def. 1.4.5, DRS.IsTrue) only on a reuse-free DRS (DRS.exists_extends_verifiesTotal_iff_exists_verifies), since a referent declared twice takes a new value here and is inert there.

theorem DRS.realize_toFormula_of_isProper L179–186

{L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] {K : DRS L V} (hK : K.IsProper) (v : V → M) :

K.toFormula.Realize v ↔ ∃ (f : V → M), VerifiesTotal f K

Built from

The truth of a proper, reuse-free DRS is the truth of its first-order translation (§1.5).

theorem DRS.isTrue_iff_realize_toFormula L188–193

{L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] {K : DRS L V} (hrf : ReuseFreeAt ∅ K) (hK : K.IsProper) (f' : V → M) :

K.IsTrue M ↔ K.toFormula.Realize f'

Built from