Presuppositional Conditionals: K/P vs K/P*

@cite{sharvit-2025} @cite{heim-1992} @cite{rooth-partee-1982} @cite{karttunen-peters-1979}

Formalizes the contrast between Karttunen/Peters (K/P) and Sharvit's K/P* conditionals from "Rooth-Partee Conditionals" (Linguistics & Philosophy, 2025).

The problem

Rooth-Partee conditionals like "If Mia is penniless or proud of her money, Sue is (too)" have two readings:

• if-over-∃: single conditional with disjunctive antecedent
• ∀-over-if: conjunction of two conditionals (one per disjunct)

Under K/P, the disjunction or^{K/P}(penniless, proud-of-money) is UNDEFINED at worlds where "proud of her money"'s presupposition ("has money") fails. This causes penniless-worlds to drop from the ∃-reading's quantification domain, while the ∀-reading's first conditional still covers them. Result: the two readings are NOT Strawson-equivalent.

The fix

K/P* replaces K/P's local presupposition filtering ("if p₁(w) = False or p₂(w) is defined") with CLOS-based filtering ("p₂ is defined at all CLOS-closest p₁-worlds"). This is the same closest-worlds operator used in Counterfactual.closestWorlds.

Key definitions

• closB: Computable closest-worlds selector (= closestWorldsB)
• ifPresup: K/P* conditional with CLOS-based filtering
• ifKP: K/P conditional with local filtering (for comparison)
• trivialCloser: Degenerate similarity (all worlds equally close)

def Semantics.Conditionals.Presuppositional.closB {W : Type u_1} [DecidableEq W] (closer : W → W → W → Bool) (restriction antecedent : List W) (w : W) : List W

Computable CLOS (@cite{sharvit-2025}, (120)).

Selects worlds in antecedent ∩ restriction that are not dominated under the similarity ordering. Same formula as Counterfactual.closestWorldsB.

Equations

• One or more equations did not get rendered due to their size.

def Semantics.Conditionals.Presuppositional.trivialCloser {W : Type u_1} : W → W → W → Bool

Degenerate similarity: all worlds are equally close.

With trivial similarity, closB returns ALL p-worlds in the restriction. K/P* with trivial similarity has the same assertion as K/P, but the presupposition is global (all p-worlds) vs local (evaluation world).

Equations

• Semantics.Conditionals.Presuppositional.trivialCloser x✝² x✝¹ x✝ = true

def Semantics.Conditionals.Presuppositional.ifPresup {W : Type u_1} [DecidableEq W] (closer : W → W → W → Bool) (restriction : List W) (p q : Core.Presupposition.PrProp W) : Core.Presupposition.PrProp W

K/P* presuppositional conditional (@cite{sharvit-2025}, (119)).

• Outer presupposition: p must be defined at w
• Inner presupposition (CLOS): q must be defined at all CLOS-closest p-worlds (contrast with K/P's LOCAL check)
• Assertion: q holds at all CLOS-closest p-worlds

When the antecedent p has no presupposition, use PrProp.ofBProp.

Equations

• One or more equations did not get rendered due to their size.

def Semantics.Conditionals.Presuppositional.ifKP {W : Type u_1} [DecidableEq W] (restriction : List W) (p q : Core.Presupposition.PrProp W) : Core.Presupposition.PrProp W

K/P presuppositional conditional (@cite{sharvit-2025}, (100)).

• Outer presupposition: p must be defined at w (same as K/P*)
• Inner presupposition (LOCAL): if p is true at w, q must be defined at w — checks ONLY the evaluation world
• Assertion: q holds at all p-worlds in the restriction (same quantificational domain as K/P* with trivial similarity)

The difference from K/P* is entirely in the inner presupposition: K/P checks locally at w, K/P* checks globally via CLOS.

Equations

• One or more equations did not get rendered due to their size.

def Semantics.Conditionals.Presuppositional.cpAcceptable {W : Type u_1} (c p : BProp W) : Prop

Contextual Plausibility (CP): no uninformative sub-expressions.

A proposition is CP-acceptable in context c iff it is neither trivially true nor trivially false in c.

Equations

• Semantics.Conditionals.Presuppositional.cpAcceptable c p = ((∃ (w : W), c w = true ∧ p w = true) ∧ ∃ (w : W), c w = true ∧ p w = false)

def Semantics.Conditionals.Presuppositional.orProperties {E : Type u_2} [DecidableEq (E → Bool)] (q₁ q₂ : E → Bool) : (E → Bool) → Bool

Type-flexible disjunction over properties (Sharvit's or^{K/P**}, (142a)).

Given two properties Q₁, Q₂ : E → Bool, produces a generalized quantifier over properties: fun Z => Z = Q₁ ∨ Z = Q₂. This enables the ∀-over-if reading by making the universal quantifier range over {Q₁, Q₂}.

Equations

• Semantics.Conditionals.Presuppositional.orProperties q₁ q₂ z = (z == q₁ || z == q₂)

def Semantics.Conditionals.Presuppositional.definedFalse {W : Type u_1} (p : Core.Presupposition.PrProp W) : BProp W

Worlds where p is defined and its assertion is false.

Used in orPresup: the CLOS-based disjunction checks presuppositions at closest worlds where the OTHER disjunct is defined-and-false.

Equations

• Semantics.Conditionals.Presuppositional.definedFalse p w = (p.presup w && !p.assertion w)

def Semantics.Conditionals.Presuppositional.andPresup {W : Type u_1} [DecidableEq W] (closer : W → W → W → Bool) (restriction : List W) (p q : Core.Presupposition.PrProp W) : Core.Presupposition.PrProp W

K/P* presuppositional conjunction (@cite{sharvit-2025}, (127)).

• Presupposition: P₁ defined at w, P₂ defined at w, and P₂ defined at all CLOS-closest P₁-assertion-worlds.
• Assertion: P₁(w) ∧ P₂(w)

This is asymmetric: the CLOS-based check only goes from P₁-worlds to P₂. The asymmetry mirrors K/P's andFilter, but uses CLOS-based rather than local presupposition checking.

Equations

• One or more equations did not get rendered due to their size.

def Semantics.Conditionals.Presuppositional.orPresup {W : Type u_1} [DecidableEq W] (closer : W → W → W → Bool) (restriction : List W) (p q : Core.Presupposition.PrProp W) : Core.Presupposition.PrProp W

K/P* presuppositional disjunction (@cite{sharvit-2025}, (128)).

• Presupposition: (and^{K/P*}(P₁)(P₂) defined OR and^{K/P*}(P₂)(P₁) defined), AND and^{K/P*}(¬P₁)(P₂) defined, AND and^{K/P*}(¬P₂)(P₁) defined. Here ¬Pᵢ means the presuppositionless proposition "Pᵢ is defined and false" (definedFalse).
• Assertion: P₁(w) ∨ P₂(w)

or^{K/P\*} is more symmetric than and^{K/P\*}: condition 1 is a disjunction over both asymmetric directions, and conditions 2-3 are symmetric by construction.

Note: For the Rooth-Partee puzzle where disjuncts have conflicting presuppositions (penniless entails ¬hasMoney, proud presupposes hasMoney), the propositional or^{K/P\*} may still be undefined at worlds where one presupposition fails. The paper's full solution uses K/P** (type-flexible connectives, (142)) which operates at the property level.

Equations

• One or more equations did not get rendered due to their size.

def Semantics.Conditionals.Presuppositional.clos {W : Type u_1} (closer : W → W → W → Prop) (restriction antecedent : Set W) (w : W) : Set W

Set-based CLOS (@cite{sharvit-2025}, (120)).

Definitionally identical to Counterfactual.closestWorlds with reordered parameters: clos closer R A w = closestWorlds sim R w A when sim.closer = closer. Both select the non-dominated elements of antecedent ∩ restriction under the similarity ordering centered at w.

Equations

• Semantics.Conditionals.Presuppositional.clos closer restriction antecedent w = {w' : W | w' ∈ antecedent ∩ restriction ∧ ∀ w'' ∈ antecedent ∩ restriction, closer w w' w'' ∨ ¬closer w w'' w'}

theorem Semantics.Conditionals.Presuppositional.orFilter_symmetric {W : Type u_1} (p q : Core.Presupposition.PrProp W) (w : W) : (p.orFilter q).presup w = (q.orFilter p).presup w

orFilter is inherently symmetric for presupposition projection.

This is Sharvit's observation that K/P's or does not distinguish left from right.

theorem Semantics.Conditionals.Presuppositional.kpstar_presup_implies_kp_presup {W : Type u_1} [DecidableEq W] (closer : W → W → W → Bool) (restriction : List W) (p q : Core.Presupposition.PrProp W) (w : W) (hp : p.assertion w = true) (hw : w ∈ closB closer restriction (List.filter p.assertion restriction) w) : (ifPresup closer restriction p q).presup w = true → (ifKP restriction p q).presup w = true

K/P*'s inner presupposition (CLOS) entails K/P's inner presupposition (local) when the evaluation world is in CLOS.

If CLOS-closest p-worlds all satisfy q.presup (K/P* condition), and w is among them (hw), then q.presup w = true — which is what K/P checks locally.

The hypothesis hw holds automatically with trivial similarity when w ∈ restriction and p.assertion w = true, since trivialCloser never dominates any world. Without it, the theorem is false: a non-trivial ordering can exclude w from CLOS even when p(w) = true.

theorem Semantics.Conditionals.Presuppositional.kp_presup_does_not_imply_kpstar : ∃ (W : Type) (x : DecidableEq W) (restriction : List W) (p : Core.Presupposition.PrProp W) (q : Core.Presupposition.PrProp W) (w : W), (ifKP restriction p q).presup w = true ∧ (ifPresup trivialCloser restriction p q).presup w = false

The converse fails: K/P's local presupposition does NOT entail K/P*'s global CLOS presupposition. This is the Rooth-Partee gap.

Witness: w₀ where p is false and q.presup holds (K/P vacuously satisfied), but some p-world w₁ has q.presup = false (K/P* fails globally).