Muskens (1996): Combining Montague Semantics and Discourse Representation

This file formalizes the two worked developments of [muskens-1996] over the embedding of discourse representation theory in classical type theory, in which states are atomic and discourse referents are functions from states, the substrate at Semantics/Dynamic/CDRT. The compositional fragment gives lexical translations for a fragment of English with generalized coordination at every category (cn, iv, tv, detA, detEvery, detNo, andNP, orVP) and runs the paper's derivations: cross-sentential anaphora, the donkey sentence, and verb-phrase coordination with anaphora across the conjuncts. The weakest precondition calculus extracts first-order truth conditions from update meanings (wp), with the compositional rules for tests, sequencing, and random assignment (wp_test, wp_seq, wp_randomAssign), the reduction of truth to the weakest precondition of the trivial condition (wp_true_eq_closure), and the syntactic characterization of entailment (drtEntails).

Implementation notes

The paper's types translate as follows: static predicates are E → Prop, dynamic propositions are Update S, dynamic predicates take a discourse referent to an update (DynPred), and dynamic quantifiers take a dynamic predicate to an update (DynQuant). The composition rules are function application, sequencing, and abstraction and need no separate formalization.

References

• [muskens-1996]

Semantic types

@[reducible, inline]

abbrev Muskens1996.DynPred (S : Type u_4) (E : Type u_5) : Type (max u_5 u_4)

Dynamic one-place predicate: type [π] in [muskens-1996].

Equations

• Muskens1996.DynPred S E = (DynamicSemantics.Dref S E → DynamicSemantics.Update S)

@[reducible, inline]

abbrev Muskens1996.DynQuant (S : Type u_4) (E : Type u_5) : Type (max u_5 u_4)

Dynamic generalized quantifier: type [[π]] in [muskens-1996].

Equations

• Muskens1996.DynQuant S E = (Muskens1996.DynPred S E → DynamicSemantics.Update S)

T₀ basic translations

def Muskens1996.cn {S : Type u_2} {E : Type u_3} (P : E → Prop) : DynPred S E

Common noun: farmer ↝ λv[|farmer v]. Type [π].

Equations

• Muskens1996.cn P u = DynamicSemantics.Update.test (DynamicSemantics.atom1 P u)

def Muskens1996.iv {S : Type u_2} {E : Type u_3} (P : E → Prop) : DynPred S E

Intransitive verb: stink ↝ λv[|stinks v]. Type [π].

Equations

• Muskens1996.iv P u = DynamicSemantics.Update.test (DynamicSemantics.atom1 P u)

def Muskens1996.tv {S : Type u_2} {E : Type u_3} (R : E → E → Prop) : DynQuant S E → DynPred S E

Transitive verb: love ↝ λQλv(Q(λv'[|v loves v'])). Type [[π]] → [π]: takes an NP (object) and produces a VP.

Equations

• Muskens1996.tv R Q u = Q fun (v : DynamicSemantics.Dref S E) => DynamicSemantics.Update.test (DynamicSemantics.atom2 R u v)

def Muskens1996.detA {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] (u : R) : DynPred S E → DynQuant S E

Indefinite determiner: aⁿ ↝ λP'λP([uₙ]; P'(uₙ); P(uₙ)). Type [π] → [[π]]; introduces discourse referent u.

Equations

• Muskens1996.detA u noun vp = (DynamicSemantics.RegisterStructure.randomAssign u).seq ((noun (DynamicSemantics.RegisterStructure.val u)).seq (vp (DynamicSemantics.RegisterStructure.val u)))

def Muskens1996.detEvery {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] (u : R) : DynPred S E → DynQuant S E

Universal determiner: everyⁿ ↝ λP'λP(([uₙ]; P'(uₙ)) ⇒ P(uₙ)). Dynamic implication gives universal force.

Equations

• One or more equations did not get rendered due to their size.

def Muskens1996.detNo {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] (u : R) : DynPred S E → DynQuant S E

Negative determiner: noⁿ ↝ λP'λP[|not([uₙ]; P'(uₙ); P(uₙ))].

Equations

• One or more equations did not get rendered due to their size.

def Muskens1996.properNP {S : Type u_2} {E : Type u_3} (name : DynamicSemantics.Dref S E) : DynQuant S E

Proper name NP: Maryⁿ ↝ λP.P(Mary). Type [[π]].

Equations

• Muskens1996.properNP name P = P name

def Muskens1996.pro {S : Type u_2} {E : Type u_3} (u : DynamicSemantics.Dref S E) : DynQuant S E

Pronoun NP: heₙ ↝ λP.P(uₙ) — picks up the dref from the antecedent.

Equations

• Muskens1996.pro u P = P u

def Muskens1996.cond {S : Type u_2} : DynamicSemantics.Update S → DynamicSemantics.Update S → DynamicSemantics.Update S

Conditional: if ↝ λpq[|p ⇒ q].

Equations

• Muskens1996.cond p q = DynamicSemantics.Update.test (p.impl q)

def Muskens1996.auxNeg {S : Type u_2} {E : Type u_3} : DynPred S E → DynQuant S E → DynamicSemantics.Update S

Auxiliary negation: doesn't ↝ λPλQ[|not Q(P)] — takes VP (P) then subject NP (Q), matching [muskens-1996]'s argument order.

Equations

• Muskens1996.auxNeg P Q = DynamicSemantics.Update.test (Q P).neg

Generalized coordination (§IV)

and = sequencing applied pointwise; or = Update disjunction applied pointwise. The same schema works at every syntactic category.

def Muskens1996.andS {S : Type u_2} : DynamicSemantics.Update S → DynamicSemantics.Update S → DynamicSemantics.Update S

Sentence-level and: K₁ and K₂ = K₁; K₂.

Equations

• Muskens1996.andS = DynamicSemantics.Update.seq

def Muskens1996.orS {S : Type u_2} : DynamicSemantics.Update S → DynamicSemantics.Update S → DynamicSemantics.Update S

Sentence-level or: K₁ or K₂ = [K₁ or K₂] (disjunction test).

Equations

• Muskens1996.orS D₁ D₂ = DynamicSemantics.Update.test (D₁.disj D₂)

def Muskens1996.andVP {S : Type u_2} {E : Type u_3} : DynPred S E → DynPred S E → DynPred S E

VP-level and: λv(P₁(v); P₂(v)).

Equations

• Muskens1996.andVP P₁ P₂ u = (P₁ u).seq (P₂ u)

def Muskens1996.orVP {S : Type u_2} {E : Type u_3} : DynPred S E → DynPred S E → DynPred S E

VP-level or: λv[P₁(v) or P₂(v)].

Equations

• Muskens1996.orVP P₁ P₂ u = DynamicSemantics.Update.test ((P₁ u).disj (P₂ u))

def Muskens1996.andNP {S : Type u_2} {E : Type u_3} : DynQuant S E → DynQuant S E → DynQuant S E

NP-level and: λP(Q₁(P); Q₂(P)).

Equations

• Muskens1996.andNP Q₁ Q₂ P = (Q₁ P).seq (Q₂ P)

def Muskens1996.orNP {S : Type u_2} {E : Type u_3} : DynQuant S E → DynQuant S E → DynQuant S E

NP-level or: λP[Q₁(P) or Q₂(P)].

Equations

• Muskens1996.orNP Q₁ Q₂ P = DynamicSemantics.Update.test ((Q₁ P).disj (Q₂ P))

The paper's derivations

def Muskens1996.exampleText {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] (u₁ u₂ : R) (man woman : E → Prop) (adores abhors : E → E → Prop) : DynamicSemantics.Update S

"A¹ man adores a² woman. She₂ abhors him₁." — cross-sentential anaphora: [u₁]; [man u₁]; [u₂]; [woman u₂]; [u₁ adores u₂]; [u₂ abhors u₁]. The single-sentence tree is the paper's derivation (39); the man/woman/adores/ abhors box is the worked example Muskens runs the wp calculus on (p. 173), with truth conditions ∃x₁ x₂ (man x₁ ∧ woman x₂ ∧ adores x₁ x₂ ∧ abhors x₂ x₁).

Equations

• One or more equations did not get rendered due to their size.

def Muskens1996.donkeySentence {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] (u₁ u₂ : R) (farmer donkey_ : E → Prop) (owns beats : E → E → Prop) : DynamicSemantics.Update S

"Every¹ farmer who owns a² donkey beats it₂." — universal force from detEvery, anaphoric it₂ picking up the indefinite's dref: ([u₁]; [farmer u₁]; [u₂]; [donkey u₂]; [u₁ owns u₂]) ⇒ [u₁ beats u₂].

Equations

• One or more equations did not get rendered due to their size.

def Muskens1996.vpCoordExample {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] (u₁ u₂ : R) (cat fish : E → Prop) (catches eats : E → E → Prop) : DynamicSemantics.Update S

"A² cat catches a¹ fish and eats it₁." — the paper's (52), decorated as tree (56): VP coordination with cross-conjunct anaphora. andVP sequences the conjuncts, so the dref introduced by "a¹ fish" is accessible to "it₁" (contrast (53) with no¹, where it is not).

Equations

• One or more equations did not get rendered due to their size.

Weakest preconditions (§III.6)

Given an Update D and postcondition χ, wp D χ characterizes the input states from which D can transition to a state satisfying χ. The rules WP_{[]}, WP_{;} and the TR extraction rules make truth-condition computation compositional.

def Muskens1996.wp {S : Type u_2} (D : DynamicSemantics.Update S) (χ : DynamicSemantics.Condition S) : DynamicSemantics.Condition S

Weakest precondition: wp D χ i iff some output j has D i j ∧ χ j.

Equations

• Muskens1996.wp D χ i = ∃ (j : S), D i j ∧ χ j

theorem Muskens1996.wp_test {S : Type u_2} (C χ : DynamicSemantics.Condition S) : wp (DynamicSemantics.Update.test C) χ = fun (i : S) => C i ∧ χ i

WP of a test: wp [C] χ = C ∧ χ.

theorem Muskens1996.wp_seq {S : Type u_2} (D₁ D₂ : DynamicSemantics.Update S) (χ : DynamicSemantics.Condition S) : wp (D₁.seq D₂) χ = wp D₁ (wp D₂ χ)

WP of sequencing (WP_{;}): the postcondition threads through.

theorem Muskens1996.wp_randomAssign {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] (u : R) (χ : DynamicSemantics.Condition S) : wp (DynamicSemantics.RegisterStructure.randomAssign u) χ = fun (i : S) => ∃ (e : E), χ (DynamicSemantics.RegisterStructure.extend i u e)

WP of random assignment (the ∃ clause of WP_{[]}): introducing a dref existentially quantifies over its values.

theorem Muskens1996.wp_dexists {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S E] (u : R) (D : DynamicSemantics.Update S) (χ : DynamicSemantics.Condition S) : wp (DynamicSemantics.RegisterStructure.dexists u D) χ = fun (i : S) => ∃ (e : E), wp D χ (DynamicSemantics.RegisterStructure.extend i u e)

WP of existential Update: wp (∃u. D) χ = ∃e, wp D χ (extend i u e).

theorem Muskens1996.wp_true_eq_closure {S : Type u_2} (D : DynamicSemantics.Update S) : (wp D fun (x : S) => True) = D.closure

Proposition 2: wp(K, ⊤) is the existential closure ∃j K(i)(j) — truth is satisfiability. Muskens's statement carries a closedness antecedent (proper K); in the semantic formulation the identity is definitional and unconditional.

def Muskens1996.drtEntails {S : Type u_2} (premises : List (DynamicSemantics.Update S)) (conclusion : DynamicSemantics.Update S) : Prop

DRT entailment: all premises true at i force the conclusion true at i.

Equations

• Muskens1996.drtEntails premises conclusion = ∀ (i : S), (∀ D ∈ premises, D.closure i) → conclusion.closure i

theorem Muskens1996.proposition_3 {S : Type u_2} (premises : List (DynamicSemantics.Update S)) (conclusion : DynamicSemantics.Update S) : drtEntails premises conclusion ↔ ∀ (i : S), (∀ D ∈ premises, wp D (fun (x : S) => True) i) → wp conclusion (fun (x : S) => True) i

Proposition 3: DRT entailment reduces to entailment of truth conditions wp(Kᵢ, ⊤).

def Muskens1996.dplEntails {S : Type u_2} (D₁ D₂ : DynamicSemantics.Update S) : Prop

DPL-style entailment: every output of D₁ can be extended by D₂.

Equations

• Muskens1996.dplEntails D₁ D₂ = ∀ (i j : S), D₁ i j → ∃ (k : S), D₂ j k

theorem Muskens1996.dpl_entailment_eq_dimpl_valid {S : Type u_2} (D₁ D₂ : DynamicSemantics.Update S) : dplEntails D₁ D₂ ↔ ∀ (i : S), D₁.impl D₂ i

Corollary to Proposition 3: DPL entailment = validity of dynamic implication.

Truth-condition extraction rules

theorem Muskens1996.tr_neg_eq {S : Type u_2} (D : DynamicSemantics.Update S) : D.neg = fun (i : S) => ¬wp D (fun (x : S) => True) i

TR of negation: tr(not K) = ¬wp(K, ⊤).

theorem Muskens1996.tr_disj_eq {S : Type u_2} (D₁ D₂ : DynamicSemantics.Update S) : D₁.disj D₂ = fun (i : S) => wp D₁ (fun (x : S) => True) i ∨ wp D₂ (fun (x : S) => True) i

TR of disjunction: tr(K₁ or K₂) = wp(K₁, ⊤) ∨ wp(K₂, ⊤) — the existential distributes over disjunction.

theorem Muskens1996.tr_impl_eq {S : Type u_2} (D₁ D₂ : DynamicSemantics.Update S) : D₁.impl D₂ = fun (i : S) => ¬wp D₁ (fun (j : S) => ¬wp D₂ (fun (x : S) => True) j) i

TR of implication: tr(K₁ ⇒ K₂) = ¬wp(K₁, ¬wp(K₂, ⊤)) — no way to satisfy the antecedent without satisfying the consequent.

Semantic properness

def Muskens1996.isProper {S : Type u_2} (D : DynamicSemantics.Update S) : Prop

Semantic counterpart of [muskens-1996]'s properness (§III.5: a proper DRS contains no free referents): satisfiability doesn't depend on the input state. Proposition 1 connects the two — K is proper iff wp(K, ⊤) is a closed formula. The syntactic notion is strictly finer: Muskens notes a proper box and a non-proper box may have the same semantic value (his (45) vs (47)), which is why this semantic version is only a counterpart, not a reformulation.

Equations

• Muskens1996.isProper D = ∀ (i₁ i₂ : S), D.closure i₁ ↔ D.closure i₂

theorem Muskens1996.proper_wp_uniform {S : Type u_2} (D : DynamicSemantics.Update S) (h : isProper D) (i₁ i₂ : S) : wp D (fun (x : S) => True) i₁ ↔ wp D (fun (x : S) => True) i₂

Proper DRSes have state-independent weakest preconditions.

Cylindric-algebra bridges

CDRT's dref introduction and dref equality are cylindric-algebra operations under closure ([henkin-monk-tarski-1971]) — the CDRT face of the correspondence whose DPL face lives in Studies/GroenendijkStokhof1991.lean.

theorem Muskens1996.cdrt_new_seq_eq_cylindrify {E : Type u_4} (n : ℕ) (φ : CDRT.DProp E) : (CDRT.DProp.new n * φ).closure = CylindricAlgebra.cylindrify n (DynamicSemantics.Update.closure φ)

Discourse referent introduction under closure = cylindrification.

closure(new n * φ) = cₙ(closure(φ)): introducing dref n then continuing with φ equals cylindrifying φ at n.

theorem Muskens1996.cdrt_eq_dref_eq_diagonal {E : Type u_4} (i j : ℕ) : DynamicSemantics.eq' (CDRT.dref i) (CDRT.dref j) = CylindricAlgebra.diagonal i j

CDRT equality condition on drefs = diagonal element.

fn. 4: the equivalence is a fact about total assignments

[muskens-1996]'s fn. 4 scopes the SEM ≡ verification equivalence (DRS.toRel_iff_realize) to total assignments, contrasting them with [KR93]'s partial embeddings, where re-declared referents keep their values. A DRS that re-declares a referent separates the two: on [ | [x | man x] ⇒ [x | mortal x]] the agree-off-universe semantics may reassign the re-declared x, so it only demands that some mortal exist, while the persistence rendering (DRS.toRelAt, DRS/Indexed.lean) forces every man to be mortal. In a model with a non-mortal man the two truth values differ (fn4_diverges) — the witness is proper (fn4_isProper), so what fails is exactly reuse-freeness (fn4_not_reuseFreeAt), the hypothesis of the reconciliation DRS.trueRel_iff_toRelAt.

inductive Muskens1996.Fn4Rel : ℕ → Type

Relation symbols of the fn. 4 witness: man and mortal.

• man : Fn4Rel 1
• mortal : Fn4Rel 1

def Muskens1996.fn4Lang : FirstOrder.Language

The language of the fn. 4 witness (no function symbols).

Equations

• Muskens1996.fn4Lang = { Functions := fun (x : ℕ) => Empty, Relations := Muskens1996.Fn4Rel }

def Muskens1996.fn4Ante : DRT.DRS fn4Lang ℕ

The antecedent [x | man x].

Equations

• Muskens1996.fn4Ante = { referents := {0}, conditions := [DRT.Condition.rel Muskens1996.Fn4Rel.man ![0]] }

def Muskens1996.fn4Cons : DRT.DRS fn4Lang ℕ

The consequent [x | mortal x] — re-declaring x.

Equations

• Muskens1996.fn4Cons = { referents := {0}, conditions := [DRT.Condition.rel Muskens1996.Fn4Rel.mortal ![0]] }

def Muskens1996.fn4 : DRT.DRS fn4Lang ℕ

[ | [x | man x] ⇒ [x | mortal x]] with the referent 0 re-declared in the consequent.

Equations

• Muskens1996.fn4 = { referents := ∅, conditions := [DRT.Condition.imp Muskens1996.fn4Ante Muskens1996.fn4Cons] }

@[instance_reducible]

instance Muskens1996.instStructureFn4LangFinOfNatNat : fn4Lang.Structure (Fin 2)

A man (0) who is not mortal, and a mortal (1).

Equations

• One or more equations did not get rendered due to their size.

theorem Muskens1996.fn4_isProper : fn4.IsProper

The witness is proper: its referential presuppositions are satisfied.

theorem Muskens1996.fn4_not_reuseFreeAt : ¬DRT.DRS.ReuseFreeAt ∅ fn4

The witness is not reuse-free: the consequent re-declares 0.

theorem Muskens1996.fn4_trueRel (g : ℕ → Fin 2) : fn4.trueRel g

Flat truth: every input verifies the witness — the re-declared referent may be reassigned, so it suffices that some mortal exist.

theorem Muskens1996.fn4_not_toRelAt (g : ℕ → Fin 2) : ¬∃ (g' : ℕ → Fin 2), DRT.DRS.toRelAt ∅ fn4 g g'

Indexed falsity: persistence keeps the re-declared referent's man value, so no output verifies the witness in a model with a non-mortal man.

theorem Muskens1996.fn4_diverges (g : ℕ → Fin 2) : ¬(fn4.trueRel g ↔ ∃ (g' : ℕ → Fin 2), DRT.DRS.toRelAt ∅ fn4 g g')

The reconciliation DRS.trueRel_iff_toRelAt fails on the witness: flat-true, indexed-false.