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

[KvGR11]

The Handbook of Philosophical Logic chapter's information-state architecture, run against the indexed substrate (Semantics/Dynamic/State.lean, DRS/Indexed.lean).

Partee's marbles ((42), the argument for Def. 22): two information states that determine the same proposition but differ — anaphoric potential lives strictly below truth conditions, so propositions cannot be the objects of context change (marble_worlds_eq_coin, marble_ne_coin).
The action equation on a discourse (p. 159): "A¹ man walked in. He₁ sat down." — applying the second sentence's transition to the state the first expresses is the state of the merge (persistence_action).

Partee's marbles: propositions are too coarse (Def. 22) #

Two worlds (Bool), one live referent (Unit), two entities (Fin 2): in world true a marble (0) and a coin (1) are each missing. "A marble is missing" and "a coin is missing" express the same proposition — true in exactly world true — but the states record different witnesses for the referent, so anaphora can distinguish them.

source

def KampVanGenabithReyle2011.marbleState :

DynamicSemantics.State Bool Unit (Fin 2)

"A marble is missing": the referent carries the marble 0, in world true.

Equations

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

Instances For

source

def KampVanGenabithReyle2011.coinState :

DynamicSemantics.State Bool Unit (Fin 2)

"A coin is missing": the referent carries the coin 1, in world true.

Equations

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

Instances For

source

theorem KampVanGenabithReyle2011.marble_worlds_eq_coin :

DynamicSemantics.Possibility.world '' marbleState = DynamicSemantics.Possibility.world '' coinState

The two states determine the same worldly content (Def. 23(v)'s proposition).

source

theorem KampVanGenabithReyle2011.marble_ne_coin :

marbleState ≠ coinState

But the states differ: the marble witness is not a coin witness. The worldly collapse (marble_worlds_eq_coin) plus this separation is Partee's argument that context change operates on information states, not propositions.