PIP Expression Language (Full Static Formulation)

[KA24]

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:

Constructor	Paper item	Description
exists_	43	∃x.φ — existential quantification over domain D
forall_	43	∀x.φ — universal quantification over domain D
labelDef	17.3	X ≡ φ — tautological formula label definition
must	28	□φ — universal modality (EVERY over worlds)
might	28	◇φ — 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.

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

inductive KeshetAbney2024.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 → Prop) : 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 → Prop) : 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.φ. 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.φ. 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 : Core.Logic.Modal.AccessRel W) (φ : PIPExprF W D) : PIPExprF W D

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

• might {W : Type u_1} {D : Type u_2} (R : Core.Logic.Modal.AccessRel W) (φ : PIPExprF W D) : PIPExprF W D

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

def KeshetAbney2024.PIP.PIPExprF.truth {W : Type u_1} {D : Type u_2} : PIPExprF W D → W → Prop

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

• (KeshetAbney2024.PIP.PIPExprF.pred p).truth = p
• (φ.conj ψ).truth = fun (w : W) => φ.truth w ∧ ψ.truth w
• φ.neg.truth = fun (w : W) => ¬φ.truth w
• (φ.disj ψ).truth = fun (w : W) => φ.truth w ∨ ψ.truth w
• (φ.impl ψ).truth = fun (w : W) => φ.truth w → ψ.truth w
• (φ.presup _ψ).truth = φ.truth
• (KeshetAbney2024.PIP.PIPExprF.exists_ body).truth = fun (w : W) => ∃ (d : D), (body d).truth w
• (KeshetAbney2024.PIP.PIPExprF.forall_ body).truth = fun (w : W) => ∀ (d : D), (body d).truth w
• (KeshetAbney2024.PIP.PIPExprF.labelDef _label φ).truth = φ.truth
• (KeshetAbney2024.PIP.PIPExprF.must R φ).truth = Core.Logic.Modal.box R φ.truth
• (KeshetAbney2024.PIP.PIPExprF.might R φ).truth = Core.Logic.Modal.diamond R φ.truth

def KeshetAbney2024.PIP.PIPExprF.felicitous {W : Type u_1} {D : Type u_2} : PIPExprF W D → W → Prop

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
• F(◇φ) iff ∀w'.Fφ — felicity universal over accessible worlds

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

• (KeshetAbney2024.PIP.PIPExprF.pred p).felicitous = fun (x : W) => True
• (φ.conj ψ).felicitous = fun (w : W) => φ.felicitous w ∧ (φ.truth w → ψ.felicitous w)
• φ.neg.felicitous = φ.felicitous
• (φ.disj ψ).felicitous = fun (w : W) => φ.felicitous w ∧ (¬φ.truth w → ψ.felicitous w)
• (φ.impl ψ).felicitous = fun (w : W) => φ.felicitous w ∧ (φ.truth w → ψ.felicitous w)
• (φ.presup _ψ).felicitous = fun (w : W) => φ.felicitous w ∧ _ψ w
• (KeshetAbney2024.PIP.PIPExprF.exists_ body).felicitous = fun (w : W) => ∀ (d : D), (body d).felicitous w
• (KeshetAbney2024.PIP.PIPExprF.forall_ body).felicitous = fun (w : W) => ∀ (d : D), (body d).felicitous w
• (KeshetAbney2024.PIP.PIPExprF.labelDef _label φ).felicitous = φ.felicitous
• (KeshetAbney2024.PIP.PIPExprF.must R φ).felicitous = Core.Logic.Modal.box R φ.felicitous
• (KeshetAbney2024.PIP.PIPExprF.might R φ).felicitous = Core.Logic.Modal.box R φ.felicitous

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

• (KeshetAbney2024.PIP.PIPExprF.pred p).labelDefs = []
• (φ.conj ψ).labelDefs = φ.labelDefs ++ ψ.labelDefs
• φ.neg.labelDefs = φ.labelDefs
• (φ.disj ψ).labelDefs = φ.labelDefs ++ ψ.labelDefs
• (φ.impl ψ).labelDefs = φ.labelDefs ++ ψ.labelDefs
• (φ.presup _ψ).labelDefs = φ.labelDefs
• (KeshetAbney2024.PIP.PIPExprF.exists_ body).labelDefs = []
• (KeshetAbney2024.PIP.PIPExprF.forall_ body).labelDefs = []
• (KeshetAbney2024.PIP.PIPExprF.labelDef _label φ).labelDefs = (_label, φ) :: φ.labelDefs
• (KeshetAbney2024.PIP.PIPExprF.must R φ).labelDefs = φ.labelDefs
• (KeshetAbney2024.PIP.PIPExprF.might R φ).labelDefs = φ.labelDefs

theorem KeshetAbney2024.PIP.felicitousF_neg {W : Type u_1} {D : Type u_2} (φ : PIPExprF W D) (w : W) : φ.neg.felicitous w = φ.felicitous w

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

theorem KeshetAbney2024.PIP.felicitousF_presup {W : Type u_1} {D : Type u_2} (φ : PIPExprF W D) (ψ : W → Prop) (w : W) : (φ.presup ψ).felicitous w = (φ.felicitous w ∧ ψ w)

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

theorem KeshetAbney2024.PIP.felicitousF_labelDef {W : Type u_1} {D : Type u_2} (α : FLabel) (φ : PIPExprF W D) (w : W) : (PIPExprF.labelDef α φ).felicitous w = φ.felicitous w

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

theorem KeshetAbney2024.PIP.presupF_truth_independent {W : Type u_1} {D : Type u_2} (φ : PIPExprF W D) (ψ : W → Prop) (w : W) : (φ.presup ψ).truth w = φ.truth w

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

theorem KeshetAbney2024.PIP.labelDef_truth_transparent {W : Type u_1} {D : Type u_2} (α : FLabel) (φ : PIPExprF W D) (w : W) : (PIPExprF.labelDef α φ).truth w = φ.truth w

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

theorem KeshetAbney2024.PIP.felicitousF_conj {W : Type u_1} {D : Type u_2} (φ ψ : PIPExprF W D) (w : W) : (φ.conj ψ).felicitous w = (φ.felicitous w ∧ (φ.truth w → ψ.felicitous w))

Conjunction felicity is asymmetric (Karttunen).

theorem KeshetAbney2024.PIP.felicitousF_exists {W : Type u_1} {D : Type u_2} (body : D → PIPExprF W D) (w : W) : (PIPExprF.exists_ body).felicitous w = ∀ (d : D), (body d).felicitous w

Existential felicity is universal over witnesses.

theorem KeshetAbney2024.PIP.felicitousF_must {W : Type u_1} {D : Type u_2} (R : Core.Logic.Modal.AccessRel W) (φ : PIPExprF W D) (w : W) : (PIPExprF.must R φ).felicitous w = Core.Logic.Modal.box R φ.felicitous w

Modal necessity felicity is universal over accessible worlds.