PIP: Worked Phenomena

@cite{keshet-abney-2024} @cite{partee-1972} @cite{roberts-1989} @cite{stone-1997}Concrete examples demonstrating how PIP handles the core anaphora puzzles via description-based retrieval over finite models:

1. Stone's puzzle: "A wolf might come. It would eat you first."
2. Bathroom sentences: "Either there's no bathroom, or it's upstairs."
3. Paycheck pronouns: "John spent his paycheck. Bill saved it."

Each example uses a small finite world/entity model with native_decide to verify PIP's predictions.

inductive Semantics.Dynamic.PIP.Phenomena.SWorld : Type

Stone's puzzle world model.

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 Semantics.Dynamic.PIP.Phenomena.instDecidableEqSWorld : DecidableEq SWorld

Equations

• Semantics.Dynamic.PIP.Phenomena.instDecidableEqSWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Dynamic.PIP.Phenomena.instReprSWorld.repr : SWorld → ℕ → Std.Format

Equations

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

instance Semantics.Dynamic.PIP.Phenomena.instReprSWorld : Repr SWorld

Equations

• Semantics.Dynamic.PIP.Phenomena.instReprSWorld = { reprPrec := Semantics.Dynamic.PIP.Phenomena.instReprSWorld.repr }

def Semantics.Dynamic.PIP.Phenomena.instBEqSWorld.beq : SWorld → SWorld → Bool

Equations

• Semantics.Dynamic.PIP.Phenomena.instBEqSWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Dynamic.PIP.Phenomena.instBEqSWorld : BEq SWorld

Equations

• Semantics.Dynamic.PIP.Phenomena.instBEqSWorld = { beq := Semantics.Dynamic.PIP.Phenomena.instBEqSWorld.beq }

def Semantics.Dynamic.PIP.Phenomena.instInhabitedSWorld.default : SWorld

Equations

• Semantics.Dynamic.PIP.Phenomena.instInhabitedSWorld.default = Semantics.Dynamic.PIP.Phenomena.SWorld.actual

instance Semantics.Dynamic.PIP.Phenomena.instInhabitedSWorld : Inhabited SWorld

Equations

• Semantics.Dynamic.PIP.Phenomena.instInhabitedSWorld = { default := Semantics.Dynamic.PIP.Phenomena.instInhabitedSWorld.default }

inductive Semantics.Dynamic.PIP.Phenomena.SEntity : Type

The entities: just one wolf.

• wolf : SEntity

instance Semantics.Dynamic.PIP.Phenomena.instDecidableEqSEntity : DecidableEq SEntity

Equations

• Semantics.Dynamic.PIP.Phenomena.instDecidableEqSEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Dynamic.PIP.Phenomena.instReprSEntity.repr : SEntity → ℕ → Std.Format

Equations

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

instance Semantics.Dynamic.PIP.Phenomena.instReprSEntity : Repr SEntity

Equations

• Semantics.Dynamic.PIP.Phenomena.instReprSEntity = { reprPrec := Semantics.Dynamic.PIP.Phenomena.instReprSEntity.repr }

instance Semantics.Dynamic.PIP.Phenomena.instBEqSEntity : BEq SEntity

Equations

• Semantics.Dynamic.PIP.Phenomena.instBEqSEntity = { beq := Semantics.Dynamic.PIP.Phenomena.instBEqSEntity.beq }

def Semantics.Dynamic.PIP.Phenomena.instBEqSEntity.beq : SEntity → SEntity → Bool

Equations

• Semantics.Dynamic.PIP.Phenomena.instBEqSEntity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Dynamic.PIP.Phenomena.instInhabitedSEntity.default : SEntity

Equations

• Semantics.Dynamic.PIP.Phenomena.instInhabitedSEntity.default = Semantics.Dynamic.PIP.Phenomena.SEntity.wolf

instance Semantics.Dynamic.PIP.Phenomena.instInhabitedSEntity : Inhabited SEntity

Equations

• Semantics.Dynamic.PIP.Phenomena.instInhabitedSEntity = { default := Semantics.Dynamic.PIP.Phenomena.instInhabitedSEntity.default }

def Semantics.Dynamic.PIP.Phenomena.sWorlds : List SWorld

All worlds in the model.

Equations

• Semantics.Dynamic.PIP.Phenomena.sWorlds = [Semantics.Dynamic.PIP.Phenomena.SWorld.actual, Semantics.Dynamic.PIP.Phenomena.SWorld.wolfIn, Semantics.Dynamic.PIP.Phenomena.SWorld.noWolf]

def Semantics.Dynamic.PIP.Phenomena.αWolf : FLabel

Formula label for "a wolf".

Equations

• Semantics.Dynamic.PIP.Phenomena.αWolf = { idx := 0 }

def Semantics.Dynamic.PIP.Phenomena.vWolf : Core.IVar

Variable for the wolf.

Equations

• Semantics.Dynamic.PIP.Phenomena.vWolf = { idx := 0 }

def Semantics.Dynamic.PIP.Phenomena.sAccess : PAccessRel SWorld

Epistemic accessibility from actual world.

The speaker considers both wolfIn and noWolf possible.

Equations

• Semantics.Dynamic.PIP.Phenomena.sAccess Semantics.Dynamic.PIP.Phenomena.SWorld.actual Semantics.Dynamic.PIP.Phenomena.SWorld.wolfIn = true
• Semantics.Dynamic.PIP.Phenomena.sAccess Semantics.Dynamic.PIP.Phenomena.SWorld.actual Semantics.Dynamic.PIP.Phenomena.SWorld.noWolf = true
• Semantics.Dynamic.PIP.Phenomena.sAccess x✝¹ x✝ = false

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

Wolf predicate: true when the wolf variable is bound to wolf.

Equations

• Semantics.Dynamic.PIP.Phenomena.isWolf g _w = (g⟦Semantics.Dynamic.PIP.Phenomena.vWolf⟧ᵢ == Semantics.Dynamic.Core.Entity.some Semantics.Dynamic.PIP.Phenomena.SEntity.wolf)

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

Come-in predicate: wolves come in only at wolfIn.

Equations

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

def Semantics.Dynamic.PIP.Phenomena.stoneSentence1 : PUpdate SWorld SEntity

Stone's sentence 1: "A wolf might come."

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

The existential is inside the modal:

• x (the wolf) is local — bound by ∃ inside might
• The world variable is external — bound by might

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

Equations

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

theorem Semantics.Dynamic.PIP.Phenomena.stone_label_registered (d : 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.

This is the crucial property: even though the wolf exists only in possible worlds, the descriptive content "wolf(x)" is available in the discourse state for subsequent anaphora.

def Semantics.Dynamic.PIP.Phenomena.stoneSentence2 : PUpdate SWorld SEntity

Stone's sentence 2: "It would eat you first."

"It" = DEF_αWolf{x} — retrieves the wolf via its description. "would" = must in the same accessibility relation.

The pronoun succeeds because αWolf was registered by sentence 1 and labels survive modal operators.

Equations

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

def Semantics.Dynamic.PIP.Phenomena.stoneDiscourse : PUpdate SWorld SEntity

The full Stone's puzzle discourse: sentence 1; sentence 2.

The discourse is well-defined (non-trivially consistent) because:

1. Sentence 1 registers αWolf and filters to worlds where a wolf might come in
2. Sentence 2 retrieves the wolf via DEF_αWolf and continues in the modal context

Equations

• Semantics.Dynamic.PIP.Phenomena.stoneDiscourse = Semantics.Dynamic.PIP.conj Semantics.Dynamic.PIP.Phenomena.stoneSentence1 Semantics.Dynamic.PIP.Phenomena.stoneSentence2

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

After the full discourse, the label is still available. Labels are monotonically accumulated through conjunction, retrieveDef, and would/must because all these operators preserve labels.

theorem Semantics.Dynamic.PIP.Phenomena.stone_discourse_consistent : Set.Nonempty (stoneDiscourse Semantics.Dynamic.PIP.Phenomena.stone_d₀✝).info

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

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

1. might: g_wolf at.actual survives because (g_wolf,.wolfIn) is in the body result (the wolf exists at.wolfIn via existsLabeled)
2. retrieveDef αWolf: succeeds because the label was registered
3. would/must: g_wolf at.actual survives because modalExpand adds (g_wolf,.wolfIn) and (g_wolf,.noWolf) to the body's input, and the atom predicate (vWolf ≠ ⋆) holds for all of them

Without modalExpand, step 3 would fail: must would check accessible worlds.wolfIn/.noWolf but find no pairs there in the body result.

theorem Semantics.Dynamic.PIP.Phenomena.stone_discourse_rejects_unbound : (Semantics.Dynamic.PIP.Phenomena.g₀_stone✝, SWorld.actual) ∉ (stoneSentence1 Semantics.Dynamic.PIP.Phenomena.stone_d₀✝).info

Negative test: an assignment with unbound wolf variable does NOT survive Stone's discourse. The existsLabeled in sentence 1 extends assignments with vWolf ↦.some.wolf, and the atom predicate isWolf requires g.indiv vWolf ==.some.wolf. An unbound assignment (vWolf = ⋆) fails this predicate check, so it cannot appear in the body result of might, and is correctly rejected.

This confirms the discourse genuinely filters — it's not vacuously accepting all assignments.

inductive Semantics.Dynamic.PIP.Phenomena.BWorld : Type

Bathroom world model.

Two possible worlds:

• bath: there is a bathroom (upstairs)
• noBath: there is no bathroom

• bath : BWorld
• noBath : BWorld

instance Semantics.Dynamic.PIP.Phenomena.instDecidableEqBWorld : DecidableEq BWorld

Equations

• Semantics.Dynamic.PIP.Phenomena.instDecidableEqBWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Dynamic.PIP.Phenomena.instReprBWorld.repr : BWorld → ℕ → Std.Format

Equations

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

instance Semantics.Dynamic.PIP.Phenomena.instReprBWorld : Repr BWorld

Equations

• Semantics.Dynamic.PIP.Phenomena.instReprBWorld = { reprPrec := Semantics.Dynamic.PIP.Phenomena.instReprBWorld.repr }

instance Semantics.Dynamic.PIP.Phenomena.instBEqBWorld : BEq BWorld

Equations

• Semantics.Dynamic.PIP.Phenomena.instBEqBWorld = { beq := Semantics.Dynamic.PIP.Phenomena.instBEqBWorld.beq }

def Semantics.Dynamic.PIP.Phenomena.instBEqBWorld.beq : BWorld → BWorld → Bool

Equations

• Semantics.Dynamic.PIP.Phenomena.instBEqBWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Dynamic.PIP.Phenomena.instInhabitedBWorld.default : BWorld

Equations

• Semantics.Dynamic.PIP.Phenomena.instInhabitedBWorld.default = Semantics.Dynamic.PIP.Phenomena.BWorld.bath

instance Semantics.Dynamic.PIP.Phenomena.instInhabitedBWorld : Inhabited BWorld

Equations

• Semantics.Dynamic.PIP.Phenomena.instInhabitedBWorld = { default := Semantics.Dynamic.PIP.Phenomena.instInhabitedBWorld.default }

inductive Semantics.Dynamic.PIP.Phenomena.BEntity : Type

The entities.

• bathroom : BEntity

instance Semantics.Dynamic.PIP.Phenomena.instDecidableEqBEntity : DecidableEq BEntity

Equations

• Semantics.Dynamic.PIP.Phenomena.instDecidableEqBEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Dynamic.PIP.Phenomena.instReprBEntity : Repr BEntity

Equations

• Semantics.Dynamic.PIP.Phenomena.instReprBEntity = { reprPrec := Semantics.Dynamic.PIP.Phenomena.instReprBEntity.repr }

def Semantics.Dynamic.PIP.Phenomena.instReprBEntity.repr : BEntity → ℕ → Std.Format

Equations

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

instance Semantics.Dynamic.PIP.Phenomena.instBEqBEntity : BEq BEntity

Equations

• Semantics.Dynamic.PIP.Phenomena.instBEqBEntity = { beq := Semantics.Dynamic.PIP.Phenomena.instBEqBEntity.beq }

def Semantics.Dynamic.PIP.Phenomena.instBEqBEntity.beq : BEntity → BEntity → Bool

Equations

• Semantics.Dynamic.PIP.Phenomena.instBEqBEntity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Dynamic.PIP.Phenomena.instInhabitedBEntity : Inhabited BEntity

Equations

• Semantics.Dynamic.PIP.Phenomena.instInhabitedBEntity = { default := Semantics.Dynamic.PIP.Phenomena.instInhabitedBEntity.default }

def Semantics.Dynamic.PIP.Phenomena.instInhabitedBEntity.default : BEntity

Equations

• Semantics.Dynamic.PIP.Phenomena.instInhabitedBEntity.default = Semantics.Dynamic.PIP.Phenomena.BEntity.bathroom

def Semantics.Dynamic.PIP.Phenomena.αBath : FLabel

Label for "a bathroom".

Equations

• Semantics.Dynamic.PIP.Phenomena.αBath = { idx := 1 }

def Semantics.Dynamic.PIP.Phenomena.vBath : Core.IVar

Variable for the bathroom.

Equations

• Semantics.Dynamic.PIP.Phenomena.vBath = { idx := 1 }

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

Bathroom predicate.

Equations

• Semantics.Dynamic.PIP.Phenomena.isBathroom g _w = (g⟦Semantics.Dynamic.PIP.Phenomena.vBath⟧ᵢ == Semantics.Dynamic.Core.Entity.some Semantics.Dynamic.PIP.Phenomena.BEntity.bathroom)

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

Upstairs predicate: the bathroom is upstairs in the bath world.

Equations

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

def Semantics.Dynamic.PIP.Phenomena.bathroomSentence : PUpdate BWorld BEntity

Partee's bathroom sentence: "Either there's no bathroom, or it's upstairs."

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

1. First disjunct: negation of labeled existential

   • The label αBath is registered even under negation
   • Records description "bathroom(x)"

2. Second disjunct: uses DEF_αBath to retrieve the bathroom

   • The description "bathroom(x)" is available because labels survive negation (the fundamental PIP insight)

This contrasts with standard DPL/DRT where negation blocks accessibility of discourse referents introduced in the negated scope.

Equations

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

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

The bathroom label is registered after the first disjunct, even though it's under negation.

theorem Semantics.Dynamic.PIP.Phenomena.bathroom_sentence_consistent : Set.Nonempty (bathroomSentence Semantics.Dynamic.PIP.Phenomena.bath_d₀✝).info

End-to-end test: the full bathroom sentence is consistent on a concrete model.

Given a universal input (all assignment-world pairs), the bathroom sentence produces a non-empty output. The witness (g₀,.noBath) survives via the first disjunct (negation): g₀ doesn't bind vBath to any entity, so it's NOT in the existsLabeled output, meaning negation keeps it.

This verifies the full compositional pipeline: disj → negation → existsLabeled → atom (first disjunct) disj → label floating → retrieveDef → atom (second disjunct)

theorem Semantics.Dynamic.PIP.Phenomena.bathroom_rejects_nonupstairs : (Semantics.Dynamic.PIP.Phenomena.g_bath✝, BWorld.noBath) ∉ (bathroomSentence Semantics.Dynamic.PIP.Phenomena.bath_d₀✝).info

Negative test: a bathroom-bound assignment at the no-bathroom world is rejected by the full bathroom sentence.

At .noBath, both disjuncts fail:

• First (negation): g_bath IS in the existential's output (it matches the isBathroom predicate), so negation removes it
• Second (upstairs): isUpstairs requires w ==.bath, but w = .noBath

This tests the genuine semantic content: the sentence says either there's no bathroom OR the bathroom is upstairs. A bathroom that isn't upstairs violates both conditions.

inductive Semantics.Dynamic.PIP.Phenomena.PEntity : Type

Paycheck pronouns:

"John spent his paycheck. Bill saved it."

"it" ≠ John's paycheck (which was already spent). "it" = "his paycheck" with "his" re-evaluated for Bill.

PIP analysis:

• "his paycheck" introduces label α with description "paycheck-of(x, possessor)" where possessor is contextually resolved
• "it" = DEF_α{x} — re-evaluates the description relative to the current assignment, where the subject is now Bill

This is the cleanest argument for description-based over value-based anaphora: the pronoun carries a function (λperson. person's paycheck), not a fixed entity.

Value-based account: "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 Semantics.Dynamic.PIP.Phenomena.instDecidableEqPEntity : DecidableEq PEntity

Equations

• Semantics.Dynamic.PIP.Phenomena.instDecidableEqPEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Dynamic.PIP.Phenomena.instReprPEntity : Repr PEntity

Equations

• Semantics.Dynamic.PIP.Phenomena.instReprPEntity = { reprPrec := Semantics.Dynamic.PIP.Phenomena.instReprPEntity.repr }

def Semantics.Dynamic.PIP.Phenomena.instReprPEntity.repr : PEntity → ℕ → Std.Format

Equations

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

instance Semantics.Dynamic.PIP.Phenomena.instBEqPEntity : BEq PEntity

Equations

• Semantics.Dynamic.PIP.Phenomena.instBEqPEntity = { beq := Semantics.Dynamic.PIP.Phenomena.instBEqPEntity.beq }

def Semantics.Dynamic.PIP.Phenomena.instBEqPEntity.beq : PEntity → PEntity → Bool

Equations

• Semantics.Dynamic.PIP.Phenomena.instBEqPEntity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Dynamic.PIP.Phenomena.instInhabitedPEntity : Inhabited PEntity

Equations

• Semantics.Dynamic.PIP.Phenomena.instInhabitedPEntity = { default := Semantics.Dynamic.PIP.Phenomena.instInhabitedPEntity.default }

def Semantics.Dynamic.PIP.Phenomena.instInhabitedPEntity.default : PEntity

Equations

• Semantics.Dynamic.PIP.Phenomena.instInhabitedPEntity.default = Semantics.Dynamic.PIP.Phenomena.PEntity.john

def Semantics.Dynamic.PIP.Phenomena.αPaycheck : FLabel

Label for the paycheck description.

Equations

• Semantics.Dynamic.PIP.Phenomena.αPaycheck = { idx := 2 }

def Semantics.Dynamic.PIP.Phenomena.vPaycheck : Core.IVar

Variable for the paycheck.

Equations

• Semantics.Dynamic.PIP.Phenomena.vPaycheck = { idx := 2 }

def Semantics.Dynamic.PIP.Phenomena.vPossessor : Core.IVar

Variable for the possessor.

Equations

• Semantics.Dynamic.PIP.Phenomena.vPossessor = { idx := 3 }

inductive Semantics.Dynamic.PIP.Phenomena.PWorld : Type

Single-world model (paycheck is non-modal).

• w0 : PWorld

instance Semantics.Dynamic.PIP.Phenomena.instDecidableEqPWorld : DecidableEq PWorld

Equations

• Semantics.Dynamic.PIP.Phenomena.instDecidableEqPWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Dynamic.PIP.Phenomena.instReprPWorld.repr : PWorld → ℕ → Std.Format

Equations

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

instance Semantics.Dynamic.PIP.Phenomena.instReprPWorld : Repr PWorld

Equations

• Semantics.Dynamic.PIP.Phenomena.instReprPWorld = { reprPrec := Semantics.Dynamic.PIP.Phenomena.instReprPWorld.repr }

instance Semantics.Dynamic.PIP.Phenomena.instBEqPWorld : BEq PWorld

Equations

• Semantics.Dynamic.PIP.Phenomena.instBEqPWorld = { beq := Semantics.Dynamic.PIP.Phenomena.instBEqPWorld.beq }

def Semantics.Dynamic.PIP.Phenomena.instBEqPWorld.beq : PWorld → PWorld → Bool

Equations

• Semantics.Dynamic.PIP.Phenomena.instBEqPWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Dynamic.PIP.Phenomena.instInhabitedPWorld : Inhabited PWorld

Equations

• Semantics.Dynamic.PIP.Phenomena.instInhabitedPWorld = { default := Semantics.Dynamic.PIP.Phenomena.instInhabitedPWorld.default }

def Semantics.Dynamic.PIP.Phenomena.instInhabitedPWorld.default : PWorld

Equations

• Semantics.Dynamic.PIP.Phenomena.instInhabitedPWorld.default = Semantics.Dynamic.PIP.Phenomena.PWorld.w0

def Semantics.Dynamic.PIP.Phenomena.isPaycheckOf (g : Core.ICDRTAssignment PWorld PEntity) (_w : PWorld) : Bool

Paycheck-of predicate: relates a paycheck to its owner.

The key property: this predicate is relational — it depends on both the paycheck variable and the possessor variable. When the possessor changes (John → Bill), the paycheck changes too.

Equations

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

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

Description-based anaphora correctly predicts the paycheck reading because the description "paycheck-of(x, possessor)" is re-evaluated when the possessor variable changes.

In a value-based system, "it" would be bound to johnsPaycheck. In PIP, "it" = DEF_α{x} with α = "paycheck-of(x, possessor)", and the possessor variable gets rebound to bill.

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

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

PIP's formal construct for collecting entity values across assignments. Given a plural context G, a variable x, and a restricting formula φ, summation returns the set of all g(x) values for assignments g that satisfy φ. This is what handles summation pronouns:

"Every farmer bought a donkey. They paid a lot for them."

"them" = Σx(donkey(x)) = the set of ALL donkeys across all farmer-donkey pairs in the plural context G.

Equations

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

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

Unfiltered summation: collects ALL values of v across assignments.

This is a special case of summationFiltered with a trivially true filter.

Equations

• Semantics.Dynamic.PIP.Phenomena.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 Semantics.Dynamic.PIP.Phenomena.summationValues_eq_trivial_filter {W : Type u_1} {E : Type u_2} (c : IntensionalCDRT.IContext W E) (v : Core.IVar) : summationValues c v = summationFiltered c v fun (x : Core.ICDRTAssignment W E) (x_1 : W) => true

Unfiltered summation is summation with trivial filter.

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

The summation set is non-empty when the context is non-empty and the variable is bound (has a non-⋆ value).

inductive Semantics.Dynamic.PIP.Phenomena.AnaphoraStrategy : Type

The three systems compared in @cite{keshet-abney-2024}:

1. Value-based: Pronouns store entity values directly. Works for simple anaphora, fails for modal/negation/paycheck cases.

2. Description-based (PIP): Pronouns carry formula labels. Handles all cases uniformly.

3. File-change / DRT: Pronouns access discourse referents. Handles quantifier donkey cases but struggles with modal contexts (requires modal subordination stipulations).

PIP subsumes the file-change approach: descriptions that happen to pick out a unique entity degenerate to value-based behavior.

• valueBased : AnaphoraStrategy
• descriptionBased : AnaphoraStrategy
• fileChange : AnaphoraStrategy

instance Semantics.Dynamic.PIP.Phenomena.instDecidableEqAnaphoraStrategy : DecidableEq AnaphoraStrategy

Equations

• Semantics.Dynamic.PIP.Phenomena.instDecidableEqAnaphoraStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Dynamic.PIP.Phenomena.instReprAnaphoraStrategy : Repr AnaphoraStrategy

Equations

• Semantics.Dynamic.PIP.Phenomena.instReprAnaphoraStrategy = { reprPrec := Semantics.Dynamic.PIP.Phenomena.instReprAnaphoraStrategy.repr }

def Semantics.Dynamic.PIP.Phenomena.instReprAnaphoraStrategy.repr : AnaphoraStrategy → ℕ → Std.Format

Equations

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

def Semantics.Dynamic.PIP.Phenomena.pipStrategy : AnaphoraStrategy

PIP uses description-based anaphora.

Equations

• Semantics.Dynamic.PIP.Phenomena.pipStrategy = Semantics.Dynamic.PIP.Phenomena.AnaphoraStrategy.descriptionBased

structure Semantics.Dynamic.PIP.Phenomena.PhenomenonCoverage : Type

Phenomena coverage by strategy.

• strategy : AnaphoraStrategy
• simpleAnaphora : Bool
• donkeyAnaphora : Bool
• modalSubordination : Bool
• bathroomSentences : Bool
• paycheckPronouns : Bool
• summationPronouns : Bool

instance Semantics.Dynamic.PIP.Phenomena.instReprPhenomenonCoverage : Repr PhenomenonCoverage

Equations

• Semantics.Dynamic.PIP.Phenomena.instReprPhenomenonCoverage = { reprPrec := Semantics.Dynamic.PIP.Phenomena.instReprPhenomenonCoverage.repr }

def Semantics.Dynamic.PIP.Phenomena.instReprPhenomenonCoverage.repr : PhenomenonCoverage → ℕ → Std.Format

Equations

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

def Semantics.Dynamic.PIP.Phenomena.valueCoverage : PhenomenonCoverage

Equations

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

def Semantics.Dynamic.PIP.Phenomena.fileChangeCoverage : PhenomenonCoverage

Equations

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

def Semantics.Dynamic.PIP.Phenomena.pipCoverage : PhenomenonCoverage

Equations

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

theorem Semantics.Dynamic.PIP.Phenomena.pip_covers_all : pipCoverage.simpleAnaphora = true ∧ pipCoverage.donkeyAnaphora = true ∧ pipCoverage.modalSubordination = true ∧ pipCoverage.bathroomSentences = true ∧ pipCoverage.paycheckPronouns = true ∧ pipCoverage.summationPronouns = true

PIP covers all phenomena.

theorem Semantics.Dynamic.PIP.Phenomena.value_based_gaps : valueCoverage.modalSubordination = false ∧ valueCoverage.bathroomSentences = false ∧ valueCoverage.paycheckPronouns = false

Value-based fails on modal/negation/paycheck cases.