PIP Compositional Operations

[AK25a]

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 ([KA24]), 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 KeshetAbney2024.PIP.sigmaEval {W : Type u_1} {D : Type u_2} (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

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

@[simp]

theorem KeshetAbney2024.PIP.sigmaEval_mem {W : Type u_1} {D : Type u_2} (body : D → PIPExprF W D) (w : W) (d : D) : d ∈ sigmaEval body w ↔ (body d).truth w

theorem KeshetAbney2024.PIP.exists_iff_sigma_nonempty {W : Type u_1} {D : Type u_2} (body : D → PIPExprF W D) (w : W) : (PIPExprF.exists_ body).truth w ↔ (sigmaEval body w).Nonempty

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

theorem KeshetAbney2024.PIP.forall_iff_sigma_univ {W : Type u_1} {D : Type u_2} (body : D → PIPExprF W D) (w : W) : (PIPExprF.forall_ body).truth w ↔ sigmaEval body w = Set.univ

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

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

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

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

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

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

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

theorem KeshetAbney2024.PIP.sigmaEval_true {W : Type u_1} {D : Type u_2} (w : W) : sigmaEval (fun (x : D) => PIPExprF.pred fun (x : W) => True) w = Set.univ

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

theorem KeshetAbney2024.PIP.sigmaEval_false {W : Type u_1} {D : Type u_2} (w : W) : sigmaEval (fun (x : D) => PIPExprF.pred fun (x : W) => False) w = ∅

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

theorem KeshetAbney2024.PIP.sigmaEval_labelDef {W : Type u_1} {D : Type u_2} (α : 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 KeshetAbney2024.PIP.sigmaEval_presup {W : Type u_1} {D : Type u_2} (φ : D → PIPExprF W D) (ψ : W → Prop) (w : W) : sigmaEval (fun (d : D) => (φ d).presup ψ) w = sigmaEval φ w

Presuppositions are truth-transparent for sigma.

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

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

Equations

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

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

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

Equations

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

theorem KeshetAbney2024.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 KeshetAbney2024.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 KeshetAbney2024.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 KeshetAbney2024.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 KeshetAbney2024.PIP.gq_duality {α : Type u_1} (R S : Set α) : ¬setEvery R S ↔ setSome R Sᶜ

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

theorem KeshetAbney2024.PIP.setEvery_sigma {W : Type u_2} {D : Type u_3} (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 → (body_S d).truth w

EVERY over sigma sets ↔ pointwise universal implication.

theorem KeshetAbney2024.PIP.setSome_sigma {W : Type u_2} {D : Type u_3} (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 ∧ (body_S d).truth w

SOME over sigma sets ↔ pointwise existential conjunction.

def KeshetAbney2024.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 AccessRel W from Intensional. PIP.Connectives.must provides the dynamic implementation; must_truth_iff_mustBase below bridges the static PIPExprF.must to this set-based formulation. Cf. Semantics.Modality.Kratzer.simpleNecessity for the Kratzerian analogue (monomorphic over World).

Equations

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

def KeshetAbney2024.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

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

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

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

theorem KeshetAbney2024.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 KeshetAbney2024.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 KeshetAbney2024.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 KeshetAbney2024.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 KeshetAbney2024.PIP.accessRelToBase {W : Type u_1} (R : Core.Logic.Modal.AccessRel W) (w : W) : Set W

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

Equations

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

theorem KeshetAbney2024.PIP.must_truth_iff_mustBase {W : Type u_1} {D : Type u_2} (R : Core.Logic.Modal.AccessRel W) (φ : PIPExprF W D) (w : W) : (PIPExprF.must R φ).truth w ↔ mustBase (accessRelToBase R w) Set.univ {w' : W | φ.truth w'}

PIPExprF.must R φ truth agrees with three-argument mustBase. Direct, since must truth is box and mustBase is set inclusion.

theorem KeshetAbney2024.PIP.might_truth_iff_mightBase {W : Type u_1} {D : Type u_2} (R : Core.Logic.Modal.AccessRel W) (φ : PIPExprF W D) (w : W) : (PIPExprF.might R φ).truth w ↔ mightBase (accessRelToBase R w) Set.univ {w' : W | φ.truth w'}

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

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

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 → Prop (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. ArgumentStructure.ThematicRel for the general Davidsonian role type Entity → Event → Prop; FX is PIP's mechanism for composing such roles with restricted variables.

Equations

• KeshetAbney2024.PIP.fxApply f φ x w = (f x w ∧ φ w)

theorem KeshetAbney2024.PIP.fxApply_entails_role {W : Type u_1} {D : Type u_2} (f : D → W → Prop) (φ : W → Prop) (x : D) (w : W) (h : fxApply f φ x w) : f x w

FX entails the role predicate.

theorem KeshetAbney2024.PIP.fxApply_entails_body {W : Type u_1} {D : Type u_2} (f : D → W → Prop) (φ : W → Prop) (x : D) (w : W) (h : fxApply f φ x w) : φ w

FX entails the formula body.

theorem KeshetAbney2024.PIP.fxApply_twice {W : Type u_1} {D : Type u_2} (f g : D → W → Prop) (φ : W → Prop) (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 KeshetAbney2024.PIP.fxApply_true {W : Type u_1} {D : Type u_2} (f : D → W → Prop) (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 KeshetAbney2024.PIP.sigma_monotone {W : Type u_1} {D : Type u_2} (φ ψ : D → PIPExprF W D) (w : W) (h : ∀ (d : D), (ψ d).truth w → (φ d).truth w) : sigmaEval ψ w ⊆ sigmaEval φ w

Sigma is monotone: stronger body conditions produce smaller sets.

theorem KeshetAbney2024.PIP.sigma_subordination {W : Type u_1} {D : Type u_2} (φ ψ : 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 KeshetAbney2024.PIP.sigmaEval_labelDef_subordination {W : Type u_1} {D : Type u_2} (α : 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.