PIP Connectives and Modal Operators

@cite{keshet-abney-2024} @cite{frank-1997} @cite{kratzer-1991} @cite{veltman-1996}Dynamic encoding of PIP connectives:

• Conjunction, negation, disjunction (with label floating)
• Labeled existential quantification
• Modal operators (must, might, would) as world quantifiers
• External vs. local variable binding

Label Floating

In PIP, formula labels (X ≡ φ) are tautological and float freely to the top of any discourse. Our dynamic encoding simulates this by threading labels through all operators monotonically: labels from earlier operators are always available to later ones.

Modals as World Quantifiers

PIP's modals are generalized quantifiers over worlds (paper Section 2.5):

• MIGHT^β_w(W₁, W₂) ≜ SOME(β_w ∩ W₁, W₂)
• MUST^β_w(W₁, W₂) ≜ EVERY(β_w ∩ W₁, W₂)

Our encoding parameterizes by an accessibility relation (equivalent to a Kratzer modal base β) and quantifies over accessible worlds.

def Semantics.Dynamic.PIP.atom {W : Type u_1} {E : Type u_2} (pred : Core.ICDRTAssignment W E → W → Bool) : PUpdate W E

Atomic predicate: filters the info state to pairs satisfying the predicate. Labels are preserved.

Equations

• Semantics.Dynamic.PIP.atom pred d = d.mapInfo fun (c : Semantics.Dynamic.IntensionalCDRT.IContext W E) => {gw : Semantics.Dynamic.Core.ICDRTAssignment W E × W | gw ∈ c ∧ pred gw.1 gw.2 = true}

def Semantics.Dynamic.PIP.negation {W : Type u_1} {E : Type u_2} (φ : PUpdate W E) : PUpdate W E

Negation: complement of info state relative to input. Labels are preserved — this is the key property enabling cross-negation anaphora (bathroom sentences).

Equations

• Semantics.Dynamic.PIP.negation φ d = { info := {gw : Semantics.Dynamic.Core.ICDRTAssignment W E × W | gw ∈ d.info ∧ gw ∉ (φ d).info}, labels := (φ d).labels }

def Semantics.Dynamic.PIP.conj {W : Type u_1} {E : Type u_2} (φ ψ : PUpdate W E) : PUpdate W E

Conjunction: sequential update. Labels accumulate across both conjuncts.

Equations

• Semantics.Dynamic.PIP.conj φ ψ d = ψ (φ d)

def Semantics.Dynamic.PIP.disj {W : Type u_1} {E : Type u_2} (φ ψ : PUpdate W E) : PUpdate W E

Disjunction: union of positive updates with label floating.

Labels from the first disjunct are available to the second, simulating PIP's label floating (X ≡ φ is tautological and floats freely). Both disjuncts evaluate from the same input info state, but the second disjunct inherits labels from the first.

This is the key operator for bathroom sentences: "Either there's no bathroom, or it's upstairs." The label for "bathroom" is registered in the first disjunct (under negation) and floated to the second for DEF_α resolution.

Note: both disjuncts evaluate from the same input info state d.info. This is what distinguishes disjunction from conjunction (sequential update) and correctly predicts that "There's no bathroom. It's upstairs." fails (conjunction) while "Either...or..." succeeds (disjunction).

Equations

• Semantics.Dynamic.PIP.disj φ ψ d = { info := (φ d).info ∪ (ψ { info := d.info, labels := (φ d).labels }).info, labels := (ψ { info := d.info, labels := (φ d).labels }).labels }

def Semantics.Dynamic.PIP.existsLabeled {W : Type u_1} {E : Type u_2} (α : FLabel) (v : Core.IVar) (domain : Set E) (bodyPred : Core.ICDRTAssignment W E → W → Bool) (body : PUpdate W E) : PUpdate W E

Labeled existential: ∃^α x. φ

The core mechanism for description-based anaphora:

1. For each (g, w) in the input, and each entity e in the domain, add (g[x ↦ e], w) to the extended context
2. Register label α with the description ⟨x, bodyPred⟩
3. Evaluate the body φ in the extended context

The label α persists in the discourse state, surviving subsequent negation and modal operators. This is what enables:

• Modal subordination: "A wolf might come. It would eat you."
• Bathroom sentences: "Either there's no bathroom, or it's upstairs."
• Paycheck pronouns: "John spent his paycheck. Bill saved it."

Equations

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

def Semantics.Dynamic.PIP.exists_ {W : Type u_1} {E : Type u_2} (v : Core.IVar) (domain : Set E) (body : PUpdate W E) : PUpdate W E

Unlabeled existential: standard ∃x. φ without descriptive tracking.

Equations

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

def Semantics.Dynamic.PIP.forall_ {W : Type u_1} {E : Type u_2} (v : Core.IVar) (domain : Set E) (body : PUpdate W E) : PUpdate W E

Universal quantification: ∀x. φ ≡ ¬∃x.¬φ

Equations

• Semantics.Dynamic.PIP.forall_ v domain body = Semantics.Dynamic.PIP.negation (Semantics.Dynamic.PIP.exists_ v domain (Semantics.Dynamic.PIP.negation body))

@[reducible, inline]

abbrev Semantics.Dynamic.PIP.PAccessRel (W : Type u_3) : Type u_3

PIP accessibility relation: decidable relation between worlds.

Equations

• Semantics.Dynamic.PIP.PAccessRel W = (W → W → Bool)

def Semantics.Dynamic.PIP.modalExpand {W : Type u_1} {E : Type u_2} (c : IntensionalCDRT.IContext W E) (access : PAccessRel W) : IntensionalCDRT.IContext W E

Modal context expansion: adds accessible-world pairs to the context.

Before evaluating the body of a modal, the context must include assignment-world pairs at accessible worlds. This mirrors the standard dynamic semantics treatment where modals shift the evaluation world: predicates inside the modal body are evaluated at accessible worlds, not just the evaluation world.

Without expansion, a context filtered to a single evaluation world would produce no accessible-world pairs for universal modals to check, making must/would vacuously satisfied and losing the modal subordination mechanism.

Equations

• Semantics.Dynamic.PIP.modalExpand c access = c ∪ {gw : Semantics.Dynamic.Core.ICDRTAssignment W E × W | ∃ (w₀ : W), (gw.1, w₀) ∈ c ∧ access w₀ gw.2 = true}

theorem Semantics.Dynamic.PIP.modalExpand_superset {W : Type u_1} {E : Type u_2} (c : IntensionalCDRT.IContext W E) (access : PAccessRel W) : c ⊆ modalExpand c access

Modal expansion includes all original pairs.

theorem Semantics.Dynamic.PIP.modalExpand_adds_accessible {W : Type u_1} {E : Type u_2} (c : IntensionalCDRT.IContext W E) (access : PAccessRel W) (g : Core.ICDRTAssignment W E) (w₀ w₁ : W) (hc : (g, w₀) ∈ c) (hacc : access w₀ w₁ = true) : (g, w₁) ∈ modalExpand c access

Modal expansion adds accessible-world pairs.

def Semantics.Dynamic.PIP.must {W : Type u_1} {E : Type u_2} (access : PAccessRel W) (allWorlds : List W) (body : PUpdate W E) : PUpdate W E

Modal necessity (must): universal quantification over accessible worlds.

must_R(φ) holds at (g, w₀) iff for all w₁ accessible from w₀, (g, w₁) survives φ.

The body is evaluated on an expanded context (via modalExpand) that includes pairs at all accessible worlds, mirroring PIP's world-subscripted predicates P_{w₁}.

The world variable is external: quantified by the modal from outside the scope of any indefinites in φ. The individual variables introduced by existentials inside φ are local.

This external/local distinction is what makes PIP's treatment of modal subordination work: "A wolf might come in" introduces the wolf (local) under the modal's world quantification (external). The wolf's descriptive content (via the label) is accessible in subsequent discourse.

Equations

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

def Semantics.Dynamic.PIP.might {W : Type u_1} {E : Type u_2} (access : PAccessRel W) (allWorlds : List W) (body : PUpdate W E) : PUpdate W E

Modal possibility (might): existential quantification over accessible worlds.

might_R(φ) holds at (g, w₀) iff there exists w₁ accessible from w₀ such that (g, w₁) survives φ.

Like must, the body is evaluated on an expanded context (via modalExpand) and the world variable is external.

Equations

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

def Semantics.Dynamic.PIP.would {W : Type u_1} {E : Type u_2} (access : PAccessRel W) (allWorlds : List W) (body : PUpdate W E) : PUpdate W E

Modal subordination operator (would): universal quantification over the same accessibility relation as the prior modal.

In the paper (example 49, p. 9:23), "It would eat you first" is analyzed as MUST^{a₀}{w*}([w₁]; DEF_X{x}; EAT{w₁}{x, you}), where a₀ is the same accessibility relation from "might" in the preceding sentence. So would = must with the inherited modal base.

Equations

• Semantics.Dynamic.PIP.would access allWorlds body = Semantics.Dynamic.PIP.must access allWorlds body

theorem Semantics.Dynamic.PIP.labels_survive_negation {W : Type u_1} {E : Type u_2} (d : Discourse W E) (α : FLabel) (φ : PUpdate W E) (desc : Description W E) (h : (φ d).labels.lookup α = some desc) : (negation φ d).labels.lookup α = some desc

Labels survive negation.

This is the fundamental property enabling cross-negation anaphora (bathroom sentences). Negation affects the info state but the label registry from the body is preserved.

theorem Semantics.Dynamic.PIP.labels_survive_conj_left {W : Type u_1} {E : Type u_2} (d : Discourse W E) (α : FLabel) (φ ψ : PUpdate W E) (desc : Description W E) (_h : (φ d).labels.lookup α = some desc) (h_pres : (ψ (φ d)).labels.lookup α = some desc) : (conj φ ψ d).labels.lookup α = some desc

Labels survive conjunction (left-to-right).

Labels registered by the first conjunct are available to the second.

theorem Semantics.Dynamic.PIP.labels_survive_must {W : Type u_1} {E : Type u_2} (d : Discourse W E) (α : FLabel) (access : PAccessRel W) (allWorlds : List W) (body : PUpdate W E) (desc : Description W E) (h : (body { info := modalExpand d.info access, labels := d.labels }).labels.lookup α = some desc) : (must access allWorlds body d).labels.lookup α = some desc

Labels survive modal operators.

Labels registered inside a modal scope propagate to the outer discourse state. This is what enables modal subordination.

theorem Semantics.Dynamic.PIP.labels_survive_might {W : Type u_1} {E : Type u_2} (d : Discourse W E) (α : FLabel) (access : PAccessRel W) (allWorlds : List W) (body : PUpdate W E) (desc : Description W E) (h : (body { info := modalExpand d.info access, labels := d.labels }).labels.lookup α = some desc) : (might access allWorlds body d).labels.lookup α = some desc

theorem Semantics.Dynamic.PIP.labels_survive_disj {W : Type u_1} {E : Type u_2} (d : Discourse W E) (α : FLabel) (φ ψ : PUpdate W E) (desc : Description W E) (_h_left : (φ d).labels.lookup α = some desc) (h_pres : (ψ { info := d.info, labels := (φ d).labels }).labels.lookup α = some desc) : (disj φ ψ d).labels.lookup α = some desc

Labels from the first disjunct are available in the output.

In PIP, X ≡ φ is tautological and floats freely across all operators. Our encoding simulates this by flowing labels from the first disjunct through the second. If the second disjunct preserves labels (as all PIP operators do), the output contains all labels from both disjuncts.

def Semantics.Dynamic.PIP.modalBindings (worldVar individualVar : Core.IVar) (α : FLabel) : List BoundVar

Under a modal, the world variable is external and individual variables introduced by existentials are local.

might(∃^α x. wolf(x) ∧ come-in(x)) ↑ external world ↑ local x

This classification falls out from the scoping structure:

• The modal quantifies over worlds from outside
• The existential binds x from inside

Equations

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

def Semantics.Dynamic.PIP.quantifierBindings (boundVar restrictorVar : Core.IVar) : List BoundVar

Under a quantifier, both the bound variable and restrictor variable are local.

every(∃x. farmer(x))(∃y. donkey(y) ∧ owns(x,y) → beats(x,y)) ↑ local x ↑ local y

Equations

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