Rooth-Partee Conditionals: Empirical Data

@cite{sharvit-2025} @cite{rooth-partee-1982}Theory-neutral data for @cite{sharvit-2025} "Rooth-Partee Conditionals."

The puzzle

(85) "If Mia is penniless or proud of her money, Sue shouldn't lend her any."

Two readings:

• (86a) if-over-∃: If [penniless ∨ proud-of-money], shouldn't-lend. Single conditional with disjunctive antecedent.

• (86b) ∀-over-if: For each P ∈ {penniless, proud-of-money}: if P(m), shouldn't-lend. Conjunction of two conditionals.

"Proud of her money" presupposes "Mia has money." Empirically the readings are Strawson-equivalent — speakers cannot distinguish them. Under K/P (material conditional filtering) they are NOT Strawson-equivalent because or^{K/P}(penniless, proud) is undefined at penniless-worlds, causing those worlds to drop from the ∃-reading's quantification domain.

inductive Sharvit2025.W : Type

Worlds for sentence (85). Cross-product of Mia's financial status (penniless vs has-money-and-proud) with whether Sue lends.

• pennyNotLend : W
• pennyLend : W
• proudNotLend : W
• proudLend : W

@[implicit_reducible]

instance Sharvit2025.instDecidableEqW : DecidableEq W

Equations

• Sharvit2025.instDecidableEqW x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Sharvit2025.instReprW : Repr W

Equations

• Sharvit2025.instReprW = { reprPrec := Sharvit2025.instReprW.repr }

def Sharvit2025.instReprW.repr : W → ℕ → Std.Format

Equations

• Sharvit2025.instReprW.repr Sharvit2025.W.pennyNotLend prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sharvit2025.W.pennyNotLend")).group prec✝
• Sharvit2025.instReprW.repr Sharvit2025.W.pennyLend prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sharvit2025.W.pennyLend")).group prec✝
• Sharvit2025.instReprW.repr Sharvit2025.W.proudNotLend prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sharvit2025.W.proudNotLend")).group prec✝
• Sharvit2025.instReprW.repr Sharvit2025.W.proudLend prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sharvit2025.W.proudLend")).group prec✝

def Sharvit2025.instInhabitedW.default : W

Equations

• Sharvit2025.instInhabitedW.default = Sharvit2025.W.pennyNotLend

@[implicit_reducible]

instance Sharvit2025.instInhabitedW : Inhabited W

Equations

• Sharvit2025.instInhabitedW = { default := Sharvit2025.instInhabitedW.default }

def Sharvit2025.allWorlds : List W

All worlds in the model.

Equations

• Sharvit2025.allWorlds = [Sharvit2025.W.pennyNotLend, Sharvit2025.W.pennyLend, Sharvit2025.W.proudNotLend, Sharvit2025.W.proudLend]

theorem Sharvit2025.allWorlds_complete (w : W) : w ∈ allWorlds

def Sharvit2025.hasMoney : W → Prop

"Mia has money" — the presupposition of "proud of her money."

Equations

• Sharvit2025.hasMoney Sharvit2025.W.proudNotLend = True
• Sharvit2025.hasMoney Sharvit2025.W.proudLend = True
• Sharvit2025.hasMoney x✝ = False

@[implicit_reducible]

instance Sharvit2025.instDecidablePredWHasMoney : DecidablePred hasMoney

Equations

• Sharvit2025.instDecidablePredWHasMoney Sharvit2025.W.proudNotLend = isTrue trivial
• Sharvit2025.instDecidablePredWHasMoney Sharvit2025.W.proudLend = isTrue trivial
• Sharvit2025.instDecidablePredWHasMoney Sharvit2025.W.pennyNotLend = isFalse Sharvit2025.instDecidablePredWHasMoney._proof_1
• Sharvit2025.instDecidablePredWHasMoney Sharvit2025.W.pennyLend = isFalse Sharvit2025.instDecidablePredWHasMoney._proof_2

def Sharvit2025.penniless : W → Prop

"Mia is penniless" — presuppositionless.

Equations

• Sharvit2025.penniless Sharvit2025.W.pennyNotLend = True
• Sharvit2025.penniless Sharvit2025.W.pennyLend = True
• Sharvit2025.penniless x✝ = False

@[implicit_reducible]

instance Sharvit2025.instDecidablePredWPenniless : DecidablePred penniless

Equations

• Sharvit2025.instDecidablePredWPenniless Sharvit2025.W.pennyNotLend = isTrue trivial
• Sharvit2025.instDecidablePredWPenniless Sharvit2025.W.pennyLend = isTrue trivial
• Sharvit2025.instDecidablePredWPenniless Sharvit2025.W.proudNotLend = isFalse Sharvit2025.instDecidablePredWPenniless._proof_1
• Sharvit2025.instDecidablePredWPenniless Sharvit2025.W.proudLend = isFalse Sharvit2025.instDecidablePredWPenniless._proof_2

def Sharvit2025.proudOfMoney : Core.Presupposition.PrProp W

"Mia is proud of her money" — presupposes hasMoney.

Equations

• Sharvit2025.proudOfMoney = { presup := Sharvit2025.hasMoney, assertion := fun (w : Sharvit2025.W) => w = Sharvit2025.W.proudNotLend ∨ w = Sharvit2025.W.proudLend }

@[implicit_reducible]

instance Sharvit2025.proudOfMoney_decAssertion : DecidablePred proudOfMoney.assertion

Equations

• Sharvit2025.proudOfMoney_decAssertion = id fun (w : Sharvit2025.W) => inferInstance

def Sharvit2025.shouldntLend : Core.Presupposition.PrProp W

"Sue shouldn't lend Mia any money" — presuppositionless.

Equations

• Sharvit2025.shouldntLend = { presup := fun (x : Sharvit2025.W) => True, assertion := fun (w : Sharvit2025.W) => w = Sharvit2025.W.pennyNotLend ∨ w = Sharvit2025.W.proudNotLend }

@[implicit_reducible]

instance Sharvit2025.shouldntLend_decAssertion : DecidablePred shouldntLend.assertion

Equations

• Sharvit2025.shouldntLend_decAssertion = id fun (w : Sharvit2025.W) => inferInstance

def Sharvit2025.pennilessPr : Core.Presupposition.PrProp W

Presuppositionless version of penniless as PrProp.

Equations

• Sharvit2025.pennilessPr = Core.Presupposition.PrProp.ofProp' Sharvit2025.penniless

@[implicit_reducible]

instance Sharvit2025.pennilessPr_decAssertion : DecidablePred pennilessPr.assertion

Equations

• Sharvit2025.pennilessPr_decAssertion = id (id fun (w : Sharvit2025.W) => inferInstance)

theorem Sharvit2025.penniless_entails_no_money (w : W) : penniless w → ¬hasMoney w

Penniless entails ¬hasMoney: the presuppositions conflict.

theorem Sharvit2025.orFilter_undefined_at_penny : ¬(pennilessPr.orFilter proudOfMoney).presup W.pennyNotLend

The disjunction "penniless or proud" under orFilter is UNDEFINED at penniless-worlds. This is the root cause of K/P's failure: orFilter's filtering condition requires "proud of money" to be defined when "penniless" is true, but penniless entails ¬hasMoney.

theorem Sharvit2025.orFilter_defined_at_proud : (pennilessPr.orFilter proudOfMoney).presup W.proudNotLend

The disjunction IS defined at proud-worlds.

@[implicit_reducible]

instance Sharvit2025.orFilter_decAssertion : DecidablePred (pennilessPr.orFilter proudOfMoney).assertion

Equations

• Sharvit2025.orFilter_decAssertion w = id (id (id (id inferInstance)))

def Sharvit2025.existReading_KP : Core.Presupposition.PrProp W

Under K/P, the ∃-reading uses orFilter for the antecedent disjunction.

Equations

• Sharvit2025.existReading_KP = Semantics.Conditionals.Presupposition.ifKP Sharvit2025.allWorlds (Sharvit2025.pennilessPr.orFilter Sharvit2025.proudOfMoney) Sharvit2025.shouldntLend

def Sharvit2025.forallReading_KP : Core.Presupposition.PrProp W

Under K/P, the ∀-reading is the conjunction of two K/P conditionals.

Equations

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

theorem Sharvit2025.kp_exist_undefined_at_penny : ¬existReading_KP.presup W.pennyNotLend ∧ ¬existReading_KP.presup W.pennyLend

K/P ∃-reading is UNDEFINED at penniless-worlds.

theorem Sharvit2025.kp_exist_defined_at_proud : existReading_KP.presup W.proudNotLend ∧ existReading_KP.presup W.proudLend

K/P ∃-reading IS defined at proud-worlds.

theorem Sharvit2025.kp_forall_first_cond_always_defined (w : W) : (Semantics.Conditionals.Presupposition.ifKP allWorlds pennilessPr shouldntLend).presup w

K/P ∀-reading: the first conditional (if penniless, shouldntLend) is always defined.

theorem Sharvit2025.kp_forall_presup_eq_hasMoney (w : W) : forallReading_KP.presup w ↔ hasMoney w

K/P ∀-reading presup = hasMoney (from the second conditional).

theorem Sharvit2025.kp_exist_assertion_excludes_penny : existReading_KP.presup W.proudNotLend ∧ (Semantics.Conditionals.Presupposition.ifKP allWorlds pennilessPr shouldntLend).presup W.proudNotLend

K/P ∃-reading assertion excludes penny-worlds from quantification.

@[implicit_reducible]

instance Sharvit2025.instDecidablePredWDefinedFalsePennilessPr : DecidablePred (Semantics.Conditionals.Presupposition.definedFalse pennilessPr)

Equations

• Sharvit2025.instDecidablePredWDefinedFalsePennilessPr w = id (id (id inferInstance))

@[implicit_reducible]

instance Sharvit2025.instDecidablePredWDefinedFalseProudOfMoney : DecidablePred (Semantics.Conditionals.Presupposition.definedFalse proudOfMoney)

Equations

• Sharvit2025.instDecidablePredWDefinedFalseProudOfMoney w = id (id inferInstance)

def Sharvit2025.cond_penniless : Core.Presupposition.PrProp W

K/P* conditional: if penniless, shouldntLend.

Equations

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

def Sharvit2025.cond_proud : Core.Presupposition.PrProp W

K/P* conditional: if proud-of-money, shouldntLend.

Equations

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

theorem Sharvit2025.kpstar_penniless_always_defined (w : W) : cond_penniless.presup w

K/P* conditional with penniless: always defined.

theorem Sharvit2025.kpstar_proud_presup_eq_hasMoney (w : W) : cond_proud.presup w ↔ hasMoney w

K/P* conditional with proud-of-money: defined iff hasMoney.

@[implicit_reducible]

instance Sharvit2025.cond_penniless_decAssertion : DecidablePred cond_penniless.assertion

Equations

• Sharvit2025.cond_penniless_decAssertion w = id (id inferInstance)

@[implicit_reducible]

instance Sharvit2025.orPresup_decAssertion : DecidablePred (Semantics.Conditionals.Presupposition.orPresup Semantics.Conditionals.Presupposition.trivialCloser allWorlds pennilessPr proudOfMoney).assertion

Equations

• Sharvit2025.orPresup_decAssertion w = id (id (id (id inferInstance)))

@[implicit_reducible]

instance Sharvit2025.orPresup_defFalse_dec : DecidablePred (Semantics.Conditionals.Presupposition.definedFalse (Semantics.Conditionals.Presupposition.orPresup Semantics.Conditionals.Presupposition.trivialCloser allWorlds pennilessPr proudOfMoney))

Equations

• Sharvit2025.orPresup_defFalse_dec w = id (id (id (id (id inferInstance))))

def Sharvit2025.existReading_KPstar : Core.Presupposition.PrProp W

K/P* ∃-reading.

Equations

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

def Sharvit2025.forallReading_KPstar : Core.Presupposition.PrProp W

K/P* ∀-reading.

Equations

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

theorem Sharvit2025.kpstar_exist_presup_eq (w : W) : existReading_KPstar.presup w ↔ hasMoney w

Both K/P* readings have presupposition = hasMoney.

theorem Sharvit2025.kpstar_forall_presup_eq (w : W) : forallReading_KPstar.presup w ↔ hasMoney w

theorem Sharvit2025.kpstar_assertions_agree (w : W) : existReading_KPstar.assertion w ↔ forallReading_KPstar.assertion w

Both K/P* readings have identical assertions.

theorem Sharvit2025.kpstar_strawson_equiv : existReading_KPstar.strawsonEquiv forallReading_KPstar

Strawson equivalence of ∃ and ∀ readings under K/P*.

theorem Sharvit2025.kp_exist_presup_eq (w : W) : existReading_KP.presup w ↔ hasMoney w

theorem Sharvit2025.kp_orFilter_undefined_at_penny : ¬(pennilessPr.orFilter proudOfMoney).presup W.pennyNotLend