Model-theoretic semantics of DRSs

[KR93]

DRS truth via verifying embeddings into a mathlib FirstOrder.Language.Structure — exactly Kamp & Reyle's Def. 1.4.4–1.4.5. An embedding is an assignment v : V → M of discourse referents to the model domain; the discourse referents introduced by a sub-DRS are existentially (re)assigned when that sub-DRS is entered, which is what (∀ x ∉ K.referents, v' x = v x) expresses (v' extends v on K's universe).

Main declarations

• DRS.Realize / Condition.Realize — the verifying-embedding relation (Def. 1.4.4), reusing mathlib's Structure.RelMap for atomic conditions.
• DRS.trueIn — K is true in M iff some embedding verifies it (Def. 1.4.5).

def DRT.DRS.Realize {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] (v : V → M) : DRS L V → Prop

v verifies K ([KR93], Def. 1.4.4): every condition of K holds under the assignment v.

Equations

• DRT.DRS.Realize v (DRT.DRS.mk referents conds) = DRT.Condition.RealizeAll v conds

def DRT.Condition.Realize {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] (v : V → M) : Condition L V → Prop

v verifies a condition (Def. 1.4.4(ii)). A sub-DRS K is entered by existentially (re)assigning the referents of its universe (v' agrees with v off K.referents). For imp, the consequent witness v'' extends the antecedent assignment v' (not the host v): antecedent referents are visible in the consequent — the ⇒ accessibility asymmetry.

Equations

• One or more equations did not get rendered due to their size.
• DRT.Condition.Realize v (DRT.Condition.rel R args) = FirstOrder.Language.Structure.RelMap R fun (i : Fin n) => v (args i)
• DRT.Condition.Realize v (DRT.Condition.eq a b) = (v a = v b)
• DRT.Condition.Realize v (DRT.Condition.neg K) = ¬∃ (v' : V → M), (∀ x ∉ K.referents, v' x = v x) ∧ DRT.DRS.Realize v' K

def DRT.Condition.RealizeAll {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] (v : V → M) : List (Condition L V) → Prop

Every condition in the list is verified by v. A List helper (not List.Forall (Condition.Realize v)) because Lean's structural-recursion checker for the nested List (Condition …) rejects the higher-order argument.

Equations

• DRT.Condition.RealizeAll v [] = True
• DRT.Condition.RealizeAll v (c :: cs) = (DRT.Condition.Realize v c ∧ DRT.Condition.RealizeAll v cs)

def DRT.DRS.trueIn {L : FirstOrder.Language} {V : Type w} (M : Type x) [L.Structure M] (K : DRS L V) : Prop

K is true in M iff some embedding verifies it ([KR93], Def. 1.4.5).

Equations

• DRT.DRS.trueIn M K = ∃ (v : V → M), DRT.DRS.Realize v K