PIP Integration Bridges

[KA24] [AK25a] [Kar73] [Kra91] [Lin83] [Bra10]

This file connects PIP to the rest of linglib, establishing correspondences between PIP's formulation and the standard treatments in:

1. Presupposition projection — PIP's F operator ↔ PartialProp.andFilter
2. Generalized quantifiers — PIP's EVERY/SOME ↔ GQ
3. Plural semantics — PIP's SINGLE/PLURAL ↔ Link's Atom/properPlural
4. Modal logic — PIP's must/might ↔ Intensional.box/diamond
5. Static↔dynamic agreement — PIPExprF.truth ↔ PUpdate filtering

The set-based GQ operations (setEvery/setSome), three-argument modals (mustBase/mightBase), and sigma evaluation (sigmaEval) from the Glossa companion paper ([AK25a]) are in PIP.Composition.

Design

Each section is self-contained: it imports what it needs and states the correspondence as a theorem or definition. The presupposition, modal, and static↔dynamic bridges are all proved (atomic and negation cases for the last); the full Brasoveanu model-equivalence — a bijection between PIP models and ICDRT information states — is a non-trivial model-theoretic argument left as future work, not formalized here.

Presupposition Projection: F ↔ PartialProp connectives

PIP's F operator and Semantics.Presupposition.PartialProp filtering connectives implement the same Karttunen conjunction clause ([Kar73]). These theorems were previously in the study file; they belong in the theory layer because they establish a general correspondence.

theorem KeshetAbney2024.PIP.Bridges.pip_felicity_agrees_with_andFilter {W : Type u_1} (φ ψ : Felicity.PIPExpr W) (w : W) : (φ.conj ψ).felicitous w ↔ ({ presup := fun (w : W) => φ.felicitous w, assertion := fun (w : W) => φ.truth w }.andFilter { presup := fun (w : W) => ψ.felicitous w, assertion := fun (w : W) => ψ.truth w }).presup w

PIP's conjunction felicity agrees with PartialProp.andFilter.

PIP Felicity (PIPExpr.felicitous for .conj φ ψ): φ.felicitous w && ((φ.truth w).not || ψ.felicitous w)

PartialProp.andFilter (Semantics.Presupposition): p.presup w && (!p.assertion w || q.presup w)

These are structurally identical when interpreting truth as assertion and felicitous as presup.

theorem KeshetAbney2024.PIP.Bridges.pip_felicity_agrees_with_neg {W : Type u_1} (φ : Felicity.PIPExpr W) (w : W) : φ.neg.felicitous w ↔ { presup := fun (w : W) => φ.felicitous w, assertion := fun (w : W) => φ.truth w }.neg.presup w

PIP's negation felicity agrees with PartialProp.neg: both preserve the presupposition/felicity of the negated expression unchanged.

theorem KeshetAbney2024.PIP.Bridges.pip_felicity_agrees_with_impFilter {W : Type u_1} (φ ψ : Felicity.PIPExpr W) (w : W) : (φ.impl ψ).felicitous w ↔ ({ presup := fun (w : W) => φ.felicitous w, assertion := fun (w : W) => φ.truth w }.impFilter { presup := fun (w : W) => ψ.felicitous w, assertion := fun (w : W) => ψ.truth w }).presup w

PIP's implication felicity agrees with PartialProp.impFilter.

F(φ → ψ) = Fφ ∧ (φ → Fψ)

This is exactly the filtering implication from [Kar73]: the antecedent can satisfy the consequent's presupposition.

theorem KeshetAbney2024.PIP.Bridges.pip_felicity_agrees_with_orFilter {W : Type u_1} (φ ψ : Felicity.PIPExpr W) (w : W) : (φ.disj ψ).felicitous w ↔ ({ presup := fun (w : W) => φ.felicitous w, assertion := fun (w : W) => φ.truth w }.orFilter { presup := fun (w : W) => ψ.felicitous w, assertion := fun (w : W) => ψ.truth w }).presup w

PIP's disjunction felicity agrees with the filtering disjunction: F(φ ∨ ψ) = Fφ ∧ (¬φ → Fψ)

GQ Bridge: PIP's set-based quantifiers ↔ GQ

PIP defines (paper item 28):

• EVERY(R, S) iff R ⊆ S
• SOME(R, S) iff R ∩ S ≠ ∅

These are exactly the standard GQ denotations when restrictor and scope are sets (extensional GQs). The GQ type (α → Prop) → (α → Prop) → Prop is the predicate-based version.

theorem KeshetAbney2024.PIP.Bridges.setEvery_eq_every_sem {α : Type u_1} (R S : Set α) : setEvery R S ↔ Quantification.every_sem R S

setEvery (from PIP.Composition, = set inclusion R ⊆ S) agrees with Quantification.every_sem (= ∀ x, R x → S x).

This is the genuine, load-bearing bridge: setEvery is Set-typed while every_sem is predicate-typed (defeq, but the binder annotations differ, so a named lemma earns its keep). PIP's set-GQ therefore consumes Core's quantifier theory directly — conservativity, the Zwarts monotonicity hierarchy, duality — with no PIP-local re-derivation.

theorem KeshetAbney2024.PIP.Bridges.setSome_eq_some_sem {α : Type u_1} (R S : Set α) : setSome R S ↔ Quantification.some_sem R S

setSome agrees with Quantification.some_sem.

theorem KeshetAbney2024.PIP.Bridges.setEvery_conservative' {α : Type u_1} (R S : Set α) : setEvery R S ↔ setEvery R (R ∩ S)

Conservativity of setEvery, inherited from Quantification.every_conservative (not re-proved).

theorem KeshetAbney2024.PIP.Bridges.setSome_conservative' {α : Type u_1} (R S : Set α) : setSome R S ↔ setSome R (R ∩ S)

Conservativity of setSome, inherited from Quantification.some_conservative (not re-proved).

Plural Bridge: SINGLE/PLURAL ↔ Link 1983

PIP's SINGLE(τ) (paper item 71) and PLURAL(τ) (paper item 84) correspond to Link's Atom and properPlural concepts. The connection is structural:

• SINGLE ↔ the set is a singleton (a "singular" individual = Link's atom)
• PLURAL ↔ the set has 2+ elements (a "plural" individual = non-atom)

The formal connection requires interpreting PIP's sets as Link's lattice elements. PIP summation yields sets of entities; Link's lattice yields join-semilattice elements. The bridge theorem states the correspondence at the level of cardinality conditions.

def KeshetAbney2024.PIP.Bridges.single {α : Type u_1} (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

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

def KeshetAbney2024.PIP.Bridges.plural {α : Type u_1} (s : Set α) : Prop

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

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

Equations

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

theorem KeshetAbney2024.PIP.Bridges.single_singleton {α : Type u_1} (a : α) : single {a}

A singleton set satisfies SINGLE.

theorem KeshetAbney2024.PIP.Bridges.single_not_plural {α : Type u_1} (s : Set α) (hs : single s) : ¬plural s

SINGLE and PLURAL are mutually exclusive.

theorem KeshetAbney2024.PIP.Bridges.atom_iff_single_base {E : Type u_1} [SemilatticeSup E] {P : E → Prop} (hDistr : Semantics.Plurality.Algebra.IsDistr P) {x : E} (hPx : P x) : Mereology.Atom x

Link's Atom corresponds to PIP's SINGLE when the lattice element is the join of a singleton set. If P is a distributive predicate and x satisfies P, then {x} is SINGLE and x is an Atom.

theorem KeshetAbney2024.PIP.Bridges.properPlural_implies_plural {α : Type u_1} {a b : α} (hne : a ≠ b) : plural {a, b}

Proper plurals and PLURAL: if x = a ⊔ b with a ≠ b and both in P, then the corresponding set {a, b} satisfies PLURAL.

Modal Logic: PIP's must needs the T axiom

PIP's must allows anaphora because of a realistic modal base ([Kra91]): the evaluation world w* is accessible from itself (R w* w*). This is exactly the T axiom (□p → p, frame condition: reflexivity).

The must_truth_agrees_box and must_realistic_of_refl theorems in Connectives.lean already prove this correspondence. This section classifies PIP's modal operators in the lattice of normal modal logics from Intensional.

PIP's anaphora-enabling modality needs the T axiom (reflexivity): a realistic modal base guarantees the description holds at the evaluation world. The content of that claim is carried by reflexive_satisfies_T below (reflexivity ⟹ T's frame condition) together with Connectives.must_realistic_of_refl (which consumes Std.Refl R to derive p g w₀). A bare K ≤ T lemma would be vacuous — K = ⊥ — so it is intentionally omitted.

theorem KeshetAbney2024.PIP.Bridges.reflexive_satisfies_T {W : Type u_1} (R : Core.Logic.Modal.AccessRel W) [hRefl : Std.Refl R] : Core.Logic.Modal.Logic.T.frameConditions R

A reflexive accessibility relation satisfies Logic.T's frame condition.

Stated for the Prop-valued AccessRel/Std.Refl/frameConditions API in Intensional — the same accessibility type PIP's modal operators now use directly.

Kratzer Correspondence

PIP's modal operators are generalized quantifiers over worlds with an accessibility relation (paper §2.5):

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

This is structurally identical to [Kra91]'s analysis where:

• β corresponds to the modal base (conversational background)
• The ordering source (for graded modality) is not used in PIP's simple must/might

The formal connection is established via Intensional.box: must_truth_agrees_box (in Connectives.lean) proves that PIP's must R allWorlds (atom p) produces the same truth conditions as box R (p g).

Direct import of Semantics/Modality/Kratzer/ is not possible because Kratzer's implementation is monomorphic over World4. The correspondence is structural (via AccessRel ≅ ModalBase) rather than definitional.

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

Full Kratzer bridge: PIP's three-argument mustBase agrees with box when the modal base comes from an AccessRel and the restriction is tautological.

The composition: mustBase (accessRelToBase R w) ⊤ {w' | φ.truth w'} ↔ box R φ.truth w. Both express "the body holds at every R-accessible world from w".

Static↔Dynamic Agreement

PIP is natively a static, truth-conditional system. Our formalization in Basic.lean / Connectives.lean encodes PIP as a dynamic update system over IContext W E. [Bra10] shows the equivalence between plural predicate calculi and dynamic plural logics.

The following theorems prove that the static system (PIPExprF.truth) and the dynamic encoding (PUpdate operators) compute the same thing for the atomic and negation cases (the proofs are complete).

The full Brasoveanu equivalence requires establishing a bijection between PIP models and ICDRT information states — a substantial model-theoretic argument left as future work, not formalized here.

theorem KeshetAbney2024.PIP.Bridges.static_atom_agrees_dynamic {W : Type u_1} {E : Type u_2} (p : Semantics.Dynamic.Core.ICDRTAssignment W E → W → Prop) (g : Semantics.Dynamic.Core.ICDRTAssignment W E) (w : W) (d : Discourse W E) (hd : (g, w) ∈ d.info) : (g, w) ∈ (atom p d).info ↔ p g w

Static atom truth agrees with dynamic atom filtering.

For an atomic predicate p, PIPExprF.pred p has truth value p w, and atom p filters the info state to pairs where p g w. When the info state is a singleton, the dynamic update is non-empty iff the static truth value is true.

TODO: Full proof requires reasoning about Set.sep over singleton IContext.

theorem KeshetAbney2024.PIP.Bridges.static_neg_agrees_dynamic {W : Type u_1} {E : Type u_2} (φ : PUpdate W E) (g : Semantics.Dynamic.Core.ICDRTAssignment W E) (w : W) (d : Discourse W E) (hd : (g, w) ∈ d.info) : (g, w) ∈ (negation φ d).info ↔ (g, w) ∉ (φ d).info

Static negation truth agrees with dynamic negation filtering.

Negation in both systems complements the truth value / info state. The dynamic system keeps pairs from the input that did NOT survive φ.