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

In this Handbook of Philosophical Logic chapter an information state records, for each world, the witnesses of its discourse referents, so anaphoric potential lives below truth conditions and the objects of context change are information states rather than propositions. Partee's marbles (42), the argument for Definition 22, are rendered minimally as two states that determine the same proposition (Definition 23(v)) but record different witnesses for their referent. In the worked discourse (43), John owns a donkey. It loves him., applying the context change potential of the second sentence to the state the first expresses gives the state of their merge.

Main statements

• marble_worlds_eq_coin, marble_ne_coin: the two marble states determine the same proposition and differ.
• ccp_action: updating the state of the first sentence of (43) with the second is the state of their merge, as the chapter remarks after Definition 24.

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)

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

Equations

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

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

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

Equations

• KampVanGenabithReyle2011.coinState = {p : DynamicSemantics.Possibility Bool Unit (Flat (Fin 2)) | p.world = true ∧ p.assignment () = ↑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, since 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.", is [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.", is [z u | u loves z, z = x, u = y], the pronouns resolved by equations to the context's referents.

Equations

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

theorem KampVanGenabithReyle2011.context_proper : context.IsProper

The context DRS is proper.

theorem KampVanGenabithReyle2011.update_improper : ¬update.IsProper

The update DRS is not, since 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)

The update introduces no referent occurring in the context, so nothing is captured.

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) ⋯

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), as the chapter remarks after Definition 24.