PIP Connectives and Modal Operators

@cite{keshet-abney-2024} @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 (Core.ModalLogic.AccessRel, equivalent to a Kratzer modal base β) and quantifies over accessible worlds. The grounding theorem must_truth_agrees_kripkeEval proves that PIP's must produces the same truth conditions as Core.ModalLogic.kripkeEval .necessity.

def Semantics.PIP.atom {W : Type u_1} {E : Type u_2} (pred : Dynamic.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.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.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.PIP.negation φ d = { info := {gw : Semantics.Dynamic.Core.ICDRTAssignment W E × W | gw ∈ d.info ∧ gw ∉ (φ d).info}, labels := (φ d).labels }

def Semantics.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.PIP.conj φ ψ d = ψ (φ d)

def Semantics.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.PIP.disj φ ψ d = { info := (φ d).info ∪ (ψ { info := d.info, labels := (φ d).labels }).info, labels := (ψ { info := d.info, labels := (φ d).labels }).labels }

def Semantics.PIP.existsLabeled {W : Type u_1} {E : Type u_2} (α : FLabel) (v : Dynamic.Core.IVar) (domain : Set E) (bodyPred : Dynamic.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.PIP.exists_ {W : Type u_1} {E : Type u_2} (v : Dynamic.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.PIP.forall_ {W : Type u_1} {E : Type u_2} (v : Dynamic.Core.IVar) (domain : Set E) (body : PUpdate W E) : PUpdate W E

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

Equations

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

def Semantics.PIP.modalExpand {W : Type u_1} {E : Type u_2} (c : Dynamic.IntensionalCDRT.IContext W E) (access : Core.ModalLogic.AccessRel W) : Dynamic.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.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.PIP.modalExpand_superset {W : Type u_1} {E : Type u_2} (c : Dynamic.IntensionalCDRT.IContext W E) (access : Core.ModalLogic.AccessRel W) : c ⊆ modalExpand c access

Modal expansion includes all original pairs.

theorem Semantics.PIP.modalExpand_adds_accessible {W : Type u_1} {E : Type u_2} (c : Dynamic.IntensionalCDRT.IContext W E) (access : Core.ModalLogic.AccessRel W) (g : Dynamic.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.PIP.must {W : Type u_1} {E : Type u_2} (access : Core.ModalLogic.AccessRel 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.PIP.might {W : Type u_1} {E : Type u_2} (access : Core.ModalLogic.AccessRel 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.PIP.would {W : Type u_1} {E : Type u_2} (access : Core.ModalLogic.AccessRel 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's modal subordination analysis, "It would eat you first" is analyzed as MUST with the same accessibility relation from "might" in the preceding sentence. So would = must with the inherited modal base.

Equations

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

theorem Semantics.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.PIP.labels_survive_must {W : Type u_1} {E : Type u_2} (d : Discourse W E) (α : FLabel) (access : Core.ModalLogic.AccessRel 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.PIP.labels_survive_might {W : Type u_1} {E : Type u_2} (d : Discourse W E) (α : FLabel) (access : Core.ModalLogic.AccessRel 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.PIP.must_truth_agrees_kripkeEval {W : Type u_1} {E : Type u_2} [Core.Proposition.FiniteWorlds W] (R : Core.ModalLogic.AccessRel W) (p : Dynamic.Core.ICDRTAssignment W E → W → Bool) (d : Discourse W E) (g : Dynamic.Core.ICDRTAssignment W E) (w₀ : W) (hd : (g, w₀) ∈ d.info) : (g, w₀) ∈ (must R Core.Proposition.FiniteWorlds.worlds (atom p) d).info ↔ Core.ModalLogic.kripkeEval R Core.Modality.ModalForce.necessity (p g) w₀ = true

PIP's must produces the same truth conditions as Core.ModalLogic.kripkeEval .necessity.

Specifically: a pair (g, w₀) survives must R allWorlds (atom p) iff kripkeEval R .necessity (p g) w₀ = true — the body predicate holds at all R-accessible worlds. This connects PIP's discourse-update modals to the standard Kripke semantics used throughout Theories/Semantics/Modality/.

theorem Semantics.PIP.might_truth_agrees_kripkeEval {W : Type u_1} {E : Type u_2} [Core.Proposition.FiniteWorlds W] (R : Core.ModalLogic.AccessRel W) (p : Dynamic.Core.ICDRTAssignment W E → W → Bool) (d : Discourse W E) (g : Dynamic.Core.ICDRTAssignment W E) (w₀ : W) (hd : (g, w₀) ∈ d.info) : (g, w₀) ∈ (might R Core.Proposition.FiniteWorlds.worlds (atom p) d).info ↔ Core.ModalLogic.kripkeEval R Core.Modality.ModalForce.possibility (p g) w₀ = true

PIP's might agrees with kripkeEval .possibility.

theorem Semantics.PIP.must_realistic_of_refl {W : Type u_1} {E : Type u_2} [Core.Proposition.FiniteWorlds W] (R : Core.ModalLogic.AccessRel W) (hRefl : Core.ModalLogic.Refl R) (p : Dynamic.Core.ICDRTAssignment W E → W → Bool) (d : Discourse W E) (g : Dynamic.Core.ICDRTAssignment W E) (w₀ : W) (hd : (g, w₀) ∈ d.info) (hmust : (g, w₀) ∈ (must R Core.Proposition.FiniteWorlds.worlds (atom p) d).info) : p g w₀ = true

Realistic modal base (T axiom) for PIP: if R is reflexive and must R (atom p) holds at (g, w₀), then p g w₀ = true.

This derives PIP's key insight — must allows anaphora because a realistic modal base guarantees the description holds at the evaluation world — from Core.ModalLogic.T_of_refl.

theorem Semantics.PIP.must_realistic_at {W : Type u_1} {E : Type u_2} [Core.Proposition.FiniteWorlds W] (R : Core.ModalLogic.AccessRel W) (p : Dynamic.Core.ICDRTAssignment W E → W → Bool) (d : Discourse W E) (g : Dynamic.Core.ICDRTAssignment W E) (w₀ : W) (hRefl_at : R w₀ w₀ = true) (hmust : (g, w₀) ∈ (must R Core.Proposition.FiniteWorlds.worlds (atom p) d).info) : p g w₀ = true

Pointwise realistic base: if R w₀ w₀ = true and must holds at w₀, the body predicate holds at w₀.

This is the version that applies to non-globally-reflexive relations (e.g., epistemic access from a specific evaluation world). It captures @cite{kratzer-1991}'s realistic modal base without requiring global reflexivity.

def Semantics.PIP.modalBindings (worldVar individualVar : Dynamic.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.PIP.quantifierBindings (boundVar restrictorVar : Dynamic.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.

PIP Generalized Quantifiers (paper items 28, 53–56)

The paper defines (item 28):

• EVERY(x, y) iff x ⊆ y
• MOST(x, y) iff |x ∩ y|/|x| > θ
• SOME(x, y) iff x ∩ y ≠ ∅

Summation Σxφ collects entity values from assignments satisfying φ. GQs take two summation terms as arguments: the restrictor and the nuclear scope.

def Semantics.PIP.gqEvery {α : Type u_3} (restriction scope : Set α) : Prop

EVERY(restriction, scope) iff restriction ⊆ scope (paper item 28)

Equations

• Semantics.PIP.gqEvery restriction scope = (restriction ⊆ scope)

def Semantics.PIP.gqSome {α : Type u_3} (restriction scope : Set α) : Prop

SOME(restriction, scope) iff restriction ∩ scope ≠ ∅

Equations

• Semantics.PIP.gqSome restriction scope = (restriction ∩ scope).Nonempty

theorem Semantics.PIP.forall_eq_neg_exists_neg {W : Type u_3} {E : Type u_4} (v : Dynamic.Core.IVar) (domain : Set E) (body : PUpdate W E) : forall_ v domain body = negation (exists_ v domain (negation body))

forall_ encodes EVERY via ¬∃x.¬ (paper item 56)

def Semantics.PIP.single {α : Type u_3} (s : Set α) : Prop

SINGLE(τ) ↔ |τ| = 1 (paper item 71)

The existential presupposition of singular pronouns: she_τ ↝ τ|SINGLE(τ). A singular pronoun presupposes that its denotation is a singleton.

Equations

• Semantics.PIP.single s = ∃ (a : α), s = {a}

def Semantics.PIP.plural {α : Type u_3} (s : Set α) : Prop

PLURAL(τ) ↔ |τ| > 1 (paper item 84)

The presupposition of plural pronouns: they_τ ↝ τ|PLURAL(τ).

Equations

• Semantics.PIP.plural s = ∃ (a : α) (b : α), a ≠ b ∧ a ∈ s ∧ b ∈ s

theorem Semantics.PIP.single_singleton {α : Type u_3} (a : α) : single {a}

A singleton set satisfies SINGLE.

theorem Semantics.PIP.single_not_plural {α : Type u_3} (s : Set α) (hs : single s) : ¬plural s

SINGLE and PLURAL are mutually exclusive.