Kamp and Reyle (1993): From Discourse to Logic

A discourse is interpreted by constructing a discourse representation structure (DRS), and a DRS is verified by an embedding of its referents into a model. The worked examples are evaluated through DRS.trueRel, Muskens's relational truth, which is the existential closure of the book's Def. 1.4.5.

Main statements

• ulysses_tc: Jones owns Ulysses. It fascinates him. (1.1) is true of a single owning pair, the pronoun equations adding no quantificational force.
• porsche_tc, porsche_referent_inaccessible: Jones does not own a Porsche. (1.56) denies a verifying extension, and the referent under the negation is inaccessible from the top level.
• donkey_universal_reading, donkeyPronoun_agree: If a farmer owns a donkey he beats it. (2.47) gets its universal reading from the verification clause for ⇒, whether or not the pronoun has a referent of its own.

Implementation notes

The truth conditions are claims over arbitrary models, proved by unfolding the verifying embeddings; sequencing a discourse is DRS.merge, whose dynamics is the Merging Lemma DRS.toRel_merge. Names enter a DRS as the unary conditions the construction algorithm writes for them.

References

• [KR93]
• [Mus96]
• [GBM24]

inductive KampReyle1993.KRRel : ℕ → Type

The relation symbols of the worked examples; names (jones, ulysses, porsche) enter as the unary conditions the construction algorithm writes for them (Jones(x)).

• jones : KRRel 1
• ulysses : KRRel 1
• porsche : KRRel 1
• farmer : KRRel 1
• donkey : KRRel 1
• owns : KRRel 2
• fascinates : KRRel 2
• beats : 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

Names and pronouns: "Jones owns Ulysses. It fascinates him." (1.1)

def KampReyle1993.ulyssesDiscourse : DRT.DRS krLang ℕ

The completed §1.1 DRS of (1.1), [u₁ u₂ u₃ u₄ | Jones u₁, Ulysses u₂, u₁ owns u₂, u₃ = u₂, u₄ = u₁, u₃ fascinates u₄]. Each name and pronoun introduces a referent, and the (1.17)-style equations resolve it and him to the first sentence's referents.

Equations

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

theorem KampReyle1993.ulysses_tc {M : Type u_1} [krLang.Structure M] (a : ℕ → M) : ulyssesDiscourse.trueRel a ↔ ∃ (x : M) (y : M), rm KRRel.jones ![x] ∧ rm KRRel.ulysses ![y] ∧ rm KRRel.owns ![x, y] ∧ rm KRRel.fascinates ![y, x]

The (1.1) discourse is true iff a single pair verifies both sentences, since the pronouns' referents and equations add no quantificational force and the first sentence's referents persist into the second.

theorem KampReyle1993.ulysses_proper : ulyssesDiscourse.IsProper

The completed (1.1) DRS is proper (Def. 1.4.2–1.4.3), every referent its conditions use being introduced by the discourse itself.

Negation blocks anaphora: "Jones does not own a Porsche." (1.56)

def KampReyle1993.porscheNeg : DRT.DRS krLang ℕ

The box under ¬ in (1.57) is [u₂ | Porsche u₂, u₁ owns u₂].

Equations

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

def KampReyle1993.porscheDiscourse : DRT.DRS krLang ℕ

The DRS (1.57) of (1.56), [u₁ | Jones u₁, ¬[u₂ | Porsche u₂, u₁ owns u₂]], introduces the indefinite's referent inside the negation.

Equations

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

theorem KampReyle1993.porsche_tc {M : Type u_1} [krLang.Structure M] (a : ℕ → M) : porscheDiscourse.trueRel a ↔ ∃ (x : M), rm KRRel.jones ![x] ∧ ¬∃ (y : M), rm KRRel.porsche ![y] ∧ rm KRRel.owns ![x, y]

(1.57) is true when there is no Porsche that Jones owns, the negated box being verified by the non-existence of a verifying extension.

theorem KampReyle1993.porsche_referent_inaccessible : ¬porscheDiscourse.Accessible 1 2

From the top-level position, the referent trapped under ¬ is not accessible (Def. 2.1.3) — the reason a continuation "*It fascinates him." cannot resolve it.

theorem KampReyle1993.outer_referent_accessible : porscheDiscourse.Accessible 2 1

Accessibility looks left and up, so from inside the negation the outer referent is accessible, the asymmetry of Def. 2.1.3.

theorem KampReyle1993.continuation_improper : ¬(porscheDiscourse.merge { referents := ∅, conditions := [DRT.Condition.atom { arity := 2, rel := KRRel.fascinates, args := ![2, 1] }] }).IsProper

A continuation resolved to the trapped referent anyway is improper (Def. 1.4.2–1.4.3), since merging It fascinates him with it forced to u₂ leaves u₂ free.

Donkey anaphora: "If a farmer owns a donkey he beats it." (2.47)

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₂] (pronouns resolved directly, (2.44)-style).

Equations

• KampReyle1993.donkeyCons = { referents := ∅, conditions := [DRT.Condition.atom { arity := 2, rel := KampReyle1993.KRRel.beats, args := ![1, 2] }] }

def KampReyle1993.donkey : DRT.DRS krLang ℕ

(2.47) as [ | donkeyAnte ⇒ donkeyCons].

Equations

• KampReyle1993.donkey = { referents := ∅, conditions := [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 verification clause for ⇒ ((2.31), Def. 2.1.4) makes the antecedent's existentials universal, so every owning farmer–donkey pair satisfies beats. The consequent, with an empty universe, reuses the antecedent's values.

theorem KampReyle1993.donkey_proper : donkey.IsProper

The donkey DRS is proper, the antecedent supplying the consequent's referents.

def KampReyle1993.donkeyPronounCons : DRT.DRS krLang ℕ

The (2.45)-style consequent [u₃ | u₃ = u₂, beats u₁ u₃], in which the pronoun it introduces its own referent, resolved to the donkey by an equation.

Equations

• KampReyle1993.donkeyPronounCons = { referents := {3}, conditions := [DRT.Condition.eq 3 2, DRT.Condition.atom { arity := 2, rel := KampReyle1993.KRRel.beats, args := ![1, 3] }] }

def KampReyle1993.donkeyPronoun : DRT.DRS krLang ℕ

(2.47) with the pronoun completed by referent-plus-equation.

Equations

• KampReyle1993.donkeyPronoun = { referents := ∅, conditions := [DRT.Condition.imp KampReyle1993.donkeyAnte KampReyle1993.donkeyPronounCons] }

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

The pronoun-completed conditional has the same universal truth conditions, the equation forcing the new referent to the donkey's value.

theorem KampReyle1993.donkeyPronoun_agree {M : Type u_1} [krLang.Structure M] (a : ℕ → M) : donkeyPronoun.trueRel a ↔ donkey.trueRel a

Completing the pronoun directly or by a referent and an equation gives the donkey conditional the same truth conditions, as the book observes of (2.44) and (2.45).

Subordination and accessibility geometry

theorem KampReyle1993.donkey_antecedent_subordinate : DRT.DirectlySubordinate donkeyAnte donkey

The antecedent box is directly subordinate to the donkey DRS (Def. 1.4.10 as extended by Def. 2.1.2).

theorem KampReyle1993.donkey_consequent_subordinate : DRT.DirectlySubordinate donkeyCons donkey

The consequent box is likewise directly subordinate to the donkey DRS.

theorem KampReyle1993.donkey_antecedent_accessible : DRT.AccessibleTo donkey donkeyAnte donkeyCons

The antecedent is accessible to the consequent ([GBM24] §4.2) — the geometry that licenses the donkey anaphora.

theorem KampReyle1993.donkey_not_consequent_accessible : ¬DRT.AccessibleTo donkey donkeyCons donkeyAnte

The consequent is not among the boxes accessible at the antecedent, the ⇒ asymmetry.

Model evaluation: the donkey conditional in concrete models

Positive: a two-element domain where farmer 0 owns and beats donkey 1. Negative: a domain where the owning pair goes unbeaten falsifies the conditional.

@[instance_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, whose only owning pair (0, 1) is a beating pair.

@[instance_reducible]

instance KampReyle1993.instStructureKrLangBool : krLang.Structure Bool

Equations

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

theorem KampReyle1993.donkey_false_in_model (a : ℕ → Bool) : ¬donkey.trueRel a

The donkey conditional is false when the owning pair goes unbeaten, here with farmer false owning donkey true and beats empty.