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 native_decide verification.

inductive Phenomena.Anaphora.Studies.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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instDecidableEqSWorld : DecidableEq SWorld

Equations

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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instReprSWorld : Repr SWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instReprSWorld = { reprPrec := Phenomena.Anaphora.Studies.KeshetAbney2024.instReprSWorld.repr }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instReprSWorld.repr : SWorld → ℕ → Std.Format

Equations

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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqSWorld : BEq SWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqSWorld = { beq := Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqSWorld.beq }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqSWorld.beq : SWorld → SWorld → Bool

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqSWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedSWorld.default : SWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedSWorld.default = Phenomena.Anaphora.Studies.KeshetAbney2024.SWorld.actual

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedSWorld : Inhabited SWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedSWorld = { default := Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedSWorld.default }

inductive Phenomena.Anaphora.Studies.KeshetAbney2024.SEntity : Type

• wolf : SEntity

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instDecidableEqSEntity : DecidableEq SEntity

Equations

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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instReprSEntity : Repr SEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instReprSEntity = { reprPrec := Phenomena.Anaphora.Studies.KeshetAbney2024.instReprSEntity.repr }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instReprSEntity.repr : SEntity → ℕ → Std.Format

Equations

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

def Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqSEntity.beq : SEntity → SEntity → Bool

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqSEntity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqSEntity : BEq SEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqSEntity = { beq := Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqSEntity.beq }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedSEntity.default : SEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedSEntity.default = Phenomena.Anaphora.Studies.KeshetAbney2024.SEntity.wolf

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedSEntity : Inhabited SEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedSEntity = { default := Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedSEntity.default }

def Phenomena.Anaphora.Studies.KeshetAbney2024.sWorlds : List SWorld

Equations

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

def Phenomena.Anaphora.Studies.KeshetAbney2024.αWolf : Semantics.PIP.FLabel

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.αWolf = { idx := 0 }

def Phenomena.Anaphora.Studies.KeshetAbney2024.vWolf : Semantics.Dynamic.Core.IVar

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.vWolf = { idx := 0 }

def Phenomena.Anaphora.Studies.KeshetAbney2024.sAccess : Core.ModalLogic.AccessRel SWorld

Epistemic accessibility from actual world.

Equations

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

def Phenomena.Anaphora.Studies.KeshetAbney2024.isWolf (g : Semantics.Dynamic.Core.ICDRTAssignment SWorld SEntity) (_w : SWorld) : Bool

Equations

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

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

Equations

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

def Phenomena.Anaphora.Studies.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 Phenomena.Anaphora.Studies.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 Phenomena.Anaphora.Studies.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 Phenomena.Anaphora.Studies.KeshetAbney2024.stoneDiscourse : Semantics.PIP.PUpdate SWorld SEntity

Equations

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

theorem Phenomena.Anaphora.Studies.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 Phenomena.Anaphora.Studies.KeshetAbney2024.stone_discourse_consistent : Set.Nonempty (stoneDiscourse Phenomena.Anaphora.Studies.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 Phenomena.Anaphora.Studies.KeshetAbney2024.stone_discourse_rejects_unbound : (Phenomena.Anaphora.Studies.KeshetAbney2024.g₀_stone✝, SWorld.actual) ∉ (stoneSentence1 Phenomena.Anaphora.Studies.KeshetAbney2024.stone_d₀✝).info

Negative test: unbound wolf variable is rejected.

inductive Phenomena.Anaphora.Studies.KeshetAbney2024.BWorld : Type

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

• bath : BWorld
• noBath : BWorld

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instDecidableEqBWorld : DecidableEq BWorld

Equations

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

def Phenomena.Anaphora.Studies.KeshetAbney2024.instReprBWorld.repr : BWorld → ℕ → Std.Format

Equations

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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instReprBWorld : Repr BWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instReprBWorld = { reprPrec := Phenomena.Anaphora.Studies.KeshetAbney2024.instReprBWorld.repr }

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqBWorld : BEq BWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqBWorld = { beq := Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqBWorld.beq }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqBWorld.beq : BWorld → BWorld → Bool

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqBWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedBWorld : Inhabited BWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedBWorld = { default := Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedBWorld.default }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedBWorld.default : BWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedBWorld.default = Phenomena.Anaphora.Studies.KeshetAbney2024.BWorld.bath

inductive Phenomena.Anaphora.Studies.KeshetAbney2024.BEntity : Type

• bathroom : BEntity

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instDecidableEqBEntity : DecidableEq BEntity

Equations

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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instReprBEntity : Repr BEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instReprBEntity = { reprPrec := Phenomena.Anaphora.Studies.KeshetAbney2024.instReprBEntity.repr }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instReprBEntity.repr : BEntity → ℕ → Std.Format

Equations

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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqBEntity : BEq BEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqBEntity = { beq := Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqBEntity.beq }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqBEntity.beq : BEntity → BEntity → Bool

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqBEntity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedBEntity.default : BEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedBEntity.default = Phenomena.Anaphora.Studies.KeshetAbney2024.BEntity.bathroom

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedBEntity : Inhabited BEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedBEntity = { default := Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedBEntity.default }

def Phenomena.Anaphora.Studies.KeshetAbney2024.αBath : Semantics.PIP.FLabel

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.αBath = { idx := 1 }

def Phenomena.Anaphora.Studies.KeshetAbney2024.vBath : Semantics.Dynamic.Core.IVar

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.vBath = { idx := 1 }

def Phenomena.Anaphora.Studies.KeshetAbney2024.isBathroom (g : Semantics.Dynamic.Core.ICDRTAssignment BWorld BEntity) (_w : BWorld) : Bool

Equations

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

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

Equations

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

def Phenomena.Anaphora.Studies.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 Phenomena.Anaphora.Studies.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 Phenomena.Anaphora.Studies.KeshetAbney2024.bathroom_sentence_consistent : Set.Nonempty (bathroomSentence Phenomena.Anaphora.Studies.KeshetAbney2024.bath_d₀✝).info

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

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

Negative test: bathroom at noBath world is rejected.

inductive Phenomena.Anaphora.Studies.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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instDecidableEqPEntity : DecidableEq PEntity

Equations

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

def Phenomena.Anaphora.Studies.KeshetAbney2024.instReprPEntity.repr : PEntity → ℕ → Std.Format

Equations

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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instReprPEntity : Repr PEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instReprPEntity = { reprPrec := Phenomena.Anaphora.Studies.KeshetAbney2024.instReprPEntity.repr }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqPEntity.beq : PEntity → PEntity → Bool

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqPEntity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqPEntity : BEq PEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqPEntity = { beq := Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqPEntity.beq }

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedPEntity : Inhabited PEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedPEntity = { default := Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedPEntity.default }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedPEntity.default : PEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedPEntity.default = Phenomena.Anaphora.Studies.KeshetAbney2024.PEntity.john

def Phenomena.Anaphora.Studies.KeshetAbney2024.αPaycheck : Semantics.PIP.FLabel

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.αPaycheck = { idx := 2 }

def Phenomena.Anaphora.Studies.KeshetAbney2024.vPaycheck : Semantics.Dynamic.Core.IVar

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.vPaycheck = { idx := 2 }

def Phenomena.Anaphora.Studies.KeshetAbney2024.vPossessor : Semantics.Dynamic.Core.IVar

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.vPossessor = { idx := 3 }

inductive Phenomena.Anaphora.Studies.KeshetAbney2024.PWorld : Type

• w0 : PWorld

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instDecidableEqPWorld : DecidableEq PWorld

Equations

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

def Phenomena.Anaphora.Studies.KeshetAbney2024.instReprPWorld.repr : PWorld → ℕ → Std.Format

Equations

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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instReprPWorld : Repr PWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instReprPWorld = { reprPrec := Phenomena.Anaphora.Studies.KeshetAbney2024.instReprPWorld.repr }

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqPWorld : BEq PWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqPWorld = { beq := Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqPWorld.beq }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqPWorld.beq : PWorld → PWorld → Bool

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqPWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedPWorld : Inhabited PWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedPWorld = { default := Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedPWorld.default }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedPWorld.default : PWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedPWorld.default = Phenomena.Anaphora.Studies.KeshetAbney2024.PWorld.w0

def Phenomena.Anaphora.Studies.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 Phenomena.Anaphora.Studies.KeshetAbney2024.paycheck_needs_descriptions : have g := { indiv := fun (v : Semantics.Dynamic.Core.IVar) => 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.

def Phenomena.Anaphora.Studies.KeshetAbney2024.summationFiltered {W : Type u_1} {E : Type u_2} (c : Semantics.Dynamic.IntensionalCDRT.IContext W E) (v : Semantics.Dynamic.Core.IVar) (φ : Semantics.Dynamic.Core.ICDRTAssignment W E → W → Bool) : Set (Semantics.Dynamic.Core.Entity E)

Summation: Σxφ = ⋃{g(x) : g ∈ G, ⟦φ⟧^{M,{g},w*} = 1}

Collects entity values across assignments. For "Every farmer bought a donkey. They paid a lot for them.", "them" = Σx(donkey(x)).

Equations

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

def Phenomena.Anaphora.Studies.KeshetAbney2024.summationValues {W : Type u_1} {E : Type u_2} (c : Semantics.Dynamic.IntensionalCDRT.IContext W E) (v : Semantics.Dynamic.Core.IVar) : Set (Semantics.Dynamic.Core.Entity E)

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.summationValues c v = {e : Semantics.Dynamic.Core.Entity E | ∃ (g : Semantics.Dynamic.Core.ICDRTAssignment W E) (w : W), (g, w) ∈ c ∧ g⟦v⟧ᵢ = e}

theorem Phenomena.Anaphora.Studies.KeshetAbney2024.summationValues_eq_trivial_filter {W : Type u_1} {E : Type u_2} (c : Semantics.Dynamic.IntensionalCDRT.IContext W E) (v : Semantics.Dynamic.Core.IVar) : summationValues c v = summationFiltered c v fun (x : Semantics.Dynamic.Core.ICDRTAssignment W E) (x_1 : W) => true

theorem Phenomena.Anaphora.Studies.KeshetAbney2024.summation_nonempty {W : Type u_1} {E : Type u_2} (c : Semantics.Dynamic.IntensionalCDRT.IContext W E) (v : Semantics.Dynamic.Core.IVar) (gw : Semantics.Dynamic.Core.ICDRTAssignment W E × W) (h : gw ∈ c) : gw.1⟦v⟧ᵢ ∈ summationValues c v

inductive Phenomena.Anaphora.Studies.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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instDecidableEqModalContinuation : DecidableEq ModalContinuation

Equations

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

def Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqModalContinuation.beq : ModalContinuation → ModalContinuation → Bool

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqModalContinuation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqModalContinuation : BEq ModalContinuation

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqModalContinuation = { beq := Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqModalContinuation.beq }

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instReprModalContinuation : Repr ModalContinuation

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instReprModalContinuation = { reprPrec := Phenomena.Anaphora.Studies.KeshetAbney2024.instReprModalContinuation.repr }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instReprModalContinuation.repr : ModalContinuation → ℕ → Std.Format

Equations

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

def Phenomena.Anaphora.Studies.KeshetAbney2024.classifyModal2 : String → ModalContinuation

Classify an English modal by whether it subordinates.

Equations

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

def Phenomena.Anaphora.Studies.KeshetAbney2024.pipPredictsModalSub (datum : ModalSubordination.ModalSubDatum) : Bool

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

Equations

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

theorem Phenomena.Anaphora.Studies.KeshetAbney2024.pip_wolf_might_would : pipPredictsModalSub ModalSubordination.wolfMightWould = true

theorem Phenomena.Anaphora.Studies.KeshetAbney2024.pip_wolf_might_could : pipPredictsModalSub ModalSubordination.wolfMightCould = true

theorem Phenomena.Anaphora.Studies.KeshetAbney2024.pip_wolf_indicative_fails : pipPredictsModalSub ModalSubordination.wolfMightIndicative = false

theorem Phenomena.Anaphora.Studies.KeshetAbney2024.pip_wolf_will_fails : pipPredictsModalSub ModalSubordination.wolfMightWill = false

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

theorem Phenomena.Anaphora.Studies.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 Phenomena.Anaphora.Studies.KeshetAbney2024.pip_classic_bathroom : BathroomSentences.classicBathroom.felicitous = true

theorem Phenomena.Anaphora.Studies.KeshetAbney2024.pip_negation_blocks : BathroomSentences.standardNegation.felicitous = false

theorem Phenomena.Anaphora.Studies.KeshetAbney2024.pip_conjunction_fails : BathroomSentences.conjunctionVersion.felicitous = false

theorem Phenomena.Anaphora.Studies.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 Phenomena.Anaphora.Studies.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 Phenomena.Anaphora.Studies.KeshetAbney2024.pip_geach_donkey : DonkeyAnaphora.geachDonkey.boundReading = true

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

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

inductive Phenomena.Anaphora.Studies.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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instDecidableEqIBWorld : DecidableEq IBWorld

Equations

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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instReprIBWorld : Repr IBWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instReprIBWorld = { reprPrec := Phenomena.Anaphora.Studies.KeshetAbney2024.instReprIBWorld.repr }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instReprIBWorld.repr : IBWorld → ℕ → Std.Format

Equations

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

def Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqIBWorld.beq : IBWorld → IBWorld → Bool

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqIBWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqIBWorld : BEq IBWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqIBWorld = { beq := Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqIBWorld.beq }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedIBWorld.default : IBWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedIBWorld.default = Phenomena.Anaphora.Studies.KeshetAbney2024.IBWorld.actual

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedIBWorld : Inhabited IBWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedIBWorld = { default := Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedIBWorld.default }

inductive Phenomena.Anaphora.Studies.KeshetAbney2024.IBEntity : Type

• burger : IBEntity

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instDecidableEqIBEntity : DecidableEq IBEntity

Equations

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

def Phenomena.Anaphora.Studies.KeshetAbney2024.instReprIBEntity.repr : IBEntity → ℕ → Std.Format

Equations

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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instReprIBEntity : Repr IBEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instReprIBEntity = { reprPrec := Phenomena.Anaphora.Studies.KeshetAbney2024.instReprIBEntity.repr }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqIBEntity.beq : IBEntity → IBEntity → Bool

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqIBEntity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqIBEntity : BEq IBEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqIBEntity = { beq := Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqIBEntity.beq }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedIBEntity.default : IBEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedIBEntity.default = Phenomena.Anaphora.Studies.KeshetAbney2024.IBEntity.burger

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedIBEntity : Inhabited IBEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedIBEntity = { default := Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedIBEntity.default }

def Phenomena.Anaphora.Studies.KeshetAbney2024.ibWorlds : List IBWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.ibWorlds = [Phenomena.Anaphora.Studies.KeshetAbney2024.IBWorld.actual, Phenomena.Anaphora.Studies.KeshetAbney2024.IBWorld.burgerW]

def Phenomena.Anaphora.Studies.KeshetAbney2024.αBurger : Semantics.PIP.FLabel

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.αBurger = { idx := 10 }

def Phenomena.Anaphora.Studies.KeshetAbney2024.vBurger : Semantics.Dynamic.Core.IVar

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.vBurger = { idx := 10 }

def Phenomena.Anaphora.Studies.KeshetAbney2024.ibAccess : Core.ModalLogic.AccessRel IBWorld

Equations

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

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

World-dependent predicate: burger exists only at burgerW.

Equations

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

def Phenomena.Anaphora.Studies.KeshetAbney2024.burgerSentence : Semantics.PIP.PUpdate IBWorld IBEntity

Equations

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

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

theorem Phenomena.Anaphora.Studies.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.

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instFiniteWorldsIBWorld : Core.Proposition.FiniteWorlds IBWorld

Equations

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

theorem Phenomena.Anaphora.Studies.KeshetAbney2024.burger_not_realistic : ibAccess IBWorld.actual IBWorld.actual = false

Might does NOT give reflexivity at .actual — ibAccess .actual .actual = false. This is why might blocks anaphora: the evaluation world is not among the accessible worlds, so the description need not hold there.

inductive Phenomena.Anaphora.Studies.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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instDecidableEqIAWorld : DecidableEq IAWorld

Equations

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

def Phenomena.Anaphora.Studies.KeshetAbney2024.instReprIAWorld.repr : IAWorld → ℕ → Std.Format

Equations

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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instReprIAWorld : Repr IAWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instReprIAWorld = { reprPrec := Phenomena.Anaphora.Studies.KeshetAbney2024.instReprIAWorld.repr }

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqIAWorld : BEq IAWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqIAWorld = { beq := Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqIAWorld.beq }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqIAWorld.beq : IAWorld → IAWorld → Bool

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqIAWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedIAWorld.default : IAWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedIAWorld.default = Phenomena.Anaphora.Studies.KeshetAbney2024.IAWorld.actual

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedIAWorld : Inhabited IAWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedIAWorld = { default := Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedIAWorld.default }

inductive Phenomena.Anaphora.Studies.KeshetAbney2024.IAEntity : Type

• animal : IAEntity

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instDecidableEqIAEntity : DecidableEq IAEntity

Equations

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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instReprIAEntity : Repr IAEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instReprIAEntity = { reprPrec := Phenomena.Anaphora.Studies.KeshetAbney2024.instReprIAEntity.repr }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instReprIAEntity.repr : IAEntity → ℕ → Std.Format

Equations

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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqIAEntity : BEq IAEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqIAEntity = { beq := Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqIAEntity.beq }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqIAEntity.beq : IAEntity → IAEntity → Bool

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqIAEntity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedIAEntity.default : IAEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedIAEntity.default = Phenomena.Anaphora.Studies.KeshetAbney2024.IAEntity.animal

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedIAEntity : Inhabited IAEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedIAEntity = { default := Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedIAEntity.default }

def Phenomena.Anaphora.Studies.KeshetAbney2024.iaWorlds : List IAWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.iaWorlds = [Phenomena.Anaphora.Studies.KeshetAbney2024.IAWorld.actual, Phenomena.Anaphora.Studies.KeshetAbney2024.IAWorld.shedW]

def Phenomena.Anaphora.Studies.KeshetAbney2024.αAnimal : Semantics.PIP.FLabel

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.αAnimal = { idx := 11 }

def Phenomena.Anaphora.Studies.KeshetAbney2024.vAnimal : Semantics.Dynamic.Core.IVar

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.vAnimal = { idx := 11 }

def Phenomena.Anaphora.Studies.KeshetAbney2024.iaAccess : Core.ModalLogic.AccessRel IAWorld

Realistic epistemic: actual accessible from itself.

Equations

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

def Phenomena.Anaphora.Studies.KeshetAbney2024.isAnimalInShed (g : Semantics.Dynamic.Core.ICDRTAssignment IAWorld IAEntity) (_w : IAWorld) : Bool

World-INdependent predicate: holds at ALL worlds.

Equations

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

def Phenomena.Anaphora.Studies.KeshetAbney2024.animalSentence : Semantics.PIP.PUpdate IAWorld IAEntity

Equations

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

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

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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instFiniteWorldsIAWorld : Core.Proposition.FiniteWorlds IAWorld

Equations

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

theorem Phenomena.Anaphora.Studies.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 Phenomena.Anaphora.Studies.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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instDecidableEqMAWorld : DecidableEq MAWorld

Equations

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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instReprMAWorld : Repr MAWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instReprMAWorld = { reprPrec := Phenomena.Anaphora.Studies.KeshetAbney2024.instReprMAWorld.repr }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instReprMAWorld.repr : MAWorld → ℕ → Std.Format

Equations

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

def Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqMAWorld.beq : MAWorld → MAWorld → Bool

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqMAWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqMAWorld : BEq MAWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqMAWorld = { beq := Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqMAWorld.beq }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedMAWorld.default : MAWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedMAWorld.default = Phenomena.Anaphora.Studies.KeshetAbney2024.MAWorld.actual

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedMAWorld : Inhabited MAWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedMAWorld = { default := Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedMAWorld.default }

inductive Phenomena.Anaphora.Studies.KeshetAbney2024.MAEntity : Type

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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instDecidableEqMAEntity : DecidableEq MAEntity

Equations

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

def Phenomena.Anaphora.Studies.KeshetAbney2024.instReprMAEntity.repr : MAEntity → ℕ → Std.Format

Equations

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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instReprMAEntity : Repr MAEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instReprMAEntity = { reprPrec := Phenomena.Anaphora.Studies.KeshetAbney2024.instReprMAEntity.repr }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqMAEntity.beq : MAEntity → MAEntity → Bool

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqMAEntity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqMAEntity : BEq MAEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqMAEntity = { beq := Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqMAEntity.beq }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedMAEntity.default : MAEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedMAEntity.default = Phenomena.Anaphora.Studies.KeshetAbney2024.MAEntity.cat

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedMAEntity : Inhabited MAEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedMAEntity = { default := Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedMAEntity.default }

def Phenomena.Anaphora.Studies.KeshetAbney2024.maWorlds : List MAWorld

Equations

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

def Phenomena.Anaphora.Studies.KeshetAbney2024.αMA : Semantics.PIP.FLabel

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.αMA = { idx := 12 }

def Phenomena.Anaphora.Studies.KeshetAbney2024.vMA : Semantics.Dynamic.Core.IVar

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.vMA = { idx := 12 }

def Phenomena.Anaphora.Studies.KeshetAbney2024.maAccess : Core.ModalLogic.AccessRel MAWorld

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

Equations

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

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

World-dependent predicate: different animal in each world.

Equations

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

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

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

theorem Phenomena.Anaphora.Studies.KeshetAbney2024.ma_different_animals_per_world : isAnimalInShedMA { indiv := fun (v : Semantics.Dynamic.Core.IVar) => 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) => 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) => 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 Phenomena.Anaphora.Studies.KeshetAbney2024.ma_cross_world_plural : isAnimalInShedMA (Phenomena.Anaphora.Studies.KeshetAbney2024.maG✝ MAEntity.cat) MAWorld.actual = true ∧ isAnimalInShedMA (Phenomena.Anaphora.Studies.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 Phenomena.Anaphora.Studies.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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instDecidableEqPCWorld : DecidableEq PCWorld

Equations

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

def Phenomena.Anaphora.Studies.KeshetAbney2024.instReprPCWorld.repr : PCWorld → ℕ → Std.Format

Equations

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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instReprPCWorld : Repr PCWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instReprPCWorld = { reprPrec := Phenomena.Anaphora.Studies.KeshetAbney2024.instReprPCWorld.repr }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqPCWorld.beq : PCWorld → PCWorld → Bool

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqPCWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqPCWorld : BEq PCWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqPCWorld = { beq := Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqPCWorld.beq }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedPCWorld.default : PCWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedPCWorld.default = Phenomena.Anaphora.Studies.KeshetAbney2024.PCWorld.actual

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedPCWorld : Inhabited PCWorld

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedPCWorld = { default := Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedPCWorld.default }

inductive Phenomena.Anaphora.Studies.KeshetAbney2024.PCEntity : Type

• alice : PCEntity
• bob : PCEntity

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instDecidableEqPCEntity : DecidableEq PCEntity

Equations

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

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instReprPCEntity : Repr PCEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instReprPCEntity = { reprPrec := Phenomena.Anaphora.Studies.KeshetAbney2024.instReprPCEntity.repr }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instReprPCEntity.repr : PCEntity → ℕ → Std.Format

Equations

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

def Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqPCEntity.beq : PCEntity → PCEntity → Bool

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqPCEntity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqPCEntity : BEq PCEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqPCEntity = { beq := Phenomena.Anaphora.Studies.KeshetAbney2024.instBEqPCEntity.beq }

def Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedPCEntity.default : PCEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedPCEntity.default = Phenomena.Anaphora.Studies.KeshetAbney2024.PCEntity.alice

instance Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedPCEntity : Inhabited PCEntity

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedPCEntity = { default := Phenomena.Anaphora.Studies.KeshetAbney2024.instInhabitedPCEntity.default }

def Phenomena.Anaphora.Studies.KeshetAbney2024.pcWorlds : List PCWorld

Equations

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

def Phenomena.Anaphora.Studies.KeshetAbney2024.αWinner : Semantics.PIP.FLabel

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.αWinner = { idx := 20 }

def Phenomena.Anaphora.Studies.KeshetAbney2024.vWinner : Semantics.Dynamic.Core.IVar

Equations

• Phenomena.Anaphora.Studies.KeshetAbney2024.vWinner = { idx := 20 }

def Phenomena.Anaphora.Studies.KeshetAbney2024.pcAccess : Core.ModalLogic.AccessRel PCWorld

Epistemic: speaker considers all outcomes possible.

Equations

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

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

World-dependent predicate: winner only at resolution worlds.

Equations

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

def Phenomena.Anaphora.Studies.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 Phenomena.Anaphora.Studies.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 Phenomena.Anaphora.Studies.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 Phenomena.Anaphora.Studies.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 Phenomena.Anaphora.Studies.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⟧ᵢ == 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 Phenomena.Anaphora.Studies.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 Phenomena.Anaphora.Studies.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 Phenomena.Anaphora.Studies.KeshetAbney2024.felicity_must_allows : (Semantics.PIP.Felicity.singlePresup fun (x : IAWorld) => true).felicitous IAWorld.actual = true

theorem Phenomena.Anaphora.Studies.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 Phenomena.Anaphora.Studies.KeshetAbney2024.intensional_anaphora_is_T_axiom : iaAccess IAWorld.actual IAWorld.actual = true ∧ ibAccess IBWorld.actual IBWorld.actual = false

The might/must asymmetry is grounded in the T axiom of modal logic.

PIP's must agrees with Core.ModalLogic.kripkeEval .necessity (must_truth_agrees_kripkeEval). When the accessibility relation is reflexive at the evaluation world (realistic modal base), the T axiom (must_realistic_at) guarantees the description holds there — enabling anaphora. Non-reflexive might lacks this guarantee.

theorem Phenomena.Anaphora.Studies.KeshetAbney2024.pip_cross_sentential_predictions : CrossSententialAnaphora.indefinitePersists.felicitous = true ∧ CrossSententialAnaphora.standardNegationBlocks.felicitous = false ∧ 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 Phenomena.Anaphora.Studies.KeshetAbney2024.pip_quantifier_blocking : CrossSententialAnaphora.universalBlocks.felicitous = false ∧ CrossSententialAnaphora.negativeBlocks.felicitous = false ∧ 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): 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.

theorem Phenomena.Anaphora.Studies.KeshetAbney2024.dpl_neg_is_test (E : Type u_1) (φ : Semantics.Dynamic.DPL.DPLRel E) (g h : ℕ → E) : φ.neg 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 ¬φ, the output assignment equals the input, so any variables bound inside φ are inaccessible.

theorem Phenomena.Anaphora.Studies.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 Phenomena.Anaphora.Studies.KeshetAbney2024.pip_solves_dpl_negation_problem : (∃ (x : ℕ) (φ : Semantics.Dynamic.DPL.DPLRel ℕ), (Semantics.Dynamic.DPL.DPLRel.exists_ x φ).neg.neg ≠ Semantics.Dynamic.DPL.DPLRel.exists_ 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: ¬¬∃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)

theorem Phenomena.Anaphora.Studies.KeshetAbney2024.pip_felicity_agrees_with_andFilter {W : Type u_1} (φ ψ : Semantics.PIP.Felicity.PIPExpr W) (w : W) : (φ.conj ψ).felicitous w = ({ presup := φ.felicitous, assertion := φ.truth }.andFilter { presup := ψ.felicitous, assertion := ψ.truth }).presup w

PIP's F operator and Core.Presupposition.PrProp.andFilter implement the same Karttunen conjunction clause (@cite{karttunen-1973}).

PIP Felicity (PIPExpr.felicitous for .conj φ ψ): φ.felicitous w && ((φ.truth w).not || ψ.felicitous w)

PrProp.andFilter (Core.Presupposition): p.presup w && (!p.assertion w || q.presup w)

These are structurally identical: the first conjunct's felicity/presupposition must hold, AND the second conjunct's felicity/presupposition must hold whenever the first conjunct is true. The first conjunct's truth can "satisfy" the second conjunct's presupposition.

This theorem proves the correspondence by showing that PIP's F operator on conjunction produces the same Bool value as andFilter when we interpret truth as assertion and felicitous as presup.

theorem Phenomena.Anaphora.Studies.KeshetAbney2024.pip_felicity_agrees_with_neg {W : Type u_1} (φ : Semantics.PIP.Felicity.PIPExpr W) (w : W) : φ.neg.felicitous w = { presup := φ.felicitous, assertion := φ.truth }.neg.presup w

PIP's F operator for negation agrees with PrProp.neg: both preserve the presupposition/felicity of the negated expression unchanged.

theorem Phenomena.Anaphora.Studies.KeshetAbney2024.pip_presup_unconditional {W : Type u_1} (φ : Semantics.PIP.Felicity.PIPExpr W) (ψ : W → Bool) (w : W) : (φ.presup ψ).felicitous w = (φ.felicitous w && ψ w)

PIP's presupposition construct φ|ψ agrees with PrProp.andFilter where the presupposition is an atom (always felicitous) and the assertion is the presupposed content.

F(φ|ψ) = Fφ ∧ ψ andFilter(⟨Fφ, Tφ⟩, ⟨ψ, trivial⟩).presup = Fφ ∧ (!Tφ ∨ ψ)

These differ slightly: andFilter is the conjunction clause, while φ|ψ is a dedicated presupposition construct. The equivalence holds when the presupposition ψ is not conditioned on φ's truth — which is correct, since ψ must hold unconditionally for φ|ψ to be felicitous.