Plural Intensional Presuppositional Predicate Calculus (PIP)

@cite{keshet-abney-2024} @cite{brasoveanu-2010} @cite{stone-1997}Core types for @cite{keshet-abney-2024}'s PIP system, which extends first-order predicate calculus with set abstraction, plural assignments, formula labels, and world-subscripted predicates to handle intensional anaphora uniformly.

The Core Innovation

Pronouns carry descriptive content (the formula that introduced their antecedent), not stored entity values. This enables anaphora to entities introduced under modal operators, where no actual entity exists in the evaluation world.

Encoding Strategy

PIP is natively a static, truth-conditional system: formulas denote truth values relative to a model, plural assignment set G, and evaluation world w*. Our formalization encodes PIP as a dynamic update system over the generic intensional context type IContext W E (in Dynamic/Core/Intensional.lean), which is a legitimate approach: @cite{brasoveanu-2010} shows the equivalence between plural predicate calculi and dynamic plural logics. The key properties (label monotonicity, external/local variable distinction) are faithfully preserved.

PIP's Five Constructs (paper item 17)

1. Unselective closure with bracketed [x] (local) vs unbracketed x (external)
2. Summation Σxφ: set-forming over individuals
3. Formula labels X ≡ φ: tautological abbreviatory definitions
4. World subscripts P_w(x): predicates evaluated at specific worlds
5. Presuppositions φ|ψ: assert φ, presuppose ψ

Key Types

Type	Description
FLabel	Formula label index (paper's X in X ≡ φ)
Description W E	Descriptive content associated with a label
Discourse W E	Information state + label registry
PUpdate W E	Discourse-level update (dynamic encoding of PIP formulas)

@[reducible, inline]

abbrev Semantics.PIP.BAccessRel (W : Type u_1) : Type u_1

Local Bool-valued accessibility for PIP's computational modal evaluation. PIP's modal operators use Bool predicates throughout for List.all/List.any computation; this is not the parallel-universe pattern (we are not shadowing Prop infrastructure with Bool versions), it is a legitimate Bool-internal framework over which PIP's discourse-update operators compute. The Prop-valued Core.Logic.Intensional.AccessRel is the canonical type for Kripke-style modal logic; PIP needs the Bool variant for its List.all/List.any truth-value pipeline. Lifted to Prop via fun a b => R a b = true when bridging to boxR/diamondR.

Equations

• Semantics.PIP.BAccessRel W = (W → W → Bool)

structure Semantics.PIP.FLabel : Type

Formula label: an index for tracking descriptive content.

In PIP, X ≡ φ defines X as an abbreviation for formula φ. This definition is a tautology (always true) and can be "floated" to the top of any discourse. Our encoding models this as a registry entry that persists monotonically through all operators.

• idx : ℕ

def Semantics.PIP.instDecidableEqFLabel.decEq (x✝ x✝¹ : FLabel) : Decidable (x✝ = x✝¹)

Equations

• Semantics.PIP.instDecidableEqFLabel.decEq { idx := a } { idx := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.PIP.instDecidableEqFLabel : DecidableEq FLabel

Equations

• Semantics.PIP.instDecidableEqFLabel = Semantics.PIP.instDecidableEqFLabel.decEq

@[implicit_reducible]

instance Semantics.PIP.instReprFLabel : Repr FLabel

Equations

• Semantics.PIP.instReprFLabel = { reprPrec := Semantics.PIP.instReprFLabel.repr }

def Semantics.PIP.instReprFLabel.repr : FLabel → ℕ → Std.Format

Equations

• Semantics.PIP.instReprFLabel.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "idx" ++ Std.Format.text " := " ++ (Std.Format.nest 7 (repr x✝.idx)).group) " }"

@[implicit_reducible]

instance Semantics.PIP.instHashableFLabel : Hashable FLabel

Equations

• Semantics.PIP.instHashableFLabel = { hash := Semantics.PIP.instHashableFLabel.hash }

def Semantics.PIP.instHashableFLabel.hash : FLabel → UInt64

Equations

• Semantics.PIP.instHashableFLabel.hash { idx := a } = mixHash 0 (hash a)

structure Semantics.PIP.Description (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A description: the descriptive content associated with a formula label.

Records which variable is being described and the predicate that constrains it. When a pronoun carries label α, retrieval evaluates the description's predicate to find the intended referent.

• var : Dynamic.Core.IVar

  The variable being described

• predicate : Dynamic.Core.ICDRTAssignment W E → W → Bool

  The constraining predicate (per assignment and world)

def Semantics.PIP.LabelStore (W : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

A label store maps formula labels to their descriptive content.

Labels accumulate monotonically as discourse proceeds — they are never retracted by negation, modals, or other operators. This monotonicity is what enables cross-modal and cross-negation anaphora.

Equations

• Semantics.PIP.LabelStore W E = (Semantics.PIP.FLabel → Option (Semantics.PIP.Description W E))

def Semantics.PIP.LabelStore.empty {W : Type u_1} {E : Type u_2} : LabelStore W E

Empty label store: no labels registered.

Equations

• Semantics.PIP.LabelStore.empty x✝ = none

def Semantics.PIP.LabelStore.register {W : Type u_1} {E : Type u_2} (s : LabelStore W E) (α : FLabel) (d : Description W E) : LabelStore W E

Register a label with its description.

Equations

• s.register α d β = if β = α then some d else s β

def Semantics.PIP.LabelStore.lookup {W : Type u_1} {E : Type u_2} (s : LabelStore W E) (α : FLabel) : Option (Description W E)

Look up a label.

Equations

• s.lookup α = s α

def Semantics.PIP.LabelStore.registered {W : Type u_1} {E : Type u_2} (s : LabelStore W E) (α : FLabel) : Bool

A label is registered iff its lookup is not none.

Equations

• s.registered α = (s α).isSome

theorem Semantics.PIP.LabelStore.register_preserves {W : Type u_1} {E : Type u_2} (s : LabelStore W E) (α β : FLabel) (d : Description W E) (hne : β ≠ α) : s.register α d β = s β

Registration is monotonic: registering a new label preserves old ones.

structure Semantics.PIP.Discourse (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A PIP discourse state: information state + label registry.

The discourse state separates two orthogonal concerns:

1. Info: the set of live assignment-world pairs (epistemic state)
2. Labels: the accumulated descriptive content registry

This separation is key: negation and modals affect info but not labels, which is why labels survive these operators and enable cross-boundary anaphora.

• info : Dynamic.Core.IContext W E

  The information state (set of assignment-world pairs)

• labels : LabelStore W E

  The label registry (monotonically accumulated)

def Semantics.PIP.Discourse.initial {W : Type u_1} {E : Type u_2} : Discourse W E

Initial discourse: all possibilities, no labels.

Equations

• Semantics.PIP.Discourse.initial = { info := Semantics.Dynamic.Core.IContext.univ, labels := Semantics.PIP.LabelStore.empty }

def Semantics.PIP.Discourse.empty {W : Type u_1} {E : Type u_2} : Discourse W E

Empty discourse: contradiction.

Equations

• Semantics.PIP.Discourse.empty = { info := ∅, labels := Semantics.PIP.LabelStore.empty }

def Semantics.PIP.Discourse.consistent {W : Type u_1} {E : Type u_2} (d : Discourse W E) : Prop

Is the discourse consistent (non-empty info state)?

Equations

• d.consistent = Set.Nonempty d.info

def Semantics.PIP.Discourse.mapInfo {W : Type u_1} {E : Type u_2} (d : Discourse W E) (f : Dynamic.Core.IContext W E → Dynamic.Core.IContext W E) : Discourse W E

Update only the info state, preserving labels.

Equations

• d.mapInfo f = { info := f d.info, labels := d.labels }

def Semantics.PIP.Discourse.addLabel {W : Type u_1} {E : Type u_2} (d : Discourse W E) (α : FLabel) (desc : Description W E) : Discourse W E

Register a new label, preserving info state.

Equations

• d.addLabel α desc = { info := d.info, labels := d.labels.register α desc }

def Semantics.PIP.PUpdate (W : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

A PIP update: discourse-to-discourse transformer.

In PIP's native formulation, formulas are truth-conditional (not updates). Our dynamic encoding represents PIP formulas as discourse transformers, following the @cite{brasoveanu-2010} equivalence. The key invariant: labels are monotonically accumulated (never retracted), mirroring PIP's property that formula-label definitions X ≡ φ are tautologies that float freely.

Equations

• Semantics.PIP.PUpdate W E = (Semantics.PIP.Discourse W E → Semantics.PIP.Discourse W E)

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

Presupposition operator ∂: a definedness condition.

⟦∂φ⟧ filters the information state to pairs where φ holds. If the result is empty, the utterance is undefined (presupposition failure).

In PIP, presuppositions are used for:

1. Definite descriptions (DEF_α presupposes α is registered)
2. Pronominal anaphora (presupposes antecedent is accessible)

Equations

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

def Semantics.PIP.retrieveDef {W : Type u_1} {E : Type u_2} (α : FLabel) : PUpdate W E

DEF_α: retrieve the entity satisfying the description labeled α.

Given label α and the current discourse state:

1. Look up α's description (variable v, predicate P)
2. Filter to assignments where g(v) is a real entity (not ⋆)
3. Filter to assignments where P(g, w) holds

The presupposition is that α is registered and yields a real entity. This is the mechanism by which pronouns get their reference: the pronoun carries label α, and DEF_α retrieves "the x such that P(x)" from the label store.

Equations

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

def Semantics.PIP.pluralTruth {W : Type u_1} {E : Type u_2} (c : Dynamic.Core.IContext W E) (w : W) (pred : Dynamic.Core.ICDRTAssignment W E → W → Bool) : Prop

PIP truth relative to a world and a plural context.

A predicate P holds at world w in context c iff P(g, w) = true for ALL assignments g paired with w in c.

This "plural" evaluation is what gives PIP its power: different assignments may bind different entities to the same variable, and truth requires the predicate to hold across all of them.

Equations

• Semantics.PIP.pluralTruth c w pred = ∀ (g : Semantics.Dynamic.Core.ICDRTAssignment W E), (g, w) ∈ c → pred g w = true

inductive Semantics.PIP.BindingMode : Type

Variable binding mode: how a variable was introduced.

• Local: Bound by a quantifier in the same clause. Both the individual variable and its restrictor are in scope.
• External: Bound from an enclosing scope. In modal contexts, the world variable is external (introduced by the modal operator).

This distinction falls out naturally from PIP's semantics without stipulation: under quantifiers, the bound variable is local; under modals, the world variable is external because it's quantified by the modal from outside the scope of any indefinites.

• local : BindingMode
• external : BindingMode

@[implicit_reducible]

instance Semantics.PIP.instDecidableEqBindingMode : DecidableEq BindingMode

Equations

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

def Semantics.PIP.instReprBindingMode.repr : BindingMode → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.PIP.instReprBindingMode : Repr BindingMode

Equations

• Semantics.PIP.instReprBindingMode = { reprPrec := Semantics.PIP.instReprBindingMode.repr }

structure Semantics.PIP.BoundVar : Type

A bound variable record: tracks how a variable was introduced.

• var : Dynamic.Core.IVar

  The variable index

• mode : BindingMode

  How it was bound

• label : Option FLabel

  The label of the introducing formula (if labeled)

def Semantics.PIP.instReprBoundVar.repr : BoundVar → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.PIP.instReprBoundVar : Repr BoundVar

Equations

• Semantics.PIP.instReprBoundVar = { reprPrec := Semantics.PIP.instReprBoundVar.repr }

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

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

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

This is a core PIP operation (paper items 25–27), not study-specific. GQ arguments in PIP take two summation terms: restrictor and scope.

Equations

• Semantics.PIP.summationFiltered c v φ = {e : Semantics.Dynamic.Core.Entity E | ∃ (g : Semantics.Dynamic.Core.ICDRTAssignment W E) (w : W), (g, w) ∈ c ∧ φ g w = true ∧ (g⟦v⟧ᵢ) w = e}

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

Summation without filtering: collects all values of variable v.

Equations

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

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

Unfiltered summation equals trivially filtered summation.

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

Any assignment in a non-empty context contributes to summation.