Kamp & Reyle (1993): From Discourse to Logic

[KR93]

K&R's worked examples, evaluated through the faithful model-theoretic DRS core (Semantics/Dynamic/DRS/). Each truth-condition is a theorem about the substrate denotation DRS.trueRel (Muskens's relational truth, equivalently DRS.Realize), not a local re-implementation.

Examples

1. Existential persistence: "A man walked in. He sat down." The indefinite's discourse referent persists across sentences — ∃ e, man e ∧ walked-in e ∧ sat-down e (persistence_tc).
2. Donkey anaphora: "If a farmer owns a donkey, he beats it." The implication clause (K&R Def. 1.4.4) yields the universal reading — ∀ farmer-donkey owning pairs, beats (donkey_universal_reading). The antecedent's referents are universally bound and remain accessible in the consequent.
3. Negation blocks anaphora: "A man didn't walk in. *He…" — a referent introduced under negation is inaccessible (negation_tc).
4. Subordination/accessibility (Def. 1.4.10/1.4.11): the antecedent and consequent boxes are subordinate to the donkey DRS, the consequent to the antecedent — the geometry licensing donkey anaphora.

Notes

decide handles the structural facts (subordination, the concrete model); the truth-conditions are semantic claims over arbitrary models, hence proved by unfolding the verifying-embedding/relational semantics. The merging lemma the original tested per-example (reduce_sound) is now the single substrate theorem DRS.toRel_merge; there is no .seq syntax (sequencing is DRS.merge), so the compositional-vs-merged equalities are definitional and not re-stated here.

inductive KampReyle1993.KRRel : ℕ → Type

The relation symbols of the worked examples.

• man : KRRel 1
• walkedIn : KRRel 1
• satDown : KRRel 1
• farmer : KRRel 1
• donkey : KRRel 1
• woman : KRRel 1
• owns : KRRel 2
• beats : KRRel 2
• adores : KRRel 2

def KampReyle1993.krLang : FirstOrder.Language

The first-order language of the examples (no functions).

Equations

• KampReyle1993.krLang = { Functions := fun (x : ℕ) => Empty, Relations := KampReyle1993.KRRel }

@[reducible, inline]

abbrev KampReyle1993.rm {M : Type u_1} [krLang.Structure M] {n : ℕ} (R : krLang.Relations n) (x : Fin n → M) : Prop

RelMap with the language pinned (a relation symbol alone does not determine L). Lets truth-conditions read as rm .farmer ![e].

Equations

• KampReyle1993.rm R x = FirstOrder.Language.Structure.RelMap R x

Existential persistence

def KampReyle1993.persistence : DRT.DRS krLang ℕ

"A¹ man walked in. He₁ sat down." — [u₁ | man u₁, walked-in u₁, sat-down u₁].

Equations

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

theorem KampReyle1993.persistence_tc {M : Type u_1} [krLang.Structure M] (a : ℕ → M) : persistence.trueRel a ↔ ∃ (e : M), rm KRRel.man ![e] ∧ rm KRRel.walkedIn ![e] ∧ rm KRRel.satDown ![e]

The indefinite's referent persists: truth is existential over a single entity that is a man, walked in, and sat down.

Donkey anaphora (universal reading)

def KampReyle1993.donkeyAnte : DRT.DRS krLang ℕ

The antecedent box [u₁ u₂ | farmer u₁, donkey u₂, owns u₁ u₂].

Equations

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

def KampReyle1993.donkeyCons : DRT.DRS krLang ℕ

The consequent box [ | beats u₁ u₂] (introduces no referents).

Equations

• KampReyle1993.donkeyCons = DRT.DRS.mk ∅ [DRT.Condition.rel KampReyle1993.KRRel.beats ![1, 2]]

def KampReyle1993.donkey : DRT.DRS krLang ℕ

"If a¹ farmer owns a² donkey, he₁ beats it₂." — [ | donkeyAnte ⇒ donkeyCons].

Equations

• KampReyle1993.donkey = DRT.DRS.mk ∅ [DRT.Condition.imp KampReyle1993.donkeyAnte KampReyle1993.donkeyCons]

theorem KampReyle1993.donkey_universal_reading {M : Type u_1} [krLang.Structure M] (a : ℕ → M) : donkey.trueRel a ↔ ∀ (e₁ e₂ : M), rm KRRel.farmer ![e₁] ∧ rm KRRel.donkey ![e₂] ∧ rm KRRel.owns ![e₁, e₂] → rm KRRel.beats ![e₁, e₂]

The donkey universal reading: the implication clause (K&R Def. 1.4.4) makes the antecedent's existentials universal — every owning farmer-donkey pair satisfies beats. The empty-universe consequent reuses the antecedent's values (the anaphora).

Negation blocks anaphora

def KampReyle1993.negInner : DRT.DRS krLang ℕ

"A¹ man didn't walk in." — [ | ¬[u₁ | man u₁, walked-in u₁]].

Equations

• KampReyle1993.negInner = DRT.DRS.mk {1} [DRT.Condition.rel KampReyle1993.KRRel.man ![1], DRT.Condition.rel KampReyle1993.KRRel.walkedIn ![1]]

def KampReyle1993.negation : DRT.DRS krLang ℕ

Equations

• KampReyle1993.negation = DRT.DRS.mk ∅ [DRT.Condition.neg KampReyle1993.negInner]

theorem KampReyle1993.negation_tc {M : Type u_1} [krLang.Structure M] (a : ℕ → M) : negation.trueRel a ↔ ¬∃ (e : M), rm KRRel.man ![e] ∧ rm KRRel.walkedIn ![e]

Under negation, truth is the non-existence of a verifying man — the referent is bound inside the negation and inaccessible to any continuation.

Subordination geometry (Def. 1.4.10/1.4.11)

theorem KampReyle1993.donkey_antecedent_subordinate : DRT.DirectlySubordinate donkeyAnte donkey

The antecedent box is directly subordinate to the donkey DRS.

theorem KampReyle1993.donkey_consequent_subordinate : DRT.DirectlySubordinate donkeyCons donkeyAnte

The consequent box is directly subordinate to the antecedent — the ⇒ asymmetry that makes the antecedent's referents accessible in the consequent.

Model evaluation: donkey true in a concrete model

A two-element domain where farmer 0 owns and beats donkey 1.

@[implicit_reducible]

instance KampReyle1993.instStructureKrLangFinOfNatNat : krLang.Structure (Fin 2)

Equations

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

theorem KampReyle1993.donkey_true_in_model (a : ℕ → Fin 2) : donkey.trueRel a

The donkey conditional is true in this model: the only owning pair is (0,1), which beats holds of.