PIP Felicity Conditions (Static Formulation) #
@cite{keshet-abney-2024} @cite{karttunen-1973}
PIP separates truth conditions from felicity conditions. Truth is classical (predicate calculus + set abstraction). Felicity is a separate recursive predicate F that determines whether presuppositions are met.
This file provides:
- An inductive
PIPExprtype representing PIP's propositional fragment - A recursive
felicitousfunction implementing the F operator - The key derived theorems from the paper (items 41–42, 44–45c)
The F Operator #
F is defined recursively on the structure of PIP expressions. This file covers the propositional fragment (items 40–42, 44–45c):
| Expression | Felicity condition |
|---|---|
| φ|ψ | Fφ ∧ ψ |
| φ ∧ ψ | Fφ ∧ (φ → Fψ) |
| ¬φ | Fφ |
| P(α₁,...,αₙ) | true |
The quantifier clauses (F(∃xφ) iff ∀x.Fφ, item 43) require a separate
domain type D and are not included here. See PIPExpr docstring.
The asymmetric conjunction clause (Karttunen's insight) allows the first conjunct to satisfy presuppositions of the second. This is what makes "France has a king and the king of France is bald" felicitous.
Incremental Discourse Felicity #
Adding sentence φ to a felicitous discourse γ requires:
∀w x (γ → Fφ)
where x ranges over the combined local variables of γ and φ. This condition ensures that the presuppositions of φ are met in every world and assignment consistent with γ.
PIP expressions: the static formula language.
This represents PIP formulas as a data type, enabling recursive definition of truth and felicity conditions. Each propositional PIP construct has a constructor.
Quantifiers omitted. The paper's ∃x, ∀x, Σx quantify over a domain of
individuals D (paper items 43, 47a-d). A correct encoding requires a separate
domain parameter D and body : D → PIPExpr W, with:
- F(∃xφ) iff ∀d:D, F(body d) — felicity universal over witnesses
- T(∃xφ) iff ∃d:D, T(body d) — truth existential The propositional fragment (pred, conj, neg, disj, impl, presup) is complete and correctly implements the F operator for items 41–42, 44–45c.
- pred
{W : Type u_2}
(p : W → Bool)
: PIPExpr W
Atomic predicate: P_w(x₁, ..., xₙ). Always felicitous.
- conj
{W : Type u_2}
(φ ψ : PIPExpr W)
: PIPExpr W
Conjunction: φ ∧ ψ. Felicity is asymmetric (Karttunen).
- neg
{W : Type u_2}
(φ : PIPExpr W)
: PIPExpr W
Negation: ¬φ. Felicity passes through.
- disj
{W : Type u_2}
(φ ψ : PIPExpr W)
: PIPExpr W
Disjunction: φ ∨ ψ.
- impl
{W : Type u_2}
(φ ψ : PIPExpr W)
: PIPExpr W
Implication: φ → ψ.
- presup
{W : Type u_2}
(φ : PIPExpr W)
(ψ : W → Bool)
: PIPExpr W
Presupposition: φ|ψ. Assert φ, presuppose ψ.
Instances For
Truth evaluation for PIP expressions.
PIP truth conditions are classical: presuppositions play no role in determining truth values. φ|ψ is true iff φ is true.
Equations
Instances For
The F operator: recursive presuppositional felicity.
This is the core of PIP's analysis of intensional anaphora. F determines whether a PIP expression is felicitous (well-defined) relative to a world w. Every failure of F traces to a presupposition violation.
Equations
- (Semantics.PIP.Felicity.PIPExpr.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
Instances For
F(¬φ) iff Fφ (paper item 45c)
F(φ|ψ) iff Fφ ∧ ψ(w) (paper item 41)
Conjunction felicity is asymmetric (paper item 42, @cite{karttunen-1973}): the first conjunct can satisfy presuppositions of the second.
If the first conjunct is true and both are felicitous, the conjunction is felicitous.
If the first conjunct is false, its felicity suffices for the conjunction.
A discourse (conjunction of sentences) is felicitous when the felicity conditions are met at every world in the context set.
This captures the paper's item 40: F(Σw(φ₁ ∧ ... ∧ φₙ))
Equations
- Semantics.PIP.Felicity.discourseFelicitous φ contextSet = ∀ (w : W), contextSet w = true → φ.felicitous w = true
Instances For
Incremental felicity: adding sentence ψ to a felicitous discourse φ requires that ψ's presuppositions are met whenever φ is true.
This captures the paper's item 51: ∀wxy(γ → Fφ)
Equations
- Semantics.PIP.Felicity.incrementallyFelicitous γ ψ = ∀ (w : W), γ.truth w = true → ψ.felicitous w = true
Instances For
The existential presupposition of pronouns.
A pronoun presupposes that its denotation is non-empty (and singular for singular pronouns). In PIP, this is modeled as a presupposition on the summation term: SINGLE(Σxφ).
Equations
- Semantics.PIP.Felicity.singlePresup denotation = (Semantics.PIP.Felicity.PIPExpr.pred fun (x : W) => true).presup denotation
Instances For
Might blocks anaphora: might(φ) does not guarantee that the antecedent description is non-empty at every world in the context set.
If might(φ) is true at w, there exists an accessible w' where φ holds, but φ may be false at w itself. A pronoun referring to an entity introduced by φ will have an empty denotation at w, causing presupposition failure.
Must allows anaphora: if must(φ) is true at w (with a realistic modal base), then φ holds at w (since w is accessible from itself). The pronoun's presupposition is satisfied.