Documentation

Linglib.Theories.Semantics.PIP.Expr

PIP Expression Language (Full Static Formulation) #

@cite{keshet-abney-2024}

PIP is natively a static, truth-conditional system: formulas denote truth values relative to a model, plural assignment set G, and evaluation world w*. This file defines the full PIPExpr type matching the paper's thesis that PIP is "just predicate calculus with set abstraction."

Constructors #

The propositional fragment (pred, conj, neg, disj, impl, presup) is extended with:

ConstructorPaper itemDescription
exists_43∃x.φ — existential quantification over domain D
forall_43∀x.φ — universal quantification over domain D
labelDef17.3X ≡ φ — tautological formula label definition
must28□φ — universal modality (EVERY over worlds)
might28◇φ — existential modality (SOME over worlds)

Domain Parameter #

The full PIPExpr is parameterized by both W (worlds) and D (individual domain). Quantifier constructors bind over D, modals bind over W. The propositional-only fragment uses D = Empty (no quantifiers needed).

Label Extraction #

PIPExpr.labelDefs extracts the label assignment from a formula. Since label definitions are tautologies that float freely, this function collects all X ≡ φ definitions regardless of their structural position.

source
class Semantics.PIP.FiniteDomain (D : Type u_1) :
Type u_1

A finite domain of individuals for PIP quantifier evaluation.

  • elements : List D
  • complete (d : D) : d ∈ elements
Instances
    source
    inductive Semantics.PIP.PIPExprF (W : Type u_1) (D : Type u_2) :
    Type (max u_1 u_2)

    PIP expressions: the full static formula language.

    Parameterized by W (possible worlds) and D (individual domain). Each PIP construct from the paper has a constructor.

    The propositional fragment (pred, conj, neg, disj, impl, presup) matches the original Felicity.PIPExpr. The quantifier and modal constructors extend it to the full system.

    • pred {W : Type u_1} {D : Type u_2} (p : W → Bool) : PIPExprF W D

      Atomic predicate: P_w(x₁, ..., xₙ). Always felicitous.

    • conj {W : Type u_1} {D : Type u_2} (φ ψ : PIPExprF W D) : PIPExprF W D

      Conjunction: φ ∧ ψ. Felicity is asymmetric (Karttunen).

    • neg {W : Type u_1} {D : Type u_2} (φ : PIPExprF W D) : PIPExprF W D

      Negation: ¬φ. Felicity passes through.

    • disj {W : Type u_1} {D : Type u_2} (φ ψ : PIPExprF W D) : PIPExprF W D

      Disjunction: φ ∨ ψ.

    • impl {W : Type u_1} {D : Type u_2} (φ ψ : PIPExprF W D) : PIPExprF W D

      Implication: φ → ψ.

    • presup {W : Type u_1} {D : Type u_2} (φ : PIPExprF W D) (ψ : W → Bool) : PIPExprF W D

      Presupposition: φ|ψ. Assert φ, presuppose ψ.

    • exists_ {W : Type u_1} {D : Type u_2} (body : D → PIPExprF W D) : PIPExprF W D

      Existential quantification: ∃x.φ (paper item 43). body takes a domain element and returns a formula.

    • forall_ {W : Type u_1} {D : Type u_2} (body : D → PIPExprF W D) : PIPExprF W D

      Universal quantification: ∀x.φ (paper item 43). body takes a domain element and returns a formula.

    • labelDef {W : Type u_1} {D : Type u_2} (label : FLabel) (φ : PIPExprF W D) : PIPExprF W D

      Formula label definition: X ≡ φ (paper item 17.3). Tautological — always true. Registers the label for later retrieval.

    • must {W : Type u_1} {D : Type u_2} (R : BAccessRel W) (φ : PIPExprF W D) : PIPExprF W D

      Modal necessity: □_R φ (paper item 28, MUST). Universal quantification over R-accessible worlds.

    • might {W : Type u_1} {D : Type u_2} (R : BAccessRel W) (φ : PIPExprF W D) : PIPExprF W D

      Modal possibility: ◇_R φ (paper item 28, MIGHT). Existential quantification over R-accessible worlds.

    Instances For
      source
      noncomputable def Semantics.PIP.PIPExprF.truth {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] :
      PIPExprF W D → W → Bool

      Truth evaluation for full PIP expressions.

      PIP truth conditions are classical: presuppositions play no role in determining truth values. Quantifiers and modals evaluate as standard first-order quantification over domains and worlds.

      Requires [Fintype D] for quantifier evaluation and [Fintype W] for modal evaluation.

      Equations
      Instances For
        source
        noncomputable def Semantics.PIP.PIPExprF.felicitous {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] :
        PIPExprF W D → W → Bool

        The F operator: recursive presuppositional felicity (full version).

        Extends the propositional fragment with:

        • F(∃xφ) iff ∀x.Fφ — felicity is universal over witnesses (item 43)
        • F(∀xφ) iff ∀x.Fφ — felicity is universal over witnesses (item 43)
        • F(X≡φ) iff Fφ — labels don't affect felicity
        • F(□φ) iff ∀w'.Fφ — felicity universal over accessible worlds (item 47)
        • F(◇φ) iff ∀w'.Fφ — felicity universal over accessible worlds (item 47)

        The universal quantification in the quantifier/modal felicity clauses is the key insight: an expression is felicitous only if its presuppositions are met for EVERY possible witness/world, not just some.

        Equations
        Instances For
          source
          def Semantics.PIP.PIPExprF.labelDefs {W : Type u_1} {D : Type u_2} :
          PIPExprF W D → List (FLabel × PIPExprF W D)

          Extract all formula label definitions from an expression.

          Since label definitions X ≡ φ are tautologies that float freely (paper §2.3), we collect them regardless of their structural position (under negation, modals, etc.). Returns a list of (label, sub-expression) pairs.

          Equations
          Instances For
            source
            theorem Semantics.PIP.felicitousF_neg {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (φ : PIPExprF W D) (w : W) :
            φ.neg.felicitous w = φ.felicitous w

            F(¬φ) iff Fφ — negation preserves felicity.

            source
            theorem Semantics.PIP.felicitousF_presup {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (φ : PIPExprF W D) (ψ : W → Bool) (w : W) :
            (φ.presup ψ).felicitous w = (φ.felicitous w && ψ w)

            F(φ|ψ) iff Fφ ∧ ψ(w) — presupposition must hold.

            source
            theorem Semantics.PIP.felicitousF_labelDef {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (α : FLabel) (φ : PIPExprF W D) (w : W) :
            (PIPExprF.labelDef α φ).felicitous w = φ.felicitous w

            F(X≡φ) iff Fφ — label definitions don't affect felicity.

            source
            theorem Semantics.PIP.presupF_truth_independent {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (φ : PIPExprF W D) (ψ : W → Bool) (w : W) :
            (φ.presup ψ).truth w = φ.truth w

            Presupposition truth-independence: φ|ψ is true iff φ is true.

            source
            theorem Semantics.PIP.labelDef_truth_transparent {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (α : FLabel) (φ : PIPExprF W D) (w : W) :
            (PIPExprF.labelDef α φ).truth w = φ.truth w

            Label definitions are truth-transparent: X≡φ is true iff φ is true.

            source
            theorem Semantics.PIP.felicitousF_conj {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (φ ψ : PIPExprF W D) (w : W) :
            (φ.conj ψ).felicitous w = (φ.felicitous w && (!φ.truth w || ψ.felicitous w))

            Conjunction felicity is asymmetric (Karttunen).

            source
            theorem Semantics.PIP.felicitousF_exists {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (body : D → PIPExprF W D) (w : W) :
            (PIPExprF.exists_ body).felicitous w = FiniteDomain.elements.all fun (d : D) => (body d).felicitous w

            Existential felicity is universal over witnesses.

            source
            theorem Semantics.PIP.felicitousF_must {W : Type u_1} {D : Type u_2} [FiniteDomain D] [Fintype W] (R : BAccessRel W) (φ : PIPExprF W D) (w : W) :
            (PIPExprF.must R φ).felicitous w = (List.filter (R w) Finset.univ.toList).all φ.felicitous

            Modal necessity felicity is universal over accessible worlds.