Kamp & Reyle (1993) [KR93]

From Discourse to Logic interprets discourse by DRS construction and verifies DRSs by embeddings into a model. This file evaluates the book's worked examples through the substrate denotation DRS.trueRel (Semantics/Dynamic/DRS/; [Mus96]'s relational truth, the existential closure of Def. 1.4.5): "Jones owns Ulysses. It fascinates him." (1.1) is true of a single owning pair, its pronoun equations adding no quantificational force (ulysses_tc); "Jones does not own a Porsche." (1.56) is the non-existence of a verifying extension (porsche_tc), the referent under ¬ being inaccessible from the top level while the outer referent stays visible inside (porsche_referent_inaccessible, outer_referent_accessible); and "If a farmer owns a donkey he beats it." (2.47) receives the universal reading through the ⇒ verification clause of (2.31)/Def. 2.1.4 (donkey_universal_reading), the pronoun-completed (2.45)-style variant having the same truth conditions (donkeyPronoun_agree).

The structural facts — subordination of the donkey boxes (Def. 1.4.10/2.1.2), the accessibility asymmetry ([GBM24] §4.2: the antecedent is accessible to the consequent, not conversely), properness, truth in concrete models — are proved by evaluation or by cases on the geometry; the truth-conditions are claims over arbitrary models, proved by unfolding the verifying-embedding semantics. Sequencing a discourse is DRS.merge, whose dynamics is the substrate Merging Lemma DRS.toRel_merge, so merged-vs-compositional equalities are definitional.

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; the pronouns it and him are resolved by the (1.17)-style equations 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: 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 the conditions use is 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): [u₂ | Porsche u₂, u₁ owns u₂].

Equations

• KampReyle1993.porscheNeg = { referents := {2}, conditions := [DRT.Condition.rel KampReyle1993.KRRel.porsche ![2], DRT.Condition.rel KampReyle1993.KRRel.owns ![1, 2]] }

def KampReyle1993.porscheDiscourse : DRT.DRS krLang ℕ

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

Equations

• KampReyle1993.porscheDiscourse = { referents := {1}, conditions := [DRT.Condition.rel KampReyle1993.KRRel.jones ![1], DRT.Condition.neg KampReyle1993.porscheNeg] }

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]

Truth of (1.57): there is no Porsche that Jones owns — the negated box is 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": 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.rel KRRel.fascinates ![2, 1]] }).IsProper

A continuation resolved to the trapped referent anyway is improper (Def. 1.4.2–1.4.3): 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.rel KampReyle1993.KRRel.beats ![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 donkey universal reading: the ⇒ verification clause ((2.31)/Def. 2.1.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).

theorem KampReyle1993.donkey_proper : donkey.IsProper

The donkey DRS is proper: the consequent's referents are supplied by the antecedent — the ⇒-accessibility in the free-variable computation.

def KampReyle1993.donkeyPronounCons : DRT.DRS krLang ℕ

The (2.45)-style consequent [u₃ | u₃ = u₂, beats u₁ u₃]: 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.rel KampReyle1993.KRRel.beats ![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 forces 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

(2.44) vs (2.45), for the donkey conditional: completing the pronoun directly or by referent-plus-equation gives the same truth conditions — the book's "clearly identical truth conditions" (p. 167).

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

Not conversely: the consequent has no outgoing accessibility edge, so its (empty) universe contributes nothing to 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: the only owning pair is (0,1), which beats holds of.

@[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: farmer false owns donkey true but beats is empty.