Documentation

Linglib.Theories.Semantics.PIP.Bridges

PIP Integration Bridges #

@cite{keshet-abney-2024} @cite{abney-keshet-2025} @cite{karttunen-1973} @cite{kratzer-1991} @cite{link-1983} @cite{brasoveanu-2010}

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 ↔ PrProp.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 ↔ Core.Logic.Intensional.boxR/diamondR
  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 (@cite{abney-keshet-2025}) 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 and modal bridges are proved; the static↔dynamic bridge uses sorry for the Brasoveanu equivalence (which requires a non-trivial model theory argument).

Presupposition Projection: F ↔ PrProp connectives #

PIP's F operator and Core.Presupposition.PrProp filtering connectives implement the same Karttunen conjunction clause (@cite{karttunen-1973}). These theorems were previously in the study file; they belong in the theory layer because they establish a general correspondence.

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

PIP's conjunction felicity agrees with PrProp.andFilter.

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

PrProp.andFilter (Core.Presupposition): p.presup w && (!p.assertion w || q.presup w)

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

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

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

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

PIP's implication felicity agrees with PrProp.impFilter.

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

This is exactly the filtering implication from @cite{karttunen-1973}: the antecedent can satisfy the consequent's presupposition.

source
theorem Semantics.PIP.Bridges.pip_felicity_agrees_with_orFilter {W : Type u_1} (φ ψ : Felicity.PIPExpr W) (w : W) :
(φ.disj ψ).felicitous w = true ↔ φ.felicitous w = true ∧ (φ.truth w = true ∨ ψ.felicitous w = true)

PIP's disjunction felicity agrees with a one-sided filtering disjunction: F(φ ∨ ψ) = Fφ ∧ (¬φ → Fψ)

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

PIP defines (paper item 28):

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.

source
def Semantics.PIP.Bridges.pipEvery {α : Type u_1} :
Core.Quantification.GQ α

PIP's EVERY as a GQ: ∀x, R(x) → S(x) (= set inclusion).

Equations
Instances For
    source
    def Semantics.PIP.Bridges.pipSome {α : Type u_1} :
    Core.Quantification.GQ α

    PIP's SOME as a GQ: ∃x, R(x) ∧ S(x) (= non-empty intersection).

    Equations
    Instances For
      source
      theorem Semantics.PIP.Bridges.pipEvery_conservative {α : Type u_1} :
      Core.Quantification.Conservative pipEvery

      PIP's EVERY is conservative: EVERY(R, S) ↔ EVERY(R, R ∩ S).

      source
      theorem Semantics.PIP.Bridges.pipEvery_scope_upward_mono {α : Type u_1} :
      Core.Quantification.ScopeUpwardMono pipEvery

      PIP's EVERY is scope-upward-monotone (right upward monotone).

      source
      theorem Semantics.PIP.Bridges.pipSome_conservative {α : Type u_1} :
      Core.Quantification.Conservative pipSome

      PIP's SOME is conservative: SOME(R, S) ↔ SOME(R, R ∩ S).

      source
      theorem Semantics.PIP.Bridges.pipSome_scope_upward_mono {α : Type u_1} :
      Core.Quantification.ScopeUpwardMono pipSome

      PIP's SOME is scope-upward-monotone (right upward monotone).

      source
      theorem Semantics.PIP.Bridges.setEvery_eq_pipEvery {α : Type u_1} (R S : Set α) :
      setEvery R S ↔ pipEvery R S

      setEvery from PIP.Composition agrees with pipEvery (and hence every_sem).

      Both express universal GQ as set inclusion / pointwise implication. This bridge lets setEvery inherit all GQ property proofs (conservativity, monotonicity) from pipEvery_conservative etc.

      source
      theorem Semantics.PIP.Bridges.setSome_eq_pipSome {α : Type u_1} (R S : Set α) :
      setSome R S ↔ pipSome R S

      setSome from PIP.Composition agrees with pipSome (and hence some_sem).

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

      Conservativity of setEvery derived from the GQ proof.

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

      Conservativity of setSome derived from the GQ proof.

      source
      theorem Semantics.PIP.Bridges.pipEvery_eq_every_sem (F : Core.Logic.Intensional.Frame) [Fintype F.Entity] :
      pipEvery = Quantification.Quantifier.every_sem F

      PIP's EVERY is definitionally equal to every_sem from Quantifier.lean.

      This closes the full bridge chain: setEvery R S ↔ pipEvery R S = every_sem m R S

      All GQ property proofs in Quantifier.lean (duality, monotonicity, Zwarts monotonicity hierarchy, quantity invariance, etc.) apply directly to PIP's quantifiers.

      source
      theorem Semantics.PIP.Bridges.pipSome_eq_some_sem (F : Core.Logic.Intensional.Frame) [Fintype F.Entity] :
      pipSome = Quantification.Quantifier.some_sem F

      PIP's SOME is definitionally equal to some_sem from Quantifier.lean.

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

      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.

      source
      def Semantics.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
      Instances For
        source
        def Semantics.PIP.Bridges.plural {α : Type u_1} (s : Set α) :
        Prop

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

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

        Equations
        Instances For
          source
          theorem Semantics.PIP.Bridges.single_singleton {α : Type u_1} (a : α) :
          single {a}

          A singleton set satisfies SINGLE.

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

          SINGLE and PLURAL are mutually exclusive.

          source
          theorem Semantics.PIP.Bridges.atom_iff_single_base {E : Type u_1} [SemilatticeSup E] {P : E → Prop} (hDistr : Plurality.Link1983.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.

          source
          theorem Semantics.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.

          PIP's must allows anaphora because of a realistic modal base (@cite{kratzer-1991}): the evaluation world w* is accessible from itself (R w* w* = true). This is exactly the T axiom (□p → p, frame condition: reflexivity).

          The must_truth_agrees_kripkeEval 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 Core.Logic.Intensional.

          source
          theorem Semantics.PIP.Bridges.pip_anaphora_requires_T :
          Core.Logic.Intensional.Logic.K ≤ Core.Logic.Intensional.Logic.T

          PIP's anaphora-enabling modality requires at least Logic.T.

          The might/must asymmetry for intensional anaphora reduces to whether the accessibility relation satisfies the T axiom (reflexivity). Must with a reflexive R guarantees the description holds at the evaluation world; might with a non-reflexive R does not.

          source
          theorem Semantics.PIP.Bridges.reflexive_satisfies_T {W : Type u_1} (R : Core.Logic.Intensional.AccessRel W) (hRefl : Core.Logic.Intensional.IsReflexive R) :
          Core.Logic.Intensional.Logic.T.frameConditions R

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

          Stated for the Prop-valued AccessRel/IsReflexive/frameConditions API in Core.Logic.Intensional. To apply this to a PIP BAccessRel R, lift via liftR R = fun a b => R a b = true.

          Kratzer Correspondence #

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

          This is structurally identical to @cite{kratzer-1991}'s analysis where:

          The formal connection is established via Core.Logic.Intensional.boxR: must_truth_agrees_boxR (in Connectives.lean) proves that PIP's must R allWorlds (atom p) produces the same truth conditions as boxR (liftR R) (liftP (p g)).

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

          source
          theorem Semantics.PIP.Bridges.mustBase_agrees_boxR {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (R : BAccessRel W) (φ : PIPExprF W D) (w : W) :
          mustBase (accessRelToBase R w) Set.univ {w' : W | φ.truth w' = true} ↔ Core.Logic.Intensional.boxR (fun (a b : W) => R a b = true) (fun (w' : W) => φ.truth w' = true) w

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

          The composition: mustBase (accessRelToBase R w) ⊤ {w' | φ w' = true} ↔ boxR (fun a b => R a b = true) (fun w' => φ w' = true) 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. @cite{brasoveanu-2010} shows the equivalence between plural predicate calculi and dynamic plural logics.

          The following theorems state that the static system (PIPExprF.truth) and the dynamic encoding (PUpdate operators) compute the same thing for atomic formulas, conjunction, negation, and presupposition.

          Full proof of the Brasoveanu equivalence requires establishing a bijection between PIP models and ICDRT information states, which is a substantial model-theoretic argument. We mark these with sorry.

          source
          theorem Semantics.PIP.Bridges.static_atom_agrees_dynamic {W : Type u_1} {E : Type u_2} (p : Dynamic.Core.ICDRTAssignment W E → W → Bool) (g : 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 = true

          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 = true. 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.

          source
          theorem Semantics.PIP.Bridges.static_neg_agrees_dynamic {W : Type u_1} {E : Type u_2} (φ : PUpdate W E) (g : 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 φ.