PIP Felicity Conditions (Propositional Fragment)

@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:

1. An inductive PIPExpr type representing PIP's propositional fragment
2. A recursive felicitous function implementing the F operator
3. The key derived theorems from the paper (items 41–42, 44–45c)

Relationship to PIP.Expr

PIPExprF W D in Expr.lean is the full PIP expression type with quantifiers (∃x, ∀x), modals (□, ◇), and label definitions. It defines its own truth and felicitous functions covering all constructors, including the quantifier felicity clauses (items 35, 39d). The propositional PIPExpr W here is the restriction to D = Empty.

The F Operator (Propositional)

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 full quantifier/modal clauses are in PIPExprF.felicitous (Expr.lean):

• F(∃xφ) iff ∀x.Fφ — felicity universal over witnesses (item 43)
• F(□φ) iff ∀w'.Fφ — felicity universal over accessible worlds (item 47)

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 γ.

inductive Semantics.PIP.Felicity.PIPExpr (W : Type u_2) : Type u_2

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 ψ.

def Semantics.PIP.Felicity.PIPExpr.truth {W : Type u_1} : PIPExpr W → W → Bool

Truth evaluation for PIP expressions.

PIP truth conditions are classical: presuppositions play no role in determining truth values. φ|ψ is true iff φ is true.

Equations

• (Semantics.PIP.Felicity.PIPExpr.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

def Semantics.PIP.Felicity.PIPExpr.felicitous {W : Type u_1} : PIPExpr W → W → Bool

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

theorem Semantics.PIP.Felicity.felicitous_neg {W : Type u_1} (φ : PIPExpr W) (w : W) : φ.neg.felicitous w = φ.felicitous w

F(¬φ) iff Fφ (paper item 45c)

theorem Semantics.PIP.Felicity.felicitous_presup {W : Type u_1} (φ : PIPExpr W) (ψ : W → Bool) (w : W) : (φ.presup ψ).felicitous w = (φ.felicitous w && ψ w)

F(φ|ψ) iff Fφ ∧ ψ(w) (paper item 41)

theorem Semantics.PIP.Felicity.presup_truth_independent {W : Type u_1} (φ : PIPExpr W) (ψ : W → Bool) (w : W) : (φ.presup ψ).truth w = φ.truth w

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

theorem Semantics.PIP.Felicity.felicitous_conj {W : Type u_1} (φ ψ : PIPExpr W) (w : W) : (φ.conj ψ).felicitous w = (φ.felicitous w && (!φ.truth w || ψ.felicitous w))

Conjunction felicity is asymmetric (paper item 42, @cite{karttunen-1973}): the first conjunct can satisfy presuppositions of the second.

theorem Semantics.PIP.Felicity.felicitous_conj_of_both {W : Type u_1} (φ ψ : PIPExpr W) (w : W) (hFφ : φ.felicitous w = true) (hFψ : ψ.felicitous w = true) : (φ.conj ψ).felicitous w = true

If the first conjunct is true and both are felicitous, the conjunction is felicitous.

theorem Semantics.PIP.Felicity.felicitous_conj_of_false_first {W : Type u_1} (φ ψ : PIPExpr W) (w : W) (hFφ : φ.felicitous w = true) (hTφ : φ.truth w = false) : (φ.conj ψ).felicitous w = true

If the first conjunct is false, its felicity suffices for the conjunction.

def Semantics.PIP.Felicity.discourseFelicitous {W : Type u_1} (φ : PIPExpr W) (contextSet : W → Bool) : Prop

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

def Semantics.PIP.Felicity.incrementallyFelicitous {W : Type u_1} (γ ψ : PIPExpr W) : Prop

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

def Semantics.PIP.Felicity.singlePresup {W : Type u_1} (denotation : W → Bool) : PIPExpr W

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

theorem Semantics.PIP.Felicity.might_blocks_anaphora {W : Type u_1} (φ_accessible pronoun_presup : W → Bool) (w : W) (h_might : φ_accessible w = false) (h_presup_needs : pronoun_presup w = φ_accessible w) : (singlePresup pronoun_presup).felicitous w = false

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.

theorem Semantics.PIP.Felicity.must_allows_anaphora {W : Type u_1} (φ_everywhere pronoun_presup : W → Bool) (w : W) (h_must_realistic : φ_everywhere w = true) (h_presup_follows : pronoun_presup w = φ_everywhere w) : (singlePresup pronoun_presup).felicitous w = true

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.

Quantifier and Modal Felicity Projection

@cite{abney-keshet-2025}

The full PIPExprF type (Expr.lean) extends the propositional fragment with quantifiers and modals. Its felicitous function implements the paper's key design: felicity projects universally through both quantifiers and modals, while truth projects existentially or universally as usual. This asymmetry is PIP's mechanism for presupposition projection.

The felicity clauses (in PIPExprF.felicitous):

• F(∃xφ) = ∀x.Fφ — universal over witnesses (item 39d)
• F(∀xφ) = ∀x.Fφ — (item 35)
• F(□φ) = ∀w'.Fφ — universal over accessible worlds
• F(◇φ) = ∀w'.Fφ — ALSO universal (truth differs: existential)

This section derives:

1. Prop-level iff characterizations for each clause
2. Factored presupposition projection — the strongest form: a presupposition under a universally-felicitous operator factors out of the universal check. This is an instance of forall_and_right (quantifiers, uniform ψ, requires Nonempty D) or forall_and (modals, world-varying ψ, unconditional).
3. One-directional extraction as corollaries

theorem Semantics.PIP.Felicity.existsF_felicitous_iff {W : Type u_2} {D : Type u_3} [FiniteDomain D] [Fintype W] (body : D → PIPExprF W D) (w : W) : (PIPExprF.exists_ body).felicitous w = true ↔ ∀ (d : D), (body d).felicitous w = true

F(∃xφ) iff ∀d, F(φ(d)) — existential felicity is universal over the domain (item 39d).

theorem Semantics.PIP.Felicity.forallF_felicitous_iff {W : Type u_2} {D : Type u_3} [FiniteDomain D] [Fintype W] (body : D → PIPExprF W D) (w : W) : (PIPExprF.forall_ body).felicitous w = true ↔ ∀ (d : D), (body d).felicitous w = true

F(∀xφ) iff ∀d, F(φ(d)) (item 35).

theorem Semantics.PIP.Felicity.existsF_forallF_felicity_agree {W : Type u_2} {D : Type u_3} [FiniteDomain D] [Fintype W] (body : D → PIPExprF W D) (w : W) : (PIPExprF.exists_ body).felicitous w = (PIPExprF.forall_ body).felicitous w

∃ and ∀ have identical felicity clauses — both project universally. The difference is only in truth conditions (∃ vs ∀).

theorem Semantics.PIP.Felicity.mustF_felicitous_iff {W : Type u_2} {D : Type u_3} [FiniteDomain D] [Fintype W] (R : BAccessRel W) (φ : PIPExprF W D) (w : W) : (PIPExprF.must R φ).felicitous w = true ↔ ∀ (w' : W), R w w' = true → φ.felicitous w' = true

F(□_R φ) iff φ is felicitous at every R-accessible world.

theorem Semantics.PIP.Felicity.mightF_felicitous_iff {W : Type u_2} {D : Type u_3} [FiniteDomain D] [Fintype W] (R : BAccessRel W) (φ : PIPExprF W D) (w : W) : (PIPExprF.might R φ).felicitous w = true ↔ ∀ (w' : W), R w w' = true → φ.felicitous w' = true

F(◇_R φ) iff φ is felicitous at every R-accessible world. Truth is existential for ◇ but felicity is universal for both.

theorem Semantics.PIP.Felicity.mustF_mightF_felicity_agree {W : Type u_2} {D : Type u_3} [FiniteDomain D] [Fintype W] (R : BAccessRel W) (φ : PIPExprF W D) (w : W) : (PIPExprF.must R φ).felicitous w = (PIPExprF.might R φ).felicitous w

□ and ◇ have identical felicity clauses — both project universally. The asymmetry between must and might is in truth, not felicity.

theorem Semantics.PIP.Felicity.existsF_presup_factored {W : Type u_2} {D : Type u_3} [FiniteDomain D] [Fintype W] [Nonempty D] (φ : D → PIPExprF W D) (ψ : W → Bool) (w : W) : (PIPExprF.exists_ fun (d : D) => (φ d).presup ψ).felicitous w = true ↔ (∀ (d : D), (φ d).felicitous w = true) ∧ ψ w = true

Factored projection through ∃: a uniform presupposition ψ factors out of the universal felicity check.

F(∃x(φ(x)|ψ)) ↔ (∀d, F(φ(d))) ∧ ψ

This is the strongest form of quantifier presupposition projection. Nonempty D is required: if D is empty, the LHS is vacuously true regardless of ψ (no witnesses to check), so the → direction fails.

Mathematically, this is forall_and_right (Mathlib): the presupposition ψ doesn't vary with d, so it factors out of ∀d, (F(φ(d)) ∧ ψ).

theorem Semantics.PIP.Felicity.forallF_presup_factored {W : Type u_2} {D : Type u_3} [FiniteDomain D] [Fintype W] [Nonempty D] (φ : D → PIPExprF W D) (ψ : W → Bool) (w : W) : (PIPExprF.forall_ fun (d : D) => (φ d).presup ψ).felicitous w = true ↔ (∀ (d : D), (φ d).felicitous w = true) ∧ ψ w = true

Factored projection through ∀ — identical to ∃ since both have the same felicity clause.

theorem Semantics.PIP.Felicity.mustF_presup_factored {W : Type u_2} {D : Type u_3} [FiniteDomain D] [Fintype W] (R : BAccessRel W) (φ : PIPExprF W D) (ψ : W → Bool) (w : W) : (PIPExprF.must R (φ.presup ψ)).felicitous w = true ↔ (∀ (w' : W), R w w' = true → φ.felicitous w' = true) ∧ ∀ (w' : W), R w w' = true → ψ w' = true

Factored projection through □: presupposition ψ and body felicity separate into independent universal checks over accessible worlds.

F(□(φ|ψ)) ↔ (∀w', R w w' → F(φ)(w')) ∧ (∀w', R w w' → ψ(w'))

No Nonempty hypothesis needed: ψ varies with w', so this is a direct instance of ∀x, (P x ∧ Q x) ↔ (∀x, P x) ∧ (∀x, Q x).

theorem Semantics.PIP.Felicity.mightF_presup_factored {W : Type u_2} {D : Type u_3} [FiniteDomain D] [Fintype W] (R : BAccessRel W) (φ : PIPExprF W D) (ψ : W → Bool) (w : W) : (PIPExprF.might R (φ.presup ψ)).felicitous w = true ↔ (∀ (w' : W), R w w' = true → φ.felicitous w' = true) ∧ ∀ (w' : W), R w w' = true → ψ w' = true

Factored projection through ◇ — identical structure to □.

theorem Semantics.PIP.Felicity.existsF_presup_projection {W : Type u_2} {D : Type u_3} [FiniteDomain D] [Fintype W] (φ : D → PIPExprF W D) (ψ : W → Bool) (w : W) (d : D) (hF : (PIPExprF.exists_ fun (d : D) => (φ d).presup ψ).felicitous w = true) : ψ w = true

Presupposition extraction through ∃: if ∃x(φ(x)|ψ) is felicitous, then ψ holds. Follows from the factored form by projecting .2.

theorem Semantics.PIP.Felicity.forallF_presup_projection {W : Type u_2} {D : Type u_3} [FiniteDomain D] [Fintype W] (φ : D → PIPExprF W D) (ψ : W → Bool) (w : W) (d : D) (hF : (PIPExprF.forall_ fun (d : D) => (φ d).presup ψ).felicitous w = true) : ψ w = true

Presupposition extraction through ∀.

theorem Semantics.PIP.Felicity.mustF_presup_at_accessible {W : Type u_2} {D : Type u_3} [FiniteDomain D] [Fintype W] (R : BAccessRel W) (φ : PIPExprF W D) (ψ : W → Bool) (w w' : W) (hR : R w w' = true) (hF : (PIPExprF.must R (φ.presup ψ)).felicitous w = true) : ψ w' = true

Presupposition extraction through □ at an accessible world.

theorem Semantics.PIP.Felicity.mightF_presup_at_accessible {W : Type u_2} {D : Type u_3} [FiniteDomain D] [Fintype W] (R : BAccessRel W) (φ : PIPExprF W D) (ψ : W → Bool) (w w' : W) (hR : R w w' = true) (hF : (PIPExprF.might R (φ.presup ψ)).felicitous w = true) : ψ w' = true

Presupposition extraction through ◇ at an accessible world.

theorem Semantics.PIP.Felicity.sigma_body_felicitous_iff {W : Type u_2} {D : Type u_3} [FiniteDomain D] [Fintype W] (body : D → PIPExprF W D) (w : W) : (∀ (d : D), (body d).felicitous w = true) ↔ (PIPExprF.exists_ body).felicitous w = true

Sigma body felicity: for Σxφ to appear felicitously in a discourse, φ must be felicitous for every witness d. This is item (39f) in the common case with no additional local variables. Since sigmaEval (Composition.lean) takes the same body type D → PIPExprF W D as ∃, sigma felicity reduces to existential felicity.