Keshet & Abney (2024): Intensional Anaphora

@cite{keshet-abney-2024} @cite{partee-1972} @cite{roberts-1987} @cite{stone-1999} @cite{brasoveanu-2010}

Formalizes the core contributions of @cite{keshet-abney-2024}'s PIP (Plural Intensional Presuppositional predicate calculus) and connects them to the theory-neutral anaphora data in Phenomena/Anaphora/.

Paper's Core Claim

Pronouns carry descriptive content (formula labels), not stored entity values. A pronoun presupposes that its antecedent description has a non-empty extension in every world of the context set (paper item 9).

This single hypothesis, implemented via PIP's formula labels and felicity conditions, uniformly explains:

1. Modal subordination — labels survive modals (paper §2.6.3, items 59–60)
2. Bathroom sentences — labels survive negation (paper §3.4, item 92b)
3. Donkey anaphora — labels survive ∀ = ¬∃¬ (paper §2.6.2, items 53–56)
4. Paycheck pronouns — descriptions re-evaluated (paper §2.6.4, items 66–67)
5. Intensional anaphora — might blocks, must allows (paper §3.1–3.3)

Architecture

This study file imports:

• Theory: Theories/Semantics/PIP/ (PIP mechanism)
• Data: Phenomena/Anaphora/ (theory-neutral judgments)

and proves that PIP's predictions match the empirical data via worked finite models with decide verification.

inductive KeshetAbney2024.SWorld : Type

Stone's puzzle world model (@cite{stone-1999}, @cite{roberts-1987}).

Three possible worlds:

• actual: the evaluation world (no wolf present)
• wolfIn: a world where a wolf comes in
• noWolf: a world where no wolf comes in

• actual : SWorld
• wolfIn : SWorld
• noWolf : SWorld

@[implicit_reducible]

instance KeshetAbney2024.instDecidableEqSWorld : DecidableEq SWorld

Equations

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

@[implicit_reducible]

instance KeshetAbney2024.instReprSWorld : Repr SWorld

Equations

• KeshetAbney2024.instReprSWorld = { reprPrec := KeshetAbney2024.instReprSWorld.repr }

def KeshetAbney2024.instReprSWorld.repr : SWorld → ℕ → Std.Format

Equations

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

def KeshetAbney2024.instInhabitedSWorld.default : SWorld

Equations

• KeshetAbney2024.instInhabitedSWorld.default = KeshetAbney2024.SWorld.actual

@[implicit_reducible]

instance KeshetAbney2024.instInhabitedSWorld : Inhabited SWorld

Equations

• KeshetAbney2024.instInhabitedSWorld = { default := KeshetAbney2024.instInhabitedSWorld.default }

inductive KeshetAbney2024.SEntity : Type

• wolf : SEntity

@[implicit_reducible]

instance KeshetAbney2024.instDecidableEqSEntity : DecidableEq SEntity

Equations

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

@[implicit_reducible]

instance KeshetAbney2024.instReprSEntity : Repr SEntity

Equations

• KeshetAbney2024.instReprSEntity = { reprPrec := KeshetAbney2024.instReprSEntity.repr }

def KeshetAbney2024.instReprSEntity.repr : SEntity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KeshetAbney2024.instInhabitedSEntity : Inhabited SEntity

Equations

• KeshetAbney2024.instInhabitedSEntity = { default := KeshetAbney2024.instInhabitedSEntity.default }

def KeshetAbney2024.instInhabitedSEntity.default : SEntity

Equations

• KeshetAbney2024.instInhabitedSEntity.default = KeshetAbney2024.SEntity.wolf

def KeshetAbney2024.sWorlds : List SWorld

Equations

• KeshetAbney2024.sWorlds = [KeshetAbney2024.SWorld.actual, KeshetAbney2024.SWorld.wolfIn, KeshetAbney2024.SWorld.noWolf]

def KeshetAbney2024.αWolf : Semantics.PIP.FLabel

Equations

• KeshetAbney2024.αWolf = { idx := 0 }

def KeshetAbney2024.vWolf : Semantics.Dynamic.Core.IVar

Equations

• KeshetAbney2024.vWolf = { idx := 0 }

def KeshetAbney2024.sAccess : Semantics.PIP.BAccessRel SWorld

Epistemic accessibility from actual world.

Equations

• KeshetAbney2024.sAccess KeshetAbney2024.SWorld.actual KeshetAbney2024.SWorld.wolfIn = true
• KeshetAbney2024.sAccess KeshetAbney2024.SWorld.actual KeshetAbney2024.SWorld.noWolf = true
• KeshetAbney2024.sAccess x✝¹ x✝ = false

def KeshetAbney2024.isWolf (g : Semantics.Dynamic.Core.ICDRTAssignment SWorld SEntity) (w : SWorld) : Bool

Equations

• KeshetAbney2024.isWolf g w = ((g⟦KeshetAbney2024.vWolf⟧ᵢ) w == Semantics.Dynamic.Core.Entity.some KeshetAbney2024.SEntity.wolf)

def KeshetAbney2024.comesIn (g : Semantics.Dynamic.Core.ICDRTAssignment SWorld SEntity) (w : SWorld) : Bool

Equations

• KeshetAbney2024.comesIn g w = ((g⟦KeshetAbney2024.vWolf⟧ᵢ) w == Semantics.Dynamic.Core.Entity.some KeshetAbney2024.SEntity.wolf && w == KeshetAbney2024.SWorld.wolfIn)

def KeshetAbney2024.stoneSentence1 : Semantics.PIP.PUpdate SWorld SEntity

"A wolf might come in." (paper item 59a)

might(∃^αWolf x. wolf(x) ∧ comeIn(x))

Label αWolf records the description "wolf(x) that comes in".

Equations

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

theorem KeshetAbney2024.stone_label_registered (d : Semantics.PIP.Discourse SWorld SEntity) (_hConsistent : Set.Nonempty d.info) : (stoneSentence1 d).labels.registered αWolf = true

After "A wolf might come in", the label αWolf is registered.

def KeshetAbney2024.stoneSentence2 : Semantics.PIP.PUpdate SWorld SEntity

"It would eat you first." (paper item 59b)

"It" = DEF_αWolf{x}; "would" = must with inherited accessibility.

Equations

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

def KeshetAbney2024.stoneDiscourse : Semantics.PIP.PUpdate SWorld SEntity

Equations

• KeshetAbney2024.stoneDiscourse = Semantics.PIP.conj KeshetAbney2024.stoneSentence1 KeshetAbney2024.stoneSentence2

theorem KeshetAbney2024.stone_discourse_label_available (d : Semantics.PIP.Discourse SWorld SEntity) : (stoneDiscourse d).labels.registered αWolf = true

After the full discourse, the label is still available.

theorem KeshetAbney2024.stone_discourse_consistent : Set.Nonempty (stoneDiscourse KeshetAbney2024.stone_d₀✝).info

End-to-end test: Stone's discourse is consistent on a concrete model.

After "A wolf might come. It would eat you first.", the discourse state is non-empty: g_wolf (with vWolf ↦ wolf) at actual survives the pipeline.

theorem KeshetAbney2024.stone_discourse_rejects_unbound : (KeshetAbney2024.g₀_stone✝, SWorld.actual) ∉ (stoneSentence1 KeshetAbney2024.stone_d₀✝).info

Negative test: unbound wolf variable is rejected.

inductive KeshetAbney2024.BWorld : Type

@cite{partee-1972}'s bathroom sentence world model.

• bath : BWorld
• noBath : BWorld

@[implicit_reducible]

instance KeshetAbney2024.instDecidableEqBWorld : DecidableEq BWorld

Equations

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

def KeshetAbney2024.instReprBWorld.repr : BWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KeshetAbney2024.instReprBWorld : Repr BWorld

Equations

• KeshetAbney2024.instReprBWorld = { reprPrec := KeshetAbney2024.instReprBWorld.repr }

def KeshetAbney2024.instInhabitedBWorld.default : BWorld

Equations

• KeshetAbney2024.instInhabitedBWorld.default = KeshetAbney2024.BWorld.bath

@[implicit_reducible]

instance KeshetAbney2024.instInhabitedBWorld : Inhabited BWorld

Equations

• KeshetAbney2024.instInhabitedBWorld = { default := KeshetAbney2024.instInhabitedBWorld.default }

inductive KeshetAbney2024.BEntity : Type

• bathroom : BEntity

@[implicit_reducible]

instance KeshetAbney2024.instDecidableEqBEntity : DecidableEq BEntity

Equations

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

def KeshetAbney2024.instReprBEntity.repr : BEntity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KeshetAbney2024.instReprBEntity : Repr BEntity

Equations

• KeshetAbney2024.instReprBEntity = { reprPrec := KeshetAbney2024.instReprBEntity.repr }

def KeshetAbney2024.instInhabitedBEntity.default : BEntity

Equations

• KeshetAbney2024.instInhabitedBEntity.default = KeshetAbney2024.BEntity.bathroom

@[implicit_reducible]

instance KeshetAbney2024.instInhabitedBEntity : Inhabited BEntity

Equations

• KeshetAbney2024.instInhabitedBEntity = { default := KeshetAbney2024.instInhabitedBEntity.default }

def KeshetAbney2024.αBath : Semantics.PIP.FLabel

Equations

• KeshetAbney2024.αBath = { idx := 1 }

def KeshetAbney2024.vBath : Semantics.Dynamic.Core.IVar

Equations

• KeshetAbney2024.vBath = { idx := 1 }

def KeshetAbney2024.isBathroom (g : Semantics.Dynamic.Core.ICDRTAssignment BWorld BEntity) (w : BWorld) : Bool

Equations

• KeshetAbney2024.isBathroom g w = ((g⟦KeshetAbney2024.vBath⟧ᵢ) w == Semantics.Dynamic.Core.Entity.some KeshetAbney2024.BEntity.bathroom)

def KeshetAbney2024.isUpstairs (g : Semantics.Dynamic.Core.ICDRTAssignment BWorld BEntity) (w : BWorld) : Bool

Equations

• KeshetAbney2024.isUpstairs g w = ((g⟦KeshetAbney2024.vBath⟧ᵢ) w == Semantics.Dynamic.Core.Entity.some KeshetAbney2024.BEntity.bathroom && w == KeshetAbney2024.BWorld.bath)

def KeshetAbney2024.bathroomSentence : Semantics.PIP.PUpdate BWorld BEntity

"Either there's no bathroom, or it's upstairs." (paper item 92b)

PIP analysis: ¬∃^αBath x.bathroom(x) ∨ upstairs(DEF_αBath{x})

Label αBath is registered under negation and floated to the second disjunct.

Equations

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

theorem KeshetAbney2024.bathroom_label_survives_negation (d : Semantics.PIP.Discourse BWorld BEntity) : have firstDisjunct := Semantics.PIP.negation (Semantics.PIP.existsLabeled αBath vBath {BEntity.bathroom} isBathroom (Semantics.PIP.atom isBathroom)); (firstDisjunct d).labels.registered αBath = true

The bathroom label survives negation — core PIP mechanism.

theorem KeshetAbney2024.bathroom_sentence_consistent : Set.Nonempty (bathroomSentence KeshetAbney2024.bath_d₀✝).info

End-to-end: the bathroom sentence is consistent.

theorem KeshetAbney2024.bathroom_rejects_nonupstairs : (KeshetAbney2024.g_bath✝, BWorld.noBath) ∉ (bathroomSentence KeshetAbney2024.bath_d₀✝).info

Negative test: bathroom at noBath world is rejected.

inductive KeshetAbney2024.PEntity : Type

"John spent his paycheck. Bill saved it." (paper items 66–67)

"it" carries descriptive content "paycheck-of(x, possessor)" which is re-evaluated when the possessor variable is rebound to Bill.

Value-based: "it" → John's paycheck → wrong referent Description-based: "it" → "the paycheck of [current subject]" → Bill's paycheck

• john : PEntity
• bill : PEntity
• johnsPaycheck : PEntity
• billsPaycheck : PEntity

@[implicit_reducible]

instance KeshetAbney2024.instDecidableEqPEntity : DecidableEq PEntity

Equations

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

def KeshetAbney2024.instReprPEntity.repr : PEntity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KeshetAbney2024.instReprPEntity : Repr PEntity

Equations

• KeshetAbney2024.instReprPEntity = { reprPrec := KeshetAbney2024.instReprPEntity.repr }

@[implicit_reducible]

instance KeshetAbney2024.instInhabitedPEntity : Inhabited PEntity

Equations

• KeshetAbney2024.instInhabitedPEntity = { default := KeshetAbney2024.instInhabitedPEntity.default }

def KeshetAbney2024.instInhabitedPEntity.default : PEntity

Equations

• KeshetAbney2024.instInhabitedPEntity.default = KeshetAbney2024.PEntity.john

def KeshetAbney2024.αPaycheck : Semantics.PIP.FLabel

Equations

• KeshetAbney2024.αPaycheck = { idx := 2 }

def KeshetAbney2024.vPaycheck : Semantics.Dynamic.Core.IVar

Equations

• KeshetAbney2024.vPaycheck = { idx := 2 }

def KeshetAbney2024.vPossessor : Semantics.Dynamic.Core.IVar

Equations

• KeshetAbney2024.vPossessor = { idx := 3 }

inductive KeshetAbney2024.PWorld : Type

• w0 : PWorld

@[implicit_reducible]

instance KeshetAbney2024.instDecidableEqPWorld : DecidableEq PWorld

Equations

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

@[implicit_reducible]

instance KeshetAbney2024.instReprPWorld : Repr PWorld

Equations

• KeshetAbney2024.instReprPWorld = { reprPrec := KeshetAbney2024.instReprPWorld.repr }

def KeshetAbney2024.instReprPWorld.repr : PWorld → ℕ → Std.Format

Equations

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

def KeshetAbney2024.instInhabitedPWorld.default : PWorld

Equations

• KeshetAbney2024.instInhabitedPWorld.default = KeshetAbney2024.PWorld.w0

@[implicit_reducible]

instance KeshetAbney2024.instInhabitedPWorld : Inhabited PWorld

Equations

• KeshetAbney2024.instInhabitedPWorld = { default := KeshetAbney2024.instInhabitedPWorld.default }

def KeshetAbney2024.isPaycheckOf (g : Semantics.Dynamic.Core.ICDRTAssignment PWorld PEntity) (w : PWorld) : Bool

Relational paycheck predicate: depends on both paycheck and possessor.

Equations

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

theorem KeshetAbney2024.paycheck_needs_descriptions : have g := { indiv := fun (v : Semantics.Dynamic.Core.IVar) (_w : PWorld) => if (v == vPaycheck) = true then Semantics.Dynamic.Core.Entity.some PEntity.billsPaycheck else if (v == vPossessor) = true then Semantics.Dynamic.Core.Entity.some PEntity.bill else Semantics.Dynamic.Core.Entity.star, prop := fun (x : Semantics.Dynamic.Core.PVar) => ∅ }; isPaycheckOf g PWorld.w0 = true

Re-evaluation yields Bill's paycheck when possessor = Bill.

structure KeshetAbney2024.ModalSubDatum : Type

A modal subordination datum.

• sentence1 : String
• sentence2 : String
• modal1 : String
• modal2 : String
• anaphor : String
• antecedent : String
• felicitous : Bool
• source : String

@[implicit_reducible]

instance KeshetAbney2024.instReprModalSubDatum : Repr ModalSubDatum

Equations

• KeshetAbney2024.instReprModalSubDatum = { reprPrec := KeshetAbney2024.instReprModalSubDatum.repr }

def KeshetAbney2024.instReprModalSubDatum.repr : ModalSubDatum → ℕ → Std.Format

Equations

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

def KeshetAbney2024.wolfMightWould : ModalSubDatum

Equations

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

def KeshetAbney2024.wolfMightCould : ModalSubDatum

Equations

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

def KeshetAbney2024.burglarMightWould : ModalSubDatum

Equations

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

def KeshetAbney2024.wolfMightIndicative : ModalSubDatum

Equations

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

def KeshetAbney2024.wolfMightWill : ModalSubDatum

Equations

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

def KeshetAbney2024.wolfCouldWould : ModalSubDatum

Equations

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

def KeshetAbney2024.modalSubData : List ModalSubDatum

Equations

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

def KeshetAbney2024.felicitousModalSub : List ModalSubDatum

Equations

• KeshetAbney2024.felicitousModalSub = List.filter (fun (x : KeshetAbney2024.ModalSubDatum) => x.felicitous) KeshetAbney2024.modalSubData

inductive KeshetAbney2024.ModalContinuation : Type

Modal continuation type: whether a modal inherits its accessibility relation from prior discourse context.

PIP predicts modal subordination is felicitous iff the second modal subordinates — i.e., it inherits the accessibility relation established by the first modal (paper §2.6.3). "Would" is analyzed as must with the inherited R; "could" as might with the inherited R.

Modals that establish their own accessibility relation (epistemic "must", future "will", indicative mood) cannot access entities introduced under a prior modal's scope.

• subordinating : ModalContinuation
• independent : ModalContinuation

@[implicit_reducible]

instance KeshetAbney2024.instDecidableEqModalContinuation : DecidableEq ModalContinuation

Equations

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

@[implicit_reducible]

instance KeshetAbney2024.instReprModalContinuation : Repr ModalContinuation

Equations

• KeshetAbney2024.instReprModalContinuation = { reprPrec := KeshetAbney2024.instReprModalContinuation.repr }

def KeshetAbney2024.instReprModalContinuation.repr : ModalContinuation → ℕ → Std.Format

Equations

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

def KeshetAbney2024.classifyModal2 : String → ModalContinuation

Classify an English modal by whether it subordinates.

Equations

• KeshetAbney2024.classifyModal2 "would" = KeshetAbney2024.ModalContinuation.subordinating
• KeshetAbney2024.classifyModal2 "could" = KeshetAbney2024.ModalContinuation.subordinating
• KeshetAbney2024.classifyModal2 x✝ = KeshetAbney2024.ModalContinuation.independent

def KeshetAbney2024.pipPredictsModalSub (datum : ModalSubDatum) : Bool

PIP predicts modal subordination felicity iff the second modal subordinates (inherits the accessibility relation from the first).

Equations

• KeshetAbney2024.pipPredictsModalSub datum = (KeshetAbney2024.classifyModal2 datum.modal2 == KeshetAbney2024.ModalContinuation.subordinating)

theorem KeshetAbney2024.pip_wolf_might_would : pipPredictsModalSub wolfMightWould = true

theorem KeshetAbney2024.pip_wolf_might_could : pipPredictsModalSub wolfMightCould = true

theorem KeshetAbney2024.pip_wolf_indicative_fails : pipPredictsModalSub wolfMightIndicative = false

theorem KeshetAbney2024.pip_wolf_will_fails : pipPredictsModalSub wolfMightWill = false

theorem KeshetAbney2024.pip_modal_sub_felicitous_agreement : (felicitousModalSub.all fun (d : ModalSubDatum) => pipPredictsModalSub d == d.felicitous) = true

theorem KeshetAbney2024.modal_sub_binding_modes : (Semantics.PIP.modalBindings { idx := 99 } { idx := 0 } αWolf)[1]? = some { var := { idx := 0 }, mode := Semantics.PIP.BindingMode.local, label := some αWolf } ∧ (Semantics.PIP.modalBindings { idx := 99 } { idx := 0 } αWolf)[0]? = some { var := { idx := 99 }, mode := Semantics.PIP.BindingMode.external, label := none }

External/local binding modes under modals (paper §2.1).

theorem KeshetAbney2024.bathroom_mechanism (d : Semantics.PIP.Discourse BWorld BEntity) : (Semantics.PIP.negation (Semantics.PIP.existsLabeled αBath vBath {BEntity.bathroom} isBathroom (Semantics.PIP.atom isBathroom)) d).labels.registered αBath = true

Label survival is the core mechanism for bathroom sentences.

theorem KeshetAbney2024.bathroom_full_sentence_label_available (d : Semantics.PIP.Discourse BWorld BEntity) : (bathroomSentence d).labels.registered αBath = true

Full bathroom sentence preserves labels through disj + negation.

theorem KeshetAbney2024.pip_geach_donkey : Phenomena.Anaphora.DonkeyAnaphora.geachDonkey.boundReading = true

theorem KeshetAbney2024.pip_conditional_donkey : Phenomena.Anaphora.DonkeyAnaphora.conditionalDonkey.boundReading = true

theorem KeshetAbney2024.pip_paycheck : Phenomena.Anaphora.DonkeyAnaphora.paycheckSentence.boundReading = true

inductive KeshetAbney2024.IBWorld : Type

"Andrea might be eating a cheeseburger. #It is large." (paper item 79)

The burger description is world-dependent: BURGER_w([b]) holds only at worlds where Andrea is eating a burger. At worlds where she isn't, Σb(BURGER_w(b)) = ∅, failing the existential presupposition SINGLE(ΣbE).

Felicity condition (paper item 83): ∀w(MIGHT_w(ΣwE) → SINGLE(ΣbE)) fails because some context-set worlds have no burger.

• actual : IBWorld
• burgerW : IBWorld

@[implicit_reducible]

instance KeshetAbney2024.instDecidableEqIBWorld : DecidableEq IBWorld

Equations

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

def KeshetAbney2024.instReprIBWorld.repr : IBWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KeshetAbney2024.instReprIBWorld : Repr IBWorld

Equations

• KeshetAbney2024.instReprIBWorld = { reprPrec := KeshetAbney2024.instReprIBWorld.repr }

@[implicit_reducible]

instance KeshetAbney2024.instInhabitedIBWorld : Inhabited IBWorld

Equations

• KeshetAbney2024.instInhabitedIBWorld = { default := KeshetAbney2024.instInhabitedIBWorld.default }

def KeshetAbney2024.instInhabitedIBWorld.default : IBWorld

Equations

• KeshetAbney2024.instInhabitedIBWorld.default = KeshetAbney2024.IBWorld.actual

inductive KeshetAbney2024.IBEntity : Type

• burger : IBEntity

@[implicit_reducible]

instance KeshetAbney2024.instDecidableEqIBEntity : DecidableEq IBEntity

Equations

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

@[implicit_reducible]

instance KeshetAbney2024.instReprIBEntity : Repr IBEntity

Equations

• KeshetAbney2024.instReprIBEntity = { reprPrec := KeshetAbney2024.instReprIBEntity.repr }

def KeshetAbney2024.instReprIBEntity.repr : IBEntity → ℕ → Std.Format

Equations

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

def KeshetAbney2024.instInhabitedIBEntity.default : IBEntity

Equations

• KeshetAbney2024.instInhabitedIBEntity.default = KeshetAbney2024.IBEntity.burger

@[implicit_reducible]

instance KeshetAbney2024.instInhabitedIBEntity : Inhabited IBEntity

Equations

• KeshetAbney2024.instInhabitedIBEntity = { default := KeshetAbney2024.instInhabitedIBEntity.default }

def KeshetAbney2024.ibWorlds : List IBWorld

Equations

• KeshetAbney2024.ibWorlds = [KeshetAbney2024.IBWorld.actual, KeshetAbney2024.IBWorld.burgerW]

def KeshetAbney2024.αBurger : Semantics.PIP.FLabel

Equations

• KeshetAbney2024.αBurger = { idx := 10 }

def KeshetAbney2024.vBurger : Semantics.Dynamic.Core.IVar

Equations

• KeshetAbney2024.vBurger = { idx := 10 }

def KeshetAbney2024.ibAccess : Semantics.PIP.BAccessRel IBWorld

Equations

• KeshetAbney2024.ibAccess KeshetAbney2024.IBWorld.actual KeshetAbney2024.IBWorld.actual = true
• KeshetAbney2024.ibAccess KeshetAbney2024.IBWorld.actual KeshetAbney2024.IBWorld.burgerW = true
• KeshetAbney2024.ibAccess x✝¹ x✝ = false

def KeshetAbney2024.isBurgerAt (g : Semantics.Dynamic.Core.ICDRTAssignment IBWorld IBEntity) (w : IBWorld) : Bool

World-dependent predicate: burger exists only at burgerW.

Equations

• KeshetAbney2024.isBurgerAt g w = ((g⟦KeshetAbney2024.vBurger⟧ᵢ) w == Semantics.Dynamic.Core.Entity.some KeshetAbney2024.IBEntity.burger && w == KeshetAbney2024.IBWorld.burgerW)

def KeshetAbney2024.burgerSentence : Semantics.PIP.PUpdate IBWorld IBEntity

Equations

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

theorem KeshetAbney2024.burger_label_registered (d : Semantics.PIP.Discourse IBWorld IBEntity) : (burgerSentence d).labels.registered αBurger = true

theorem KeshetAbney2024.burger_desc_fails_at_actual (g : Semantics.Dynamic.Core.ICDRTAssignment IBWorld IBEntity) : isBurgerAt g IBWorld.actual = false

The burger description fails at actual — presupposition failure.

@[implicit_reducible]

instance KeshetAbney2024.instFintypeIBWorld : Fintype IBWorld

Equations

• KeshetAbney2024.instFintypeIBWorld = { elems := {KeshetAbney2024.IBWorld.actual, KeshetAbney2024.IBWorld.burgerW}, complete := KeshetAbney2024.instFintypeIBWorld._proof_1 }

theorem KeshetAbney2024.burger_desc_world_dependent : isBurgerAt { indiv := fun (x : Semantics.Dynamic.Core.IVar) (x_1 : IBWorld) => Semantics.Dynamic.Core.Entity.some IBEntity.burger, prop := fun (x : Semantics.Dynamic.Core.PVar) => ∅ } IBWorld.actual = false ∧ ibAccess IBWorld.actual IBWorld.actual = true

Might blocks anaphora NOT because of non-reflexive access, but because the burger description is world-dependent: isBurgerAt g .actual = false for all g (burger_desc_fails_at_actual). Even with a reflexive modal base, the description Σb(BURGER_w([b])) is empty at .actual — no burger there.

The accessibility IS reflexive at .actual (ibAccess .actual .actual = true), confirming that the blocking mechanism is about description content, not accessibility structure.

inductive KeshetAbney2024.IAWorld : Type

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

The animal description is world-INdependent: ANIMAL_w([x]) ∧ SINGLE(x) holds at ALL accessible worlds (realistic modal base includes actual).

Felicity condition (paper item 90): ∀w(MUST_w(ΣwX) → SINGLE(ΣxX)) succeeds because must guarantees X at every accessible world including w.

• actual : IAWorld
• shedW : IAWorld

@[implicit_reducible]

instance KeshetAbney2024.instDecidableEqIAWorld : DecidableEq IAWorld

Equations

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

@[implicit_reducible]

instance KeshetAbney2024.instReprIAWorld : Repr IAWorld

Equations

• KeshetAbney2024.instReprIAWorld = { reprPrec := KeshetAbney2024.instReprIAWorld.repr }

def KeshetAbney2024.instReprIAWorld.repr : IAWorld → ℕ → Std.Format

Equations

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

def KeshetAbney2024.instInhabitedIAWorld.default : IAWorld

Equations

• KeshetAbney2024.instInhabitedIAWorld.default = KeshetAbney2024.IAWorld.actual

@[implicit_reducible]

instance KeshetAbney2024.instInhabitedIAWorld : Inhabited IAWorld

Equations

• KeshetAbney2024.instInhabitedIAWorld = { default := KeshetAbney2024.instInhabitedIAWorld.default }

inductive KeshetAbney2024.IAEntity : Type

• animal : IAEntity

@[implicit_reducible]

instance KeshetAbney2024.instDecidableEqIAEntity : DecidableEq IAEntity

Equations

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

@[implicit_reducible]

instance KeshetAbney2024.instReprIAEntity : Repr IAEntity

Equations

• KeshetAbney2024.instReprIAEntity = { reprPrec := KeshetAbney2024.instReprIAEntity.repr }

def KeshetAbney2024.instReprIAEntity.repr : IAEntity → ℕ → Std.Format

Equations

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

def KeshetAbney2024.instInhabitedIAEntity.default : IAEntity

Equations

• KeshetAbney2024.instInhabitedIAEntity.default = KeshetAbney2024.IAEntity.animal

@[implicit_reducible]

instance KeshetAbney2024.instInhabitedIAEntity : Inhabited IAEntity

Equations

• KeshetAbney2024.instInhabitedIAEntity = { default := KeshetAbney2024.instInhabitedIAEntity.default }

def KeshetAbney2024.iaWorlds : List IAWorld

Equations

• KeshetAbney2024.iaWorlds = [KeshetAbney2024.IAWorld.actual, KeshetAbney2024.IAWorld.shedW]

def KeshetAbney2024.αAnimal : Semantics.PIP.FLabel

Equations

• KeshetAbney2024.αAnimal = { idx := 11 }

def KeshetAbney2024.vAnimal : Semantics.Dynamic.Core.IVar

Equations

• KeshetAbney2024.vAnimal = { idx := 11 }

def KeshetAbney2024.iaAccess : Semantics.PIP.BAccessRel IAWorld

Realistic epistemic: actual accessible from itself.

Equations

• KeshetAbney2024.iaAccess KeshetAbney2024.IAWorld.actual KeshetAbney2024.IAWorld.actual = true
• KeshetAbney2024.iaAccess KeshetAbney2024.IAWorld.actual KeshetAbney2024.IAWorld.shedW = true
• KeshetAbney2024.iaAccess x✝¹ x✝ = false

def KeshetAbney2024.isAnimalInShed (g : Semantics.Dynamic.Core.ICDRTAssignment IAWorld IAEntity) (w : IAWorld) : Bool

World-INdependent predicate: holds at ALL worlds.

Equations

• KeshetAbney2024.isAnimalInShed g w = ((g⟦KeshetAbney2024.vAnimal⟧ᵢ) w == Semantics.Dynamic.Core.Entity.some KeshetAbney2024.IAEntity.animal)

def KeshetAbney2024.animalSentence : Semantics.PIP.PUpdate IAWorld IAEntity

Equations

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

theorem KeshetAbney2024.animal_label_registered (d : Semantics.PIP.Discourse IAWorld IAEntity) : (animalSentence d).labels.registered αAnimal = true

theorem KeshetAbney2024.animal_desc_succeeds (g : Semantics.Dynamic.Core.ICDRTAssignment IAWorld IAEntity) (w : IAWorld) : ((g⟦vAnimal⟧ᵢ) w == Semantics.Dynamic.Core.Entity.some IAEntity.animal) = true → isAnimalInShed g w = true

@[implicit_reducible]

instance KeshetAbney2024.instFintypeIAWorld : Fintype IAWorld

Equations

• KeshetAbney2024.instFintypeIAWorld = { elems := {KeshetAbney2024.IAWorld.actual, KeshetAbney2024.IAWorld.shedW}, complete := KeshetAbney2024.instFintypeIAWorld._proof_1 }

theorem KeshetAbney2024.animal_must_realistic : iaAccess IAWorld.actual IAWorld.actual = true

Must allows anaphora via Kratzer's realistic modal base.

The animal accessibility relation is reflexive at .actual (the evaluation world), so must_realistic_at (derived from the T axiom) guarantees that the description predicate holds at .actual. This is the Kripke-semantic grounding of why must enables intensional anaphora.

inductive KeshetAbney2024.MAWorld : Type

The paper's deeper argument about must (items 106–107): in different accessible worlds, different animals could be in the shed. The summation across assignments gives MULTIPLE animals, not a single one.

Must still allows anaphora because:

1. The accessibility relation is realistic (actual ∈ β_w*)
2. The animal AT the actual world is singular (SINGLE)

The summation Σx ANIMAL_w*([x]) — evaluated at the discourse world w* — gives the singleton {cat}. The summation across ALL worlds would give {cat, dog, raccoon}, but the world variable in ΣxX is bound by the discourse-level Σw, fixing it to w*.

This enriched model shows why Stone/Brasoveanu's system incorrectly predicts plurality: it would sum across all accessible worlds, getting {cat, dog, raccoon} — failing SINGLE.

• actual : MAWorld
• shedW1 : MAWorld
• shedW2 : MAWorld

@[implicit_reducible]

instance KeshetAbney2024.instDecidableEqMAWorld : DecidableEq MAWorld

Equations

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

def KeshetAbney2024.instReprMAWorld.repr : MAWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KeshetAbney2024.instReprMAWorld : Repr MAWorld

Equations

• KeshetAbney2024.instReprMAWorld = { reprPrec := KeshetAbney2024.instReprMAWorld.repr }

@[implicit_reducible]

instance KeshetAbney2024.instInhabitedMAWorld : Inhabited MAWorld

Equations

• KeshetAbney2024.instInhabitedMAWorld = { default := KeshetAbney2024.instInhabitedMAWorld.default }

def KeshetAbney2024.instInhabitedMAWorld.default : MAWorld

Equations

• KeshetAbney2024.instInhabitedMAWorld.default = KeshetAbney2024.MAWorld.actual

inductive KeshetAbney2024.MAEntity : Type

• cat : MAEntity
• dog : MAEntity
• raccoon : MAEntity

@[implicit_reducible]

instance KeshetAbney2024.instDecidableEqMAEntity : DecidableEq MAEntity

Equations

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

def KeshetAbney2024.instReprMAEntity.repr : MAEntity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KeshetAbney2024.instReprMAEntity : Repr MAEntity

Equations

• KeshetAbney2024.instReprMAEntity = { reprPrec := KeshetAbney2024.instReprMAEntity.repr }

def KeshetAbney2024.instInhabitedMAEntity.default : MAEntity

Equations

• KeshetAbney2024.instInhabitedMAEntity.default = KeshetAbney2024.MAEntity.cat

@[implicit_reducible]

instance KeshetAbney2024.instInhabitedMAEntity : Inhabited MAEntity

Equations

• KeshetAbney2024.instInhabitedMAEntity = { default := KeshetAbney2024.instInhabitedMAEntity.default }

def KeshetAbney2024.maWorlds : List MAWorld

Equations

• KeshetAbney2024.maWorlds = [KeshetAbney2024.MAWorld.actual, KeshetAbney2024.MAWorld.shedW1, KeshetAbney2024.MAWorld.shedW2]

def KeshetAbney2024.αMA : Semantics.PIP.FLabel

Equations

• KeshetAbney2024.αMA = { idx := 12 }

def KeshetAbney2024.vMA : Semantics.Dynamic.Core.IVar

Equations

• KeshetAbney2024.vMA = { idx := 12 }

def KeshetAbney2024.maAccess : Semantics.PIP.BAccessRel MAWorld

Realistic epistemic: actual accessible from itself, plus two alternatives.

Equations

• KeshetAbney2024.maAccess KeshetAbney2024.MAWorld.actual x✝ = true
• KeshetAbney2024.maAccess x✝¹ x✝ = false

def KeshetAbney2024.isAnimalInShedMA (g : Semantics.Dynamic.Core.ICDRTAssignment MAWorld MAEntity) (w : MAWorld) : Bool

World-dependent predicate: different animal in each world.

Equations

• KeshetAbney2024.isAnimalInShedMA g KeshetAbney2024.MAWorld.actual = true
• KeshetAbney2024.isAnimalInShedMA g KeshetAbney2024.MAWorld.shedW1 = true
• KeshetAbney2024.isAnimalInShedMA g KeshetAbney2024.MAWorld.shedW2 = true
• KeshetAbney2024.isAnimalInShedMA g w✝ = false

theorem KeshetAbney2024.ma_single_at_actual : isAnimalInShedMA (KeshetAbney2024.maG✝ MAEntity.cat) MAWorld.actual = true ∧ isAnimalInShedMA (KeshetAbney2024.maG✝ MAEntity.dog) MAWorld.actual = false ∧ isAnimalInShedMA (KeshetAbney2024.maG✝ MAEntity.raccoon) MAWorld.actual = false

At actual, only cat satisfies the description (SINGLE).

theorem KeshetAbney2024.ma_different_animals_per_world : isAnimalInShedMA { indiv := fun (v : Semantics.Dynamic.Core.IVar) (_w : MAWorld) => if (v == vMA) = true then Semantics.Dynamic.Core.Entity.some MAEntity.cat else Semantics.Dynamic.Core.Entity.star, prop := fun (x : Semantics.Dynamic.Core.PVar) => ∅ } MAWorld.actual = true ∧ isAnimalInShedMA { indiv := fun (v : Semantics.Dynamic.Core.IVar) (_w : MAWorld) => if (v == vMA) = true then Semantics.Dynamic.Core.Entity.some MAEntity.dog else Semantics.Dynamic.Core.Entity.star, prop := fun (x : Semantics.Dynamic.Core.PVar) => ∅ } MAWorld.shedW1 = true ∧ isAnimalInShedMA { indiv := fun (v : Semantics.Dynamic.Core.IVar) (_w : MAWorld) => if (v == vMA) = true then Semantics.Dynamic.Core.Entity.some MAEntity.raccoon else Semantics.Dynamic.Core.Entity.star, prop := fun (x : Semantics.Dynamic.Core.PVar) => ∅ } MAWorld.shedW2 = true

Different entities satisfy the description at different worlds.

theorem KeshetAbney2024.ma_cross_world_plural : isAnimalInShedMA (KeshetAbney2024.maG✝ MAEntity.cat) MAWorld.actual = true ∧ isAnimalInShedMA (KeshetAbney2024.maG✝ MAEntity.dog) MAWorld.shedW1 = true ∧ MAEntity.cat ≠ MAEntity.dog

Cross-world summation yields PLURAL — Stone/Brasoveanu would incorrectly predict plurality here since they sum across all accessible worlds. Different animals satisfy the description at different worlds: cat at actual, dog at shedW1.

inductive KeshetAbney2024.PCWorld : Type

"There may already be a winner in the mayoral race. #She is a woman." (paper item 85)

This is PIP's strongest argument against Stone/Brasoveanu's "in" predicate. The candidates (alice, bob) are real people who exist in the actual world. A Stone/Brasoveanu-style presupposition requiring only that the referent "exist in the world of evaluation" would wrongly predict felicity.

PIP correctly blocks anaphora because the description WINNER_w([x]) is world-dependent: in worlds where the tabulation isn't complete, there is no winner, so Σx WINNER_w([x]) = ∅, failing SINGLE (paper item 87):

∀w(MIGHT_w(Σw WINNER_w([x])) → SINGLE(Σx WINNER_w([x])))

• actual : PCWorld
• aliceWins : PCWorld
• bobWins : PCWorld

@[implicit_reducible]

instance KeshetAbney2024.instDecidableEqPCWorld : DecidableEq PCWorld

Equations

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

def KeshetAbney2024.instReprPCWorld.repr : PCWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KeshetAbney2024.instReprPCWorld : Repr PCWorld

Equations

• KeshetAbney2024.instReprPCWorld = { reprPrec := KeshetAbney2024.instReprPCWorld.repr }

@[implicit_reducible]

instance KeshetAbney2024.instInhabitedPCWorld : Inhabited PCWorld

Equations

• KeshetAbney2024.instInhabitedPCWorld = { default := KeshetAbney2024.instInhabitedPCWorld.default }

def KeshetAbney2024.instInhabitedPCWorld.default : PCWorld

Equations

• KeshetAbney2024.instInhabitedPCWorld.default = KeshetAbney2024.PCWorld.actual

inductive KeshetAbney2024.PCEntity : Type

• alice : PCEntity
• bob : PCEntity

@[implicit_reducible]

instance KeshetAbney2024.instDecidableEqPCEntity : DecidableEq PCEntity

Equations

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

@[implicit_reducible]

instance KeshetAbney2024.instReprPCEntity : Repr PCEntity

Equations

• KeshetAbney2024.instReprPCEntity = { reprPrec := KeshetAbney2024.instReprPCEntity.repr }

def KeshetAbney2024.instReprPCEntity.repr : PCEntity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KeshetAbney2024.instInhabitedPCEntity : Inhabited PCEntity

Equations

• KeshetAbney2024.instInhabitedPCEntity = { default := KeshetAbney2024.instInhabitedPCEntity.default }

def KeshetAbney2024.instInhabitedPCEntity.default : PCEntity

Equations

• KeshetAbney2024.instInhabitedPCEntity.default = KeshetAbney2024.PCEntity.alice

def KeshetAbney2024.pcWorlds : List PCWorld

Equations

• KeshetAbney2024.pcWorlds = [KeshetAbney2024.PCWorld.actual, KeshetAbney2024.PCWorld.aliceWins, KeshetAbney2024.PCWorld.bobWins]

def KeshetAbney2024.αWinner : Semantics.PIP.FLabel

Equations

• KeshetAbney2024.αWinner = { idx := 20 }

def KeshetAbney2024.vWinner : Semantics.Dynamic.Core.IVar

Equations

• KeshetAbney2024.vWinner = { idx := 20 }

def KeshetAbney2024.pcAccess : Semantics.PIP.BAccessRel PCWorld

Epistemic: speaker considers all outcomes possible.

Equations

• KeshetAbney2024.pcAccess KeshetAbney2024.PCWorld.actual x✝ = true
• KeshetAbney2024.pcAccess x✝¹ x✝ = false

def KeshetAbney2024.isWinner (g : Semantics.Dynamic.Core.ICDRTAssignment PCWorld PCEntity) (w : PCWorld) : Bool

World-dependent predicate: winner only at resolution worlds.

Equations

• KeshetAbney2024.isWinner g KeshetAbney2024.PCWorld.aliceWins = true
• KeshetAbney2024.isWinner g KeshetAbney2024.PCWorld.bobWins = true
• KeshetAbney2024.isWinner g w✝ = false

def KeshetAbney2024.candidateSentence : Semantics.PIP.PUpdate PCWorld PCEntity

"There may already be a winner."

Equations

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

theorem KeshetAbney2024.winner_desc_empty_at_actual (g : Semantics.Dynamic.Core.ICDRTAssignment PCWorld PCEntity) : isWinner g PCWorld.actual = false

The winner description is empty at the actual world — no winner declared yet.

theorem KeshetAbney2024.candidates_exist_but_description_fails : {PCEntity.alice, PCEntity.bob}.Nonempty ∧ ∀ (g : Semantics.Dynamic.Core.ICDRTAssignment PCWorld PCEntity), isWinner g PCWorld.actual = false

Contrast with Stone/Brasoveanu: the entities EXIST in the actual world (alice and bob are real candidates), but the description WINNER is empty there. The "in" predicate would say alice/bob exist → felicitous. PIP says the DESCRIPTION yields nothing at actual → infelicitous.

theorem KeshetAbney2024.candidate_label_registered (d : Semantics.PIP.Discourse PCWorld PCEntity) : (candidateSentence d).labels.registered αWinner = true

The label is registered (the mechanism works), but the description cannot be satisfied at the actual world.

theorem KeshetAbney2024.pip_intensional_anaphora_contrast : (∀ (g : Semantics.Dynamic.Core.ICDRTAssignment IBWorld IBEntity), isBurgerAt g IBWorld.actual = false) ∧ ∀ (g : Semantics.Dynamic.Core.ICDRTAssignment IAWorld IAEntity) (w : IAWorld), ((g⟦vAnimal⟧ᵢ) w == Semantics.Dynamic.Core.Entity.some IAEntity.animal) = true → isAnimalInShed g w = true

The paper's core contribution (§3): might blocks anaphora, must allows it.

The mechanism is the same for both (label + retrieveDef). The difference:

• must guarantees the description holds at the evaluation world (realistic base)
• might only guarantees SOME accessible world

Since the pronoun's existential presupposition (paper item 9) requires the description to hold at the evaluation world, might fails and must succeeds.

theorem KeshetAbney2024.labels_registered_in_both_cases : (∀ (d : Semantics.PIP.Discourse IBWorld IBEntity), (burgerSentence d).labels.registered αBurger = true) ∧ ∀ (d : Semantics.PIP.Discourse IAWorld IAEntity), (animalSentence d).labels.registered αAnimal = true

Labels are registered in BOTH cases — the asymmetry is about world-dependence of the description, not label availability.

theorem KeshetAbney2024.felicity_might_blocks : (Semantics.PIP.Felicity.singlePresup fun (w : IBWorld) => w == IBWorld.burgerW).felicitous IBWorld.actual = false

Static felicity operator F distinguishes might from must.

theorem KeshetAbney2024.felicity_must_allows : (Semantics.PIP.Felicity.singlePresup fun (x : IAWorld) => true).felicitous IAWorld.actual = true

theorem KeshetAbney2024.label_monotonicity_is_uniform : (∀ (d : Semantics.PIP.Discourse BWorld BEntity), (Semantics.PIP.negation (Semantics.PIP.existsLabeled αBath vBath {BEntity.bathroom} isBathroom (Semantics.PIP.atom isBathroom)) d).labels.registered αBath = true) ∧ (∀ (d : Semantics.PIP.Discourse IBWorld IBEntity), (burgerSentence d).labels.registered αBurger = true) ∧ (∀ (d : Semantics.PIP.Discourse IAWorld IAEntity), (animalSentence d).labels.registered αAnimal = true) ∧ ∀ (d : Semantics.PIP.Discourse SWorld SEntity), (stoneDiscourse d).labels.registered αWolf = true

PIP provides a unified account via TWO mechanisms:

1. Label monotonicity: labels survive all operators → modal subordination, bathroom sentences, donkey anaphora

2. World-dependent descriptions + existential presupposition: pronouns presuppose their description holds at the evaluation world → might blocks anaphora, must allows it

No stipulated accommodation rules, no "in" predicate (contra @cite{stone-1999} / @cite{brasoveanu-2010}), no special accessibility conditions.

Evidence: all 5 phenomena are verified by the theorems above:

• stone_discourse_consistent + stone_discourse_rejects_unbound
• bathroom_sentence_consistent + bathroom_rejects_nonupstairs
• paycheck_needs_descriptions
• burger_desc_fails_at_actual + animal_desc_succeeds
• pip_intensional_anaphora_contrast

theorem KeshetAbney2024.intensional_anaphora_is_T_axiom : iaAccess IAWorld.actual IAWorld.actual = true ∧ ibAccess IBWorld.actual IBWorld.actual = true ∧ ∀ (g : Semantics.Dynamic.Core.ICDRTAssignment IBWorld IBEntity), isBurgerAt g IBWorld.actual = false

The might/must asymmetry is grounded in descriptions, not accessibility.

Both modal bases are reflexive at .actual. The difference:

• Must (animal): the description isAnimalInShed is world-INdependent (holds at all worlds) → SINGLE succeeds at every context-set world.
• Might (burger): the description isBurgerAt is world-dependent (holds only at .burgerW) → SINGLE fails at .actual.

The T axiom is necessary but not sufficient: reflexivity guarantees the description is checked at the evaluation world, but the description itself must hold there.

theorem KeshetAbney2024.pip_cross_sentential_predictions : Phenomena.Anaphora.CrossSententialAnaphora.indefinitePersists.felicitous = true ∧ Phenomena.Anaphora.CrossSententialAnaphora.standardNegationBlocks.felicitous = false ∧ Phenomena.Anaphora.CrossSententialAnaphora.doubleNegation.felicitous = true

PIP predicts the standard cross-sentential anaphora pattern:

• Indefinite persistence (Karttunen 1969): ∃^α introduces a label that persists through sequential conjunction → pronoun resolves via DEF_α.
• Standard negation blocks (Heim 1982): negation filters the info state, and the CONJUNCTION version ("John didn't see a bird. It was singing.") fails because sequential conjunction makes the second sentence evaluate in a context where no bird-assignments survive.
• Double negation enables (Elliott & Sudo 2025): ¬¬∃^α x.φ registers α in the body; label monotonicity through both negations preserves it.

The difference between standard negation blocking and double negation enabling is exactly PIP's label monotonicity: labels survive negation (labels_survive_negation), but the info state does not survive single negation in sequential discourse.

theorem KeshetAbney2024.pip_quantifier_blocking : Phenomena.Anaphora.CrossSententialAnaphora.universalBlocks.felicitous = false ∧ Phenomena.Anaphora.CrossSententialAnaphora.negativeBlocks.felicitous = false ∧ Phenomena.Anaphora.CrossSententialAnaphora.mostBlocks.felicitous = false

PIP predicts that universals and negative quantifiers block cross-sentential anaphora: ∀x.φ = ¬∃x.¬φ does not introduce a labeled existential, so no DEF_α is available.

PIP vs DPL: The Architectural Difference

DPL negation is a test: ⟦¬φ⟧(g, h) iff g = h ∧ ¬∃k. φ(g, k). The output assignment equals the input — no bindings are exported through negation. This is why ¬¬∃xφ ≠ ∃xφ in DPL (dpl_dne_fails_anaphora below): double negation doesn't recover the binding.

PIP negation propagates labels from the body: (negation φ d).labels = (φ d).labels. The info state is complemented, but the label registry survives. This is exactly what enables bathroom sentences and double-negation anaphora.

The following theorems make this architectural difference explicit.

Substrate names: DPL relations are DRS (Assignment E) from Theories/Semantics/Dynamic/Connectives/. The DPL operator aliases are substrate operations: DPLRel.neg φ is test (dneg φ), DPLRel.exists_ x φ is existsAt x φ.

theorem KeshetAbney2024.dpl_neg_is_test (E : Type u_1) (φ : Semantics.Dynamic.Core.DynProp.DRS (Core.Assignment E)) (g h : Core.Assignment E) : [∼φ] g h → g = h

DPL negation resets the output assignment — it cannot export bindings.

This is the key structural property of DPL that blocks cross-negation anaphora: after ¬φ (test (dneg φ)), the output assignment equals the input, so any variables bound inside φ are inaccessible.

theorem KeshetAbney2024.pip_neg_preserves_labels (d : Semantics.PIP.Discourse BWorld BEntity) (φ : Semantics.PIP.PUpdate BWorld BEntity) (α : Semantics.PIP.FLabel) (desc : Semantics.PIP.Description BWorld BEntity) : (φ d).labels.lookup α = some desc → (Semantics.PIP.negation φ d).labels.lookup α = some desc

PIP negation preserves labels — it CAN export descriptive content.

This is the fundamental advantage of PIP over DPL: even though the info state is complemented (like DPL's test), the label registry propagates outward. The pronoun resolves via DEF_α (label lookup), not via assignment binding.

theorem KeshetAbney2024.pip_solves_dpl_negation_problem : (∃ (x : ℕ) (φ : Semantics.Dynamic.Core.DynProp.DRS (Core.Assignment ℕ)), [∼[∼Semantics.Dynamic.Core.existsAt x φ]] ≠ Semantics.Dynamic.Core.existsAt x φ) ∧ ∀ (d : Semantics.PIP.Discourse BWorld BEntity), (Semantics.PIP.negation (Semantics.PIP.existsLabeled αBath vBath {BEntity.bathroom} isBathroom (Semantics.PIP.atom isBathroom)) d).labels.registered αBath = true

The contrast: DPL negation blocks anaphora (test), PIP negation allows it (labels survive). This is the architectural reason bathroom sentences are infelicitous in DPL but felicitous in PIP.

Concretely:

• dpl_dne_fails_anaphora (above): ¬¬∃x.φ ≠ ∃x.φ in DPL (double negation doesn't recover binding)
• bathroom_mechanism: labels survive through negation in PIP (the bathroom sentence works because αBath is registered despite negation)

Presupposition projection bridges are in PIP.Bridges:

• pip_felicity_agrees_with_andFilter — F(φ ∧ ψ) ↔ andFilter
• pip_felicity_agrees_with_neg — F(¬φ) ↔ PrProp.neg
• pip_felicity_agrees_with_impFilter — F(φ → ψ) ↔ impFilter
• pip_felicity_agrees_with_orFilter — F(φ ∨ ψ) decomposition

PIP Donkey Derivation

"Every farmer who owns a donkey beats it." (paper items 53–56)

PIP analysis: ∀x(farmer(x) ∧ ∃^αD y(donkey(y) ∧ owns(x,y)) → beats(x, DEF_αD{y}))

The label αD for the donkey is registered inside the restrictor's existential. Because ∀ = ¬∃¬ and labels survive both negations, αD is available in the nuclear scope for DEF_αD retrieval.

Key property: formula label subordination. The label αD is subordinated to the restrictor — its descriptive content is "donkey(y) ∧ owns(x,y)". When the pronoun "it" (= DEF_αD{y}) is resolved, it finds the unique donkey owned by the farmer under discussion.

inductive KeshetAbney2024.DWorld : Type

• w0 : DWorld

@[implicit_reducible]

instance KeshetAbney2024.instDecidableEqDWorld : DecidableEq DWorld

Equations

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

def KeshetAbney2024.instReprDWorld.repr : DWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KeshetAbney2024.instReprDWorld : Repr DWorld

Equations

• KeshetAbney2024.instReprDWorld = { reprPrec := KeshetAbney2024.instReprDWorld.repr }

@[implicit_reducible]

instance KeshetAbney2024.instInhabitedDWorld : Inhabited DWorld

Equations

• KeshetAbney2024.instInhabitedDWorld = { default := KeshetAbney2024.instInhabitedDWorld.default }

def KeshetAbney2024.instInhabitedDWorld.default : DWorld

Equations

• KeshetAbney2024.instInhabitedDWorld.default = KeshetAbney2024.DWorld.w0

inductive KeshetAbney2024.DEntity : Type

• farmer1 : DEntity
• farmer2 : DEntity
• donkey1 : DEntity
• donkey2 : DEntity

@[implicit_reducible]

instance KeshetAbney2024.instDecidableEqDEntity : DecidableEq DEntity

Equations

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

def KeshetAbney2024.instReprDEntity.repr : DEntity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KeshetAbney2024.instReprDEntity : Repr DEntity

Equations

• KeshetAbney2024.instReprDEntity = { reprPrec := KeshetAbney2024.instReprDEntity.repr }

@[implicit_reducible]

instance KeshetAbney2024.instInhabitedDEntity : Inhabited DEntity

Equations

• KeshetAbney2024.instInhabitedDEntity = { default := KeshetAbney2024.instInhabitedDEntity.default }

def KeshetAbney2024.instInhabitedDEntity.default : DEntity

Equations

• KeshetAbney2024.instInhabitedDEntity.default = KeshetAbney2024.DEntity.farmer1

def KeshetAbney2024.dWorlds : List DWorld

Equations

• KeshetAbney2024.dWorlds = [KeshetAbney2024.DWorld.w0]

def KeshetAbney2024.αDonkey : Semantics.PIP.FLabel

Equations

• KeshetAbney2024.αDonkey = { idx := 30 }

def KeshetAbney2024.vFarmer : Semantics.Dynamic.Core.IVar

Equations

• KeshetAbney2024.vFarmer = { idx := 30 }

def KeshetAbney2024.vDonkey : Semantics.Dynamic.Core.IVar

Equations

• KeshetAbney2024.vDonkey = { idx := 31 }

def KeshetAbney2024.isFarmer (g : Semantics.Dynamic.Core.ICDRTAssignment DWorld DEntity) (w : DWorld) : Bool

Equations

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

def KeshetAbney2024.isDonkey (g : Semantics.Dynamic.Core.ICDRTAssignment DWorld DEntity) (w : DWorld) : Bool

Equations

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

def KeshetAbney2024.owns (g : Semantics.Dynamic.Core.ICDRTAssignment DWorld DEntity) (w : DWorld) : Bool

Ownership: farmer1 owns donkey1, farmer2 owns donkey2.

Equations

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

def KeshetAbney2024.beats (g : Semantics.Dynamic.Core.ICDRTAssignment DWorld DEntity) (w : DWorld) : Bool

Beating: every farmer who owns a donkey beats it.

Equations

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

def KeshetAbney2024.donkeySentence : Semantics.PIP.PUpdate DWorld DEntity

"Every farmer who owns a donkey beats it."

PIP formula: ∀x(farmer(x) ∧ ∃^αD y(donkey(y) ∧ owns(x,y)) → beats(x, DEF_αD))

Dynamic encoding: forall_ = ¬∃¬, with labeled existential for the donkey.

Equations

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

@[implicit_reducible]

instance KeshetAbney2024.instFintypeDWorld : Fintype DWorld

Equations

• KeshetAbney2024.instFintypeDWorld = { elems := {KeshetAbney2024.DWorld.w0}, complete := KeshetAbney2024.instFintypeDWorld._proof_1 }

theorem KeshetAbney2024.donkey_label_registered (d : Semantics.PIP.Discourse DWorld DEntity) : (donkeySentence d).labels.registered αDonkey = true

The donkey label is registered through the forall (¬∃¬).

Cross-Attitude Anaphora: Hob-Nob

"Hob thinks a witch blighted his mare. Nob wonders whether she (the same witch) killed his cow." (Geach 1967)

PIP analysis (paper items 91–93): The label αWitch is registered under Hob's belief attitude. Nob's wonder attitude retrieves the same label. Label persistence across attitude operators is the same mechanism as modal subordination.

Key property: labels are part of the discourse state, not the information state. Since attitudes (like modals) affect only the info state while preserving labels, cross-attitude anaphora works by the same mechanism as cross-modal anaphora.

inductive KeshetAbney2024.HNWorld : Type

• actual : HNWorld
• hobBelief : HNWorld
• nobWonder : HNWorld

@[implicit_reducible]

instance KeshetAbney2024.instDecidableEqHNWorld : DecidableEq HNWorld

Equations

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

def KeshetAbney2024.instReprHNWorld.repr : HNWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KeshetAbney2024.instReprHNWorld : Repr HNWorld

Equations

• KeshetAbney2024.instReprHNWorld = { reprPrec := KeshetAbney2024.instReprHNWorld.repr }

def KeshetAbney2024.instInhabitedHNWorld.default : HNWorld

Equations

• KeshetAbney2024.instInhabitedHNWorld.default = KeshetAbney2024.HNWorld.actual

@[implicit_reducible]

instance KeshetAbney2024.instInhabitedHNWorld : Inhabited HNWorld

Equations

• KeshetAbney2024.instInhabitedHNWorld = { default := KeshetAbney2024.instInhabitedHNWorld.default }

inductive KeshetAbney2024.HNEntity : Type

• witch : HNEntity

@[implicit_reducible]

instance KeshetAbney2024.instDecidableEqHNEntity : DecidableEq HNEntity

Equations

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

def KeshetAbney2024.instReprHNEntity.repr : HNEntity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KeshetAbney2024.instReprHNEntity : Repr HNEntity

Equations

• KeshetAbney2024.instReprHNEntity = { reprPrec := KeshetAbney2024.instReprHNEntity.repr }

@[implicit_reducible]

instance KeshetAbney2024.instInhabitedHNEntity : Inhabited HNEntity

Equations

• KeshetAbney2024.instInhabitedHNEntity = { default := KeshetAbney2024.instInhabitedHNEntity.default }

def KeshetAbney2024.instInhabitedHNEntity.default : HNEntity

Equations

• KeshetAbney2024.instInhabitedHNEntity.default = KeshetAbney2024.HNEntity.witch

def KeshetAbney2024.hnWorlds : List HNWorld

Equations

• KeshetAbney2024.hnWorlds = [KeshetAbney2024.HNWorld.actual, KeshetAbney2024.HNWorld.hobBelief, KeshetAbney2024.HNWorld.nobWonder]

def KeshetAbney2024.αWitch : Semantics.PIP.FLabel

Equations

• KeshetAbney2024.αWitch = { idx := 40 }

def KeshetAbney2024.vWitch : Semantics.Dynamic.Core.IVar

Equations

• KeshetAbney2024.vWitch = { idx := 40 }

def KeshetAbney2024.hobAccess : Semantics.PIP.BAccessRel HNWorld

Hob's doxastic accessibility: Hob believes from actual to hobBelief.

Equations

• KeshetAbney2024.hobAccess KeshetAbney2024.HNWorld.actual KeshetAbney2024.HNWorld.hobBelief = true
• KeshetAbney2024.hobAccess x✝¹ x✝ = false

def KeshetAbney2024.nobAccess : Semantics.PIP.BAccessRel HNWorld

Nob's bouletic accessibility: Nob wonders from actual to nobWonder.

Equations

• KeshetAbney2024.nobAccess KeshetAbney2024.HNWorld.actual KeshetAbney2024.HNWorld.nobWonder = true
• KeshetAbney2024.nobAccess x✝¹ x✝ = false

def KeshetAbney2024.isWitch (g : Semantics.Dynamic.Core.ICDRTAssignment HNWorld HNEntity) (w : HNWorld) : Bool

Equations

• KeshetAbney2024.isWitch g w = ((g⟦KeshetAbney2024.vWitch⟧ᵢ) w == Semantics.Dynamic.Core.Entity.some KeshetAbney2024.HNEntity.witch)

def KeshetAbney2024.hobBelief : Semantics.PIP.PUpdate HNWorld HNEntity

Hob's belief: "a witch blighted his mare"

Equations

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

def KeshetAbney2024.nobWonder : Semantics.PIP.PUpdate HNWorld HNEntity

Nob's wonder: "she killed his cow" — retrieves αWitch from Hob's belief.

Equations

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

def KeshetAbney2024.hobNobDiscourse : Semantics.PIP.PUpdate HNWorld HNEntity

The full Hob-Nob discourse.

Equations

• KeshetAbney2024.hobNobDiscourse = Semantics.PIP.conj KeshetAbney2024.hobBelief KeshetAbney2024.nobWonder

theorem KeshetAbney2024.hobnob_label_persists (d : Semantics.PIP.Discourse HNWorld HNEntity) : (hobBelief d).labels.registered αWitch = true

The witch label survives from Hob's belief to Nob's wonder.

theorem KeshetAbney2024.hobnob_full_label_available (d : Semantics.PIP.Discourse HNWorld HNEntity) : (hobNobDiscourse d).labels.registered αWitch = true

After the full discourse, αWitch is still available.

DPL vs ICDRT vs PIP: Coverage Comparison

The three frameworks have different coverage profiles for anaphora phenomena. PIP's descriptive content mechanism handles all cases uniformly; DPL and ICDRT each miss some.

Phenomenon	DPL	ICDRT	PIP
Cross-sentential	✓	✓	✓
Negation blocks	✓	✓	✓
Donkey anaphora	✓	✓	✓
Double negation	✗	✓	✓
Bathroom sentences	✗	✓	✓
Modal subordination	✗	✓	✓
Paycheck pronouns	✗	✗	✓
Intensional anaphora	✗	✗	✓

structure KeshetAbney2024.CoverageDatum : Type

Coverage datum for framework comparison.

• phenomenon : String
• dpl : Bool
• icdrt : Bool
• pip : Bool

def KeshetAbney2024.instReprCoverageDatum.repr : CoverageDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KeshetAbney2024.instReprCoverageDatum : Repr CoverageDatum

Equations

• KeshetAbney2024.instReprCoverageDatum = { reprPrec := KeshetAbney2024.instReprCoverageDatum.repr }

def KeshetAbney2024.coverageData : List CoverageDatum

Equations

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

theorem KeshetAbney2024.pip_covers_all : (coverageData.all fun (x : CoverageDatum) => x.pip) = true

PIP covers all phenomena (all pip fields are true).

theorem KeshetAbney2024.dpl_misses_five : (List.filter (fun (x : CoverageDatum) => !x.dpl) coverageData).length = 5

DPL misses 5 phenomena.

theorem KeshetAbney2024.icdrt_misses_two : (List.filter (fun (x : CoverageDatum) => !x.icdrt) coverageData).length = 2

ICDRT misses 2 phenomena (paycheck + intensional).

theorem KeshetAbney2024.pip_extends_icdrt : (coverageData.all fun (d : CoverageDatum) => !d.icdrt || d.pip) = true

PIP strictly extends ICDRT: everything ICDRT covers, PIP covers too.

theorem KeshetAbney2024.pip_extends_dpl : (coverageData.all fun (d : CoverageDatum) => !d.dpl || d.pip) = true

PIP strictly extends DPL.