Kamp, van Genabith and Reyle (2011): Discourse Representation Theory

This file formalizes the information-state architecture of the Handbook of Philosophical Logic chapter [KvGR11] on the indexed DRS substrate. Partee's marbles (42), the argument for Definition 22, are rendered minimally: two information states that determine the same proposition (Definition 23(v)) but record different witnesses for their referent, so that anaphoric potential lives strictly below truth conditions and propositions cannot be the objects of context change (marble_worlds_eq_coin, marble_ne_coin). The worked discourse (43), "John owns a donkey. It loves him.", instantiates the chapter's remark after Definition 24: applying the context change potential of the second sentence to the state the first expresses is the state of their merge (ccp_action), the second sentence being improper on its own, with its free referents supplied by the context.

References

• [KvGR11]

Partee's marbles: propositions are too coarse ((42), Definition 22)

The first sentences of (42)(i) and (ii), nine of the ten coins in the bag and one marble out against nine of the ten marbles in the bag and one coin out, are truth-conditionally equivalent but make different antecedents available for the following it. Two worlds (Bool), one live referent (Unit), two entities (Fin 2): in world true a marble (0) and a coin (1) are each missing, and the two states differ only in which one the referent carries.

def KampVanGenabithReyle2011.marbleState : DynamicSemantics.State Bool Unit (Fin 2)

(42)(i): the referent carries the missing marble 0, in world true.

Equations

• KampVanGenabithReyle2011.marbleState = {p : DynamicSemantics.Possibility Bool Unit (Part (Fin 2)) | p.world = true ∧ p.assignment () = Part.some 0}

def KampVanGenabithReyle2011.coinState : DynamicSemantics.State Bool Unit (Fin 2)

(42)(ii): the referent carries the missing coin 1, in world true.

Equations

• KampVanGenabithReyle2011.coinState = {p : DynamicSemantics.Possibility Bool Unit (Part (Fin 2)) | p.world = true ∧ p.assignment () = Part.some 1}

theorem KampVanGenabithReyle2011.marble_worlds_eq_coin : DynamicSemantics.Possibility.world '' marbleState = DynamicSemantics.Possibility.world '' coinState

The two states determine the same proposition, Definition 23(v).

theorem KampVanGenabithReyle2011.marble_ne_coin : marbleState ≠ coinState

But the states differ: the marble witness is not a coin witness. With marble_worlds_eq_coin, this is Partee's argument that context change operates on information states, not on propositions.

The action of a context change potential ((43), Definition 24)

inductive KampVanGenabithReyle2011.DRel : ℕ → Type

The relation symbols of the worked discourse (43).

• john : DRel 1
• donkey : DRel 1
• own : DRel 2
• love : DRel 2

def KampVanGenabithReyle2011.dLang : FirstOrder.Language

The first-order language of the discourse (no function symbols).

Equations

• KampVanGenabithReyle2011.dLang = { Functions := fun (x : ℕ) => Empty, Relations := KampVanGenabithReyle2011.DRel }

def KampVanGenabithReyle2011.context : DRT.DRS dLang ℕ

The context DRS of (43), "John owns a donkey.": [x y | John x, donkey y, x owns y].

Equations

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

def KampVanGenabithReyle2011.update : DRT.DRS dLang ℕ

The update DRS of (43), "It loves him.": [z u | u loves z, z = x, u = y], the pronouns resolved by equations to the context's referents.

Equations

• KampVanGenabithReyle2011.update = { referents := {2, 3}, conditions := [DRT.Condition.rel KampVanGenabithReyle2011.DRel.love ![3, 2], DRT.Condition.eq 2 0, DRT.Condition.eq 3 1] }

theorem KampVanGenabithReyle2011.context_proper : context.IsProper

The context DRS is proper.

theorem KampVanGenabithReyle2011.update_improper : ¬update.IsProper

The update DRS is not: x and y occur free in it.

theorem KampVanGenabithReyle2011.update_bound : update.freeVarFinset ⊆ context.referents

Its free referents are supplied by the context's universe, the condition under which the context change potential of Definition 24 is defined on the context's state.

theorem KampVanGenabithReyle2011.update_fresh : Disjoint update.referents (DRT.Condition.varFinsetL context.conditions)

No capture: the update introduces no referent occurring in the context.

theorem KampVanGenabithReyle2011.ccp_action {W : Type u_1} {M : Type u_2} [dLang.Structure M] : (DRT.DRS.transition W update context.referents update_bound).applyState (DRT.DRS.state W context context_proper) = DRT.DRS.state W (context.merge update) ⋯

The chapter's remark after Definition 24: applying the context change potential of the second sentence to the information state expressed by the first yields the information state expressed by their merge, the DRS of the whole discourse (43).