Kamp & Reyle (1993): From Discourse to Logic #
@cite{kamp-reyle-1993}
End-to-end DRS analyses connecting the dynamic semantic formalism
from Core.Accessibility to empirical anaphora phenomena.
Examples #
Existential persistence (K&R Ch 1): "A man walked in. He sat down." Indefinites introduce discourse referents that persist across sentences. Truth conditions:
∃ e, man(e) ∧ walked_in(e) ∧ sat_down(e).Donkey anaphora (K&R Def 1.4.4): "If a farmer owns a donkey, he beats it." The implication verification clause yields universal quantification:
∀ e₁ e₂, (farmer(e₁) ∧ donkey(e₂) ∧ owns(e₁,e₂)) → beats(e₁,e₂).Negation blocking (K&R Ch 1): "A man didn't walk in. *He sat down." Drefs introduced under negation are not accessible.
Subordination (K&R Def 2.1.2): structural embedding governs anaphoric accessibility.
"A¹ man walked in. He₁ sat down."
Two sentences merge into a single DRS via sequencing:
[u₁ | man u₁, walked_in u₁] ; [| sat_down u₁]
After T₅ REDUCTION:
[u₁ | man u₁, walked_in u₁, sat_down u₁]
Rels: 0=man, 1=walked_in, 2=sat_down
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Cross-sentential anaphora: indefinite's dref persists.
Truth conditions for cross-sentential anaphora:
∃ e, man(e) ∧ walked_in(e) ∧ sat_down(e).
The pronoun "he" in the second sentence is resolved to the dref introduced by "a man" in the first — this is existential persistence.
"If a¹ farmer owns a² donkey, he₁ beats it₂."
The DRS [| [u₁ u₂ | farmer u₁, donkey u₂, owns u₁ u₂] ⇒ [| beats u₁ u₂]]
yields the universal reading: every farmer-donkey pair where ownership holds
also satisfies the beating relation. This is the K&R showpiece for how
dynamic implication (Def 1.4.4(f)) captures donkey anaphora without
E-type pronouns or syntactic movement.
Rels: 0=farmer, 1=donkey, 2=owns, 3=beats
Equations
- One or more equations did not get rendered due to their size.
Instances For
Donkey truth conditions: universal reading.
The dynamic implication verification clause (Def 1.4.4(f)) yields
universal quantification over farmer-donkey pairs:
∀ e₁ e₂, (farmer(e₁) ∧ donkey(e₂) ∧ owns(e₁,e₂)) → beats(e₁,e₂).
"A man didn't walk in. *He sat down."
Negation creates an inaccessible sub-DRS. The dref introduced under negation cannot be picked up by a subsequent pronoun.
[| ¬[u₁ | man u₁, walked_in u₁]]
Dref 1 occurs only inside the negated box and is NOT free in the overall DRS — the box binds it within the scope of negation. But critically, it is not accessible from outside the negation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Truth conditions under negation:
¬∃ e, man(e) ∧ walked_in(e).
The negation blocks dref accessibility: any continuation that tries to reference dref 1 would be improper.
"A¹ man met a² woman. He₁ greeted her₂."
Multiple drefs from a single sentence persist into the continuation.
[u₁ u₂ | man u₁, woman u₂, met u₁ u₂] ; [| greeted u₁ u₂]
Rels: 0=man, 1=woman, 2=met, 3=greeted
Equations
- One or more equations did not get rendered due to their size.
Instances For
Multiple drefs merge: drefs 1,2 from the first box are fresh in the (empty) continuation.
Structural subordination governs anaphoric accessibility. A sub-DRS K₁ is subordinate to K₂ when K₂'s conditions structurally contain K₁ (via negation, implication, or disjunction).
These examples verify the subordination relation for the donkey conditional, where both the antecedent and consequent boxes are subordinate to the outer DRS.
The antecedent box is immediately subordinate to the donkey DRS.
The consequent box is immediately subordinate to the donkey DRS.
The consequent is (weakly) subordinate to the antecedent's containing DRS, establishing the accessibility chain for donkey anaphora: drefs introduced in the antecedent are accessible in the consequent because both are subordinate to the same DRS.
Verification that trueIn correctly evaluates DRSs against
concrete models. These tests connect the model theory (Def 1.2.1)
to the wp truth-condition extraction.
A concrete two-element domain with farmer, donkey, owns, beats. Farmer = 0, donkey = 1. Farmer 0 owns donkey 1 and beats donkey 1.
Equations
- Phenomena.Anaphora.Studies.KampReyle1993.farmerPreds 0 args = (args = [0])
- Phenomena.Anaphora.Studies.KampReyle1993.farmerPreds 1 args = (args = [1])
- Phenomena.Anaphora.Studies.KampReyle1993.farmerPreds 2 args = (args = [0, 1])
- Phenomena.Anaphora.Studies.KampReyle1993.farmerPreds 3 args = (args = [0, 1])
- Phenomena.Anaphora.Studies.KampReyle1993.farmerPreds rel args = False
Instances For
The donkey conditional is true in the farmer model: farmer 0 owns donkey 1, and farmer 0 beats donkey 1.
End-to-end compositional derivation of "a¹ man adores a² woman".
The T₀–T₅ rules (@cite{muskens-1996}, pp. 165–167) produce a sequence of two boxes. The derivation tree yields:
[u₁ | man u₁] ; [u₂ | woman u₂, u₁ adores u₂]
T₅ REDUCTION (the merging lemma) collapses this into the standard
single-box DRS exManAdoresWoman from Core.DRSExpr.
Rels: 0=man, 1=woman, 2=adores
Equations
- One or more equations did not get rendered due to their size.
Instances For
T₅ REDUCTION: the merging lemma collapses the compositional derivation into the standard single-box DRS.
Truth conditions via the compositional route:
∃ e₁ e₂, man(e₁) ∧ woman(e₂) ∧ adores(e₁, e₂).
Harder derivations that stress-test reduce across multiple
dimensions: three-box merges, nested conditions, iterated reductions,
and multi-sentence discourses. Every merge theorem is a one-liner:
reduce_sound handles all freshness checks automatically.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Three-box merge via reduce.
Truth conditions: ∃ e₁ e₂ e₃, man(e₁) ∧ woman(e₂) ∧ book(e₃) ∧ gives(e₁,e₂,e₃)
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Merge with nested negation: dref 3 is fresh in ¬[u₂|smoke u₂, u₂=u₁].
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Merge through nested implication: dref 3 is fresh in the donkey conditional.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
K&R (1.47): merge with cross-referencing conditions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Iterated merge across a 4-sentence discourse — one line via reduce.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Merge with disjunction condition: dref 2 is fresh in the disjunction.