Keshet and Abney (2024): Intensional Anaphora

This file formalizes the account of anaphora under modals of [KA24]: a pronoun presupposes that its antecedent description has a non-empty extension ((9)), and in the paper's logic PIP (Logic/PIP/Syntax.lean) the antecedent description of a summation pronoun is a formula label, so Andrea might be eating a cheeseburger. #It is large. ((79)) is might_w(ΣwE) ∧ E ≡ … ∧ large_w(ΣbE | single(ΣbE)): the world variable of E is bound by the summation inside might at its first use and by the discourse at the pronoun, so the pronoun's description is evaluated at the discourse world and felicity ((83)) demands single(ΣbE) in every world where Andrea might be eating one, including those where she is not (felicitous_discourseMight_iff, not_felicitous_burger). With must ((88)–(90)) the realistic modal base guarantees the description at the world of evaluation and the pronoun is fine (felicitous_discourseMust_of_realistic), whereas a value-based presupposition of existence would wrongly license she for the mayoral candidates of (85), who all exist. The unembedded discourse (74) is felicitous ((78), felicitous_plain), and the bathroom disjunction (95) exactly when a bathroom, if there is one, is unique ((97), felicitous_bathroom_iff).

Implementation notes

The paper's felicity conditions (78), (83), (87), (90) and (97) quantify over worlds; the statements here take a world of evaluation w₀ and an assignment sending w to it, at the level of a Scenario (accessibility, antecedent description, continuation) and its PIP model Scenario.model. The modals are Modal.apply ((35)), the summation pronoun Term.sgPronoun ((71)), and the discourses discourseMight ((80b) with (82b)), discourseMust ((89)), plain ((75) with (76)) and bathroom ((95)), each expanded from its label by Formula.expandSelf.

References

• [KA24]
• [Sto99]
• [Bra10]

inductive KeshetAbney2024.Var : Type

The variables of the discourses: the world w, the modal-base world u, the antecedent's individual b.

• w : Var
• u : Var
• b : Var

@[instance_reducible]

instance KeshetAbney2024.instDecidableEqVar : DecidableEq Var

Equations

• KeshetAbney2024.instDecidableEqVar x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive KeshetAbney2024.Lab : Type

The formula labels: the antecedent description E, and X of (95).

• E : Lab
• X : Lab

@[instance_reducible]

instance KeshetAbney2024.instDecidableEqLab : DecidableEq Lab

Equations

• KeshetAbney2024.instDecidableEqLab x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive KeshetAbney2024.Sym : ℕ → Type

Relation symbols, by number of non-world arguments: accessibility between worlds, and the antecedent description and continuation of entities.

• acc : Sym 1
• desc : Sym 1
• cont : Sym 1

@[reducible, inline]

abbrev KeshetAbney2024.Tm : Type

Terms of the discourses.

Equations

• KeshetAbney2024.Tm = PIP.Term KeshetAbney2024.Var KeshetAbney2024.Lab KeshetAbney2024.Sym

@[reducible, inline]

abbrev KeshetAbney2024.Fm : Type

Formulas of the discourses.

Equations

• KeshetAbney2024.Fm = PIP.Formula KeshetAbney2024.Var KeshetAbney2024.Lab KeshetAbney2024.Sym

Scenarios

structure KeshetAbney2024.Scenario (W E : Type) : Type

A scenario: accessibility between worlds, the antecedent description and the continuation's predicate, each relative to a world.

• acc : W → W → Prop
• desc : W → E → Prop
• cont : W → E → Prop

def KeshetAbney2024.Scenario.model {W E : Type} (S : Scenario W E) : PIP.Model Sym (PIP.Atom W E)

The model of a scenario.

Equations

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

The discourses

def KeshetAbney2024.descE : Fm

E ≡ desc_w([b]) ∧ single(b): the antecedent description of (80b), with a bracketed local variable for the indefinite.

Equations

• KeshetAbney2024.descE = (PIP.Expr.atom KeshetAbney2024.Sym.desc (PIP.Expr.var KeshetAbney2024.Var.w) ![PIP.Expr.bvar KeshetAbney2024.Var.b]).conj (PIP.Expr.var KeshetAbney2024.Var.b).sg

def KeshetAbney2024.access : Fm

acc(w, u): u is accessible from w.

Equations

• KeshetAbney2024.access = PIP.Expr.atom KeshetAbney2024.Sym.acc (PIP.Expr.var KeshetAbney2024.Var.w) ![PIP.Expr.var KeshetAbney2024.Var.u]

def KeshetAbney2024.base : Tm

Σu acc(w, u): the modal base β_w.

Equations

• KeshetAbney2024.base = PIP.Expr.sigma KeshetAbney2024.Var.u KeshetAbney2024.access

inductive KeshetAbney2024.Modal : Type

The one-place modals (35): might_w(Σwφ) = some(β_w, Σwφ) and must_w(Σwφ) = every(β_w, Σwφ).

• might : Modal
• must : Modal

def KeshetAbney2024.Modal.apply : Modal → Tm → Tm → Fm

A modal applied to its base and its prejacent.

Equations

• KeshetAbney2024.Modal.might.apply x✝¹ x✝ = PIP.Formula.some_ x✝¹ x✝
• KeshetAbney2024.Modal.must.apply x✝¹ x✝ = PIP.Expr.subset x✝¹ x✝

def KeshetAbney2024.continuation (φ : Fm) : Fm

cont_w(Σbφ | single(Σbφ)): the continuation (82b), with the summation pronoun Term.sgPronoun (71).

Equations

• KeshetAbney2024.continuation φ = PIP.Expr.atom KeshetAbney2024.Sym.cont (PIP.Expr.var KeshetAbney2024.Var.w) ![PIP.Term.sgPronoun KeshetAbney2024.Var.b φ]

def KeshetAbney2024.discourse (m : Modal) (φ : Fm) : Fm

modal_w(Σwφ) ∧ E ≡ desc_w([b]) ∧ single(b) ∧ cont_w(Σbφ | single(Σbφ)).

Equations

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

def KeshetAbney2024.discourseMight : Fm

(80b) ∧ (82b): "Andrea might be eating a cheeseburger. It is large."

Equations

• KeshetAbney2024.discourseMight = KeshetAbney2024.discourse KeshetAbney2024.Modal.might (PIP.Expr.label KeshetAbney2024.Lab.E)

def KeshetAbney2024.discourseMust : Fm

(89): "There must be some sort of animal in the shed. It's making quite a racket!"

Equations

• KeshetAbney2024.discourseMust = KeshetAbney2024.discourse KeshetAbney2024.Modal.must (PIP.Expr.label KeshetAbney2024.Lab.E)

def KeshetAbney2024.plain : Fm

(75) ∧ (76): "Andrea is eating a cheeseburger. It is large.", with the simple pronoun b | single(b).

Equations

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

def KeshetAbney2024.bathroom : Fm

(95): "Either there's no bathroom in this house or it's in a funny place.", (¬∃bX ∨ cont_w(ΣbX | single(ΣbX))) ∧ X ≡ desc_w([b]) ∧ single(b).

Equations

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

Label expansion

theorem KeshetAbney2024.expandSelf_discourseMight : PIP.Formula.expandSelf discourseMight = discourse Modal.might descE

theorem KeshetAbney2024.expandSelf_discourseMust : PIP.Formula.expandSelf discourseMust = discourse Modal.must descE

theorem KeshetAbney2024.expandSelf_bathroom : PIP.Formula.expandSelf bathroom = PIP.Expr.conj (PIP.Formula.disj (PIP.Expr.exists_ Var.b descE).neg (continuation descE)) (PIP.Expr.labelDef Lab.X descE)

Values and felicity at a world of evaluation

theorem KeshetAbney2024.felicitous_descE {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) : PIP.Expr.Felicitous S.model h descE

theorem KeshetAbney2024.felicitous_access {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) : PIP.Expr.Felicitous S.model h access

theorem KeshetAbney2024.realize_descE {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) : PIP.Formula.Realize S.model h descE ↔ ∃ (w : W) (e : E), h Var.w = PIP.world w ∧ h Var.b = {Sum.inr e} ∧ S.desc w e

theorem KeshetAbney2024.realize_sigmaB_descE {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (hw : h Var.w = PIP.world w₀) : PIP.Term.realize S.model h (PIP.Expr.sigma Var.b descE) = Sum.inr '' {e : E | S.desc w₀ e}

ΣbE at w₀: the satisfiers of the description there.

theorem KeshetAbney2024.realize_sigmaW_descE {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) : PIP.Term.realize S.model h (PIP.Expr.sigma Var.w descE) = Sum.inl '' {w : W | ∃ (e : E), S.desc w e}

ΣwE: the worlds with a satisfier of the description.

theorem KeshetAbney2024.realize_base {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (hw : h Var.w = PIP.world w₀) : PIP.Term.realize S.model h base = Sum.inl '' {u : W | S.acc w₀ u}

The modal base: the worlds accessible from the world of w.

theorem KeshetAbney2024.realize_might {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (hw : h Var.w = PIP.world w₀) : PIP.Formula.Realize S.model h (Modal.might.apply base (PIP.Expr.sigma Var.w descE)) ↔ ∃ (u : W) (e : E), S.acc w₀ u ∧ S.desc u e

might_w(ΣwE) at w₀: some accessible world has a satisfier.

theorem KeshetAbney2024.realize_must {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (hw : h Var.w = PIP.world w₀) : PIP.Formula.Realize S.model h (Modal.must.apply base (PIP.Expr.sigma Var.w descE)) ↔ ∀ (u : W), S.acc w₀ u → ∃ (e : E), S.desc u e

must_w(ΣwE) at w₀: every accessible world has a satisfier.

theorem KeshetAbney2024.felicitous_modal {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) (m : Modal) : PIP.Expr.Felicitous S.model h (m.apply base (PIP.Expr.sigma Var.w descE))

theorem KeshetAbney2024.felicitous_pronoun_iff {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (hw : h Var.w = PIP.world w₀) : PIP.Expr.Felicitous S.model h (PIP.Term.sgPronoun Var.b descE) ↔ ∃! e : E, S.desc w₀ e

theorem KeshetAbney2024.felicitous_continuation_iff {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (hw : h Var.w = PIP.world w₀) : PIP.Expr.Felicitous S.model h (continuation descE) ↔ ∃! e : E, S.desc w₀ e

theorem KeshetAbney2024.felicitous_discourse_iff {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (m : Modal) (hw : h Var.w = PIP.world w₀) : PIP.Expr.Felicitous S.model h (discourse m descE) ↔ PIP.Formula.Realize S.model h (m.apply base (PIP.Expr.sigma Var.w descE)) → ∃! e : E, S.desc w₀ e

A modal discourse is felicitous at w₀ iff the modal claim there implies a unique satisfier of the antecedent description at w₀.

theorem KeshetAbney2024.felicitous_discourseMight_iff {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (hw : h Var.w = PIP.world w₀) : PIP.Expr.Felicitous S.model h (PIP.Formula.expandSelf discourseMight) ↔ (∃ (u : W) (e : E), S.acc w₀ u ∧ S.desc u e) → ∃! e : E, S.desc w₀ e

(83): with might, the discourse is felicitous at w₀ iff, whenever a world with a satisfier is accessible from w₀, w₀ itself has a unique satisfier.

theorem KeshetAbney2024.felicitous_discourseMust_iff {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (hw : h Var.w = PIP.world w₀) : PIP.Expr.Felicitous S.model h (PIP.Formula.expandSelf discourseMust) ↔ (∀ (u : W), S.acc w₀ u → ∃ (e : E), S.desc u e) → ∃! e : E, S.desc w₀ e

(90): with must, the discourse is felicitous at w₀ iff, whenever every world accessible from w₀ has a satisfier, w₀ has a unique one.

theorem KeshetAbney2024.felicitous_discourseMust_of_realistic {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (hr : ∀ (w : W), S.acc w w) (hu : ∀ (w : W), (∃ (e : E), S.desc w e) → ∃! e : E, S.desc w e) (hw : h Var.w = PIP.world w₀) : PIP.Expr.Felicitous S.model h (PIP.Formula.expandSelf discourseMust)

(88)–(90): a realistic modal base and the scalar implicature that a satisfier is unique make the must discourse felicitous at every world.

theorem KeshetAbney2024.felicitous_plain {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) : PIP.Expr.Felicitous S.model h plain

(78): the unembedded discourse (74) is felicitous under every assignment, the assertion single(b) satisfying the pronoun's presupposition.

theorem KeshetAbney2024.felicitous_exists_descE {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) : PIP.Expr.Felicitous S.model h (PIP.Expr.exists_ Var.b descE)

theorem KeshetAbney2024.realize_exists_descE {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (hw : h Var.w = PIP.world w₀) : PIP.Formula.Realize S.model h (PIP.Expr.exists_ Var.b descE) ↔ ∃ (e : E), S.desc w₀ e

theorem KeshetAbney2024.felicitous_bathroom_iff {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (hw : h Var.w = PIP.world w₀) : PIP.Expr.Felicitous S.model h (PIP.Formula.expandSelf bathroom) ↔ (∃ (e : E), S.desc w₀ e) → ∃! e : E, S.desc w₀ e

(97): the bathroom disjunction is felicitous at w₀ iff a bathroom there, if any, is unique.

Possible burgers

def KeshetAbney2024.burger : Scenario Bool Unit

(79): at false Andrea is fasting and at true she is eating a cheeseburger, and for all anyone knows at either world, either is actual.

Equations

• KeshetAbney2024.burger = { acc := fun (x x_1 : Bool) => True, desc := fun (w : Bool) (x : Unit) => w = true, cont := fun (x : Bool) (x_1 : Unit) => True }

theorem KeshetAbney2024.not_felicitous_burger (h : Var → Set (PIP.Atom Bool Unit)) (hw : h Var.w = PIP.world false) : ¬PIP.Expr.Felicitous burger.model h (PIP.Formula.expandSelf discourseMight)

(79) is infelicitous at the world where Andrea is fasting but might be eating a cheeseburger: ΣbE is empty there.