PIP Compositional Operations

@cite{abney-keshet-2025}

Compositional building blocks for PIP beyond the core formula language PIPExprF. Where PIPExprF gives truth and felicity for formulas (type t), this file defines operations whose output is a set of individuals (type e): sigma evaluation (Σxφ), set-based generalized quantifiers (EVERY/SOME), three-argument modals with explicit modal bases, the FX type-lifting operation for restricted variables, and the simple/summation pronoun distinction.

These operations correspond to the Glossa paper's enrichment of the S&P formulation (@cite{keshet-abney-2024}), making PIP's set-based compositional interface explicit.

Key Design Decision

Sigma evaluation produces a Set D, not a PIPExprF W D. This is because Σxφ denotes the set of satisfiers of φ (a semantic object of type e), not a truth value (type t). It is therefore defined externally from the PIPExprF inductive type and connected to it via bridge theorems.

def Semantics.PIP.sigmaEval {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (body : D → PIPExprF W D) (w : W) : Set D

Sigma evaluation: Σxφ = {d ∈ D | ⟦φ(d)⟧^w = 1}.

Collects all individuals satisfying a formula body at a given world. The output is a Set D (type e), not a formula (type t). This is the fundamental bridge between PIP's formula language and its set-based compositional interface.

This is the static analogue of PIP.Basic.summationFiltered, which performs the same collection on the dynamic IContext level. Agreement between the two is part of the static↔dynamic correspondence.

Equations

• Semantics.PIP.sigmaEval body w = {d : D | (body d).truth w = true}

@[simp]

theorem Semantics.PIP.sigmaEval_mem {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (body : D → PIPExprF W D) (w : W) (d : D) : d ∈ sigmaEval body w ↔ (body d).truth w = true

theorem Semantics.PIP.exists_iff_sigma_nonempty {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (body : D → PIPExprF W D) (w : W) : (PIPExprF.exists_ body).truth w = true ↔ (sigmaEval body w).Nonempty

∃xφ is true iff the sigma set is nonempty.

theorem Semantics.PIP.forall_iff_sigma_univ {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (body : D → PIPExprF W D) (w : W) : (PIPExprF.forall_ body).truth w = true ↔ sigmaEval body w = Set.univ

∀xφ is true iff every individual is in the sigma set.

theorem Semantics.PIP.sigmaEval_conj {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (φ ψ : D → PIPExprF W D) (w : W) : sigmaEval (fun (d : D) => (φ d).conj (ψ d)) w = sigmaEval φ w ∩ sigmaEval ψ w

Σx(φ ∧ ψ) = Σxφ ∩ Σxψ.

theorem Semantics.PIP.sigmaEval_disj {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (φ ψ : D → PIPExprF W D) (w : W) : sigmaEval (fun (d : D) => (φ d).disj (ψ d)) w = sigmaEval φ w ∪ sigmaEval ψ w

Σx(φ ∨ ψ) = Σxφ ∪ Σxψ.

theorem Semantics.PIP.sigmaEval_neg {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (φ : D → PIPExprF W D) (w : W) : sigmaEval (fun (d : D) => (φ d).neg) w = (sigmaEval φ w)ᶜ

Σx(¬φ) = (Σxφ)ᶜ.

theorem Semantics.PIP.sigmaEval_true {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (w : W) : sigmaEval (fun (x : D) => PIPExprF.pred fun (x : W) => true) w = Set.univ

Σx(⊤) = D (everything satisfies a tautology).

theorem Semantics.PIP.sigmaEval_false {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (w : W) : sigmaEval (fun (x : D) => PIPExprF.pred fun (x : W) => false) w = ∅

Σx(⊥) = ∅ (nothing satisfies a contradiction).

theorem Semantics.PIP.sigmaEval_labelDef {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (α : FLabel) (φ : D → PIPExprF W D) (w : W) : sigmaEval (fun (d : D) => PIPExprF.labelDef α (φ d)) w = sigmaEval φ w

Label definitions are truth-transparent for sigma.

theorem Semantics.PIP.sigmaEval_presup {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (φ : D → PIPExprF W D) (ψ : W → Bool) (w : W) : sigmaEval (fun (d : D) => (φ d).presup ψ) w = sigmaEval φ w

Presuppositions are truth-transparent for sigma.

def Semantics.PIP.setEvery {α : Type u_1} (R S : Set α) : Prop

EVERY(R, S) = R ⊆ S. Universal quantification as set inclusion.

Equations

• Semantics.PIP.setEvery R S = (R ⊆ S)

def Semantics.PIP.setSome {α : Type u_1} (R S : Set α) : Prop

SOME(R, S) = (R ∩ S).Nonempty. Existential quantification as intersection.

Equations

• Semantics.PIP.setSome R S = (R ∩ S).Nonempty

theorem Semantics.PIP.setEvery_antimono_left {α : Type u_1} {R₁ R₂ S : Set α} (h : R₁ ⊆ R₂) (hE : setEvery R₂ S) : setEvery R₁ S

EVERY is downward monotone in its first argument.

theorem Semantics.PIP.setEvery_mono_right {α : Type u_1} {R S₁ S₂ : Set α} (h : S₁ ⊆ S₂) (hE : setEvery R S₁) : setEvery R S₂

EVERY is upward monotone in its second argument.

theorem Semantics.PIP.setSome_mono_left {α : Type u_1} {R₁ R₂ S : Set α} (h : R₁ ⊆ R₂) (hS : setSome R₁ S) : setSome R₂ S

SOME is upward monotone in its first argument.

theorem Semantics.PIP.setSome_mono_right {α : Type u_1} {R S₁ S₂ : Set α} (h : S₁ ⊆ S₂) (hS : setSome R S₁) : setSome R S₂

SOME is upward monotone in its second argument.

theorem Semantics.PIP.gq_duality {α : Type u_1} (R S : Set α) : ¬setEvery R S ↔ setSome R Sᶜ

GQ duality: ¬EVERY(R, S) ↔ SOME(R, Sᶜ).

theorem Semantics.PIP.setEvery_sigma {W : Type u_2} {D : Type u_3} [FiniteDomain D] [Fintype W] (body_R body_S : D → PIPExprF W D) (w : W) : setEvery (sigmaEval body_R w) (sigmaEval body_S w) ↔ ∀ (d : D), (body_R d).truth w = true → (body_S d).truth w = true

EVERY over sigma sets ↔ pointwise universal implication.

theorem Semantics.PIP.setSome_sigma {W : Type u_2} {D : Type u_3} [FiniteDomain D] [Fintype W] (body_R body_S : D → PIPExprF W D) (w : W) : setSome (sigmaEval body_R w) (sigmaEval body_S w) ↔ ∃ (d : D), (body_R d).truth w = true ∧ (body_S d).truth w = true

SOME over sigma sets ↔ pointwise existential conjunction.

def Semantics.PIP.mustBase {W : Type u_1} (β W₁ W₂ : Set W) : Prop

MUST(β, W₁, W₂) = β ∩ W₁ ⊆ W₂.

Three-argument necessity: the modal base β restricted by W₁ is included in W₂. When W₁ = ⊤, reduces to β ⊆ W₂.

The modal base β corresponds to accessRelToBase R w for an BAccessRel W from Core.Logic.Intensional. PIP.Connectives.must provides the dynamic implementation; must_truth_iff_mustBase below bridges the static PIPExprF.must to this set-based formulation. Cf. Theories.Semantics.Modality.Kratzer.simpleNecessity for the Kratzerian analogue (monomorphic over World).

Equations

• Semantics.PIP.mustBase β W₁ W₂ = (β ∩ W₁ ⊆ W₂)

def Semantics.PIP.mightBase {W : Type u_1} (β W₁ W₂ : Set W) : Prop

MIGHT(β, W₁, W₂) = (β ∩ W₁ ∩ W₂).Nonempty.

Three-argument possibility: some world in the modal base satisfying W₁ also satisfies W₂.

Equations

• Semantics.PIP.mightBase β W₁ W₂ = (β ∩ W₁ ∩ W₂).Nonempty

theorem Semantics.PIP.mustBase_taut_restr {W : Type u_1} (β W₂ : Set W) : mustBase β Set.univ W₂ ↔ β ⊆ W₂

Tautological restriction: MUST(β, ⊤, W₂) ↔ β ⊆ W₂.

theorem Semantics.PIP.mustBase_eq_setEvery {W : Type u_1} (β W₁ W₂ : Set W) : mustBase β W₁ W₂ ↔ setEvery (β ∩ W₁) W₂

MUST as a set-based GQ: MUST(β, W₁, W₂) ↔ EVERY(β ∩ W₁, W₂).

theorem Semantics.PIP.mightBase_eq_setSome {W : Type u_1} (β W₁ W₂ : Set W) : mightBase β W₁ W₂ ↔ setSome (β ∩ W₁) W₂

MIGHT as a set-based GQ: MIGHT(β, W₁, W₂) ↔ SOME(β ∩ W₁, W₂).

theorem Semantics.PIP.mustBase_realistic {W : Type u_1} (β W₁ W₂ : Set W) (w : W) (hw_β : w ∈ β) (hw_W₁ : w ∈ W₁) (h : mustBase β W₁ W₂) : w ∈ W₂

If the actual world is in the modal base and restriction, MUST forces the consequent at the actual world.

theorem Semantics.PIP.modal_duality {W : Type u_1} (β W₁ W₂ : Set W) : ¬mustBase β W₁ W₂ ↔ mightBase β W₁ W₂ᶜ

Modal duality: ¬MUST(β, W₁, W₂) ↔ MIGHT(β, W₁, W₂ᶜ).

def Semantics.PIP.accessRelToBase {W : Type u_1} (R : BAccessRel W) (w : W) : Set W

Convert an accessibility relation to a modal base at world w.

Equations

• Semantics.PIP.accessRelToBase R w = {w' : W | R w w' = true}

theorem Semantics.PIP.must_truth_iff_mustBase {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (R : BAccessRel W) (φ : PIPExprF W D) (w : W) : (PIPExprF.must R φ).truth w = true ↔ mustBase (accessRelToBase R w) Set.univ {w' : W | φ.truth w' = true}

PIPExprF.must R φ truth agrees with three-argument mustBase.

theorem Semantics.PIP.might_truth_iff_mightBase {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (R : BAccessRel W) (φ : PIPExprF W D) (w : W) : (PIPExprF.might R φ).truth w = true ↔ mightBase (accessRelToBase R w) Set.univ {w' : W | φ.truth w' = true}

PIPExprF.might R φ truth agrees with three-argument mightBase.

def Semantics.PIP.fxApply {W : Type u_1} {D : Type u_2} (f : D → W → Bool) (φ : W → Bool) (x : D) : W → Bool

FX (↑f): lift a thematic-role predicate into a formula modifier.

↑f = λφλx. f(x) ∧ φ (base case, when f : ⟨e, t⟩)

Given a predicate f : D → W → Bool (e.g., AGENT, PATIENT), fxApply f φ x conjoins f(x) with formula φ, producing a restricted variable: x is constrained to satisfy both f and φ.

This implements the base case of the paper's recursive ↑-lifting. The recursive case (for multi-argument predicates like ⟨e, ⟨e, t⟩⟩) applies ↑ to each curried application. Iterated application via fxApply_twice captures the effect for two-argument roles.

Cf. Theories.Semantics.ArgumentStructure.ThematicRel for the general Davidsonian role type Entity → Event → Prop; FX is PIP's mechanism for composing such roles with restricted variables.

Equations

• Semantics.PIP.fxApply f φ x w = (f x w && φ w)

theorem Semantics.PIP.fxApply_entails_role {W : Type u_1} {D : Type u_2} (f : D → W → Bool) (φ : W → Bool) (x : D) (w : W) (h : fxApply f φ x w = true) : f x w = true

FX entails the role predicate.

theorem Semantics.PIP.fxApply_entails_body {W : Type u_1} {D : Type u_2} (f : D → W → Bool) (φ : W → Bool) (x : D) (w : W) (h : fxApply f φ x w = true) : φ w = true

FX entails the formula body.

theorem Semantics.PIP.fxApply_twice {W : Type u_1} {D : Type u_2} (f g : D → W → Bool) (φ : W → Bool) (x : D) (w : W) : fxApply g (fxApply f φ x) x w = (g x w && f x w && φ w)

Iterated FX accumulates assertions: ↑g(↑f(φ))(x) = g(x) ∧ f(x) ∧ φ.

theorem Semantics.PIP.fxApply_true {W : Type u_1} {D : Type u_2} (f : D → W → Bool) (x : D) (w : W) : fxApply f (fun (x : W) => true) x w = f x w

FX with tautological formula: ↑f(⊤)(x) = f(x).

Summation Pronouns

The paper distinguishes simple pronouns (type e: a single variable x with presupposition SG(x)) from summation pronouns (type e: ΣxX with presupposition PL(ΣxX)). The key insight: the semantic denotation of a summation pronoun IS sigmaEval — the exhaustive set of all satisfiers. The simple/summation distinction is structural (syntactic tree shape) and presuppositional (SG vs PL), not truth-conditional.

Concretely:

• Simple pronoun: she_x = x | FEM(x) ∧ SG(x)
• Summation pronoun: they^X_x = ΣxX | PL(ΣxX)

Both resolve to sigma sets for the pronoun's descriptive content. The presuppositional difference (SG for singularity, PL for plurality) is handled by PIP.Bridges.single and PIP.Bridges.plural.

No separate summPronounDenot definition is needed: summation pronoun denotation = sigmaEval by the paper's own analysis.

theorem Semantics.PIP.sigma_monotone {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (φ ψ : D → PIPExprF W D) (w : W) (h : ∀ (d : D), (ψ d).truth w = true → (φ d).truth w = true) : sigmaEval ψ w ⊆ sigmaEval φ w

Sigma is monotone: stronger body conditions produce smaller sets.

theorem Semantics.PIP.sigma_subordination {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (φ ψ : D → PIPExprF W D) (w : W) : sigmaEval (fun (d : D) => (φ d).conj (ψ d)) w ⊆ sigmaEval φ w

Quantificational subordination: if ψ extends φ with additional conditions, then Σx(φ ∧ ψ) ⊆ Σxφ. This is the set-theoretic foundation of cross-sentential anaphora through label-subordinated quantification.

When a subordinate quantifier's restriction φ ∧ ψ includes the main quantifier's restrictor φ via a label, the subordinate sigma set is a subset of the main one.

theorem Semantics.PIP.sigmaEval_labelDef_subordination {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (α : FLabel) (φ ψ : D → PIPExprF W D) (w : W) : sigmaEval (fun (d : D) => PIPExprF.labelDef α ((φ d).conj (ψ d))) w ⊆ sigmaEval φ w

Label definitions don't affect subordination relationships.