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 Phenomena.Presupposition.Studies.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

instance Phenomena.Presupposition.Studies.Sharvit2025.instDecidableEqW : DecidableEq W

Equations

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

def Phenomena.Presupposition.Studies.Sharvit2025.instReprW.repr : W → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.Sharvit2025.instReprW : Repr W

Equations

• Phenomena.Presupposition.Studies.Sharvit2025.instReprW = { reprPrec := Phenomena.Presupposition.Studies.Sharvit2025.instReprW.repr }

instance Phenomena.Presupposition.Studies.Sharvit2025.instInhabitedW : Inhabited W

Equations

• Phenomena.Presupposition.Studies.Sharvit2025.instInhabitedW = { default := Phenomena.Presupposition.Studies.Sharvit2025.instInhabitedW.default }

def Phenomena.Presupposition.Studies.Sharvit2025.instInhabitedW.default : W

Equations

• Phenomena.Presupposition.Studies.Sharvit2025.instInhabitedW.default = Phenomena.Presupposition.Studies.Sharvit2025.W.pennyNotLend

def Phenomena.Presupposition.Studies.Sharvit2025.allWorlds : List W

All worlds in the model.

Equations

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

theorem Phenomena.Presupposition.Studies.Sharvit2025.allWorlds_complete (w : W) : w ∈ allWorlds

def Phenomena.Presupposition.Studies.Sharvit2025.hasMoney : BProp W

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

Equations

• Phenomena.Presupposition.Studies.Sharvit2025.hasMoney Phenomena.Presupposition.Studies.Sharvit2025.W.proudNotLend = true
• Phenomena.Presupposition.Studies.Sharvit2025.hasMoney Phenomena.Presupposition.Studies.Sharvit2025.W.proudLend = true
• Phenomena.Presupposition.Studies.Sharvit2025.hasMoney x✝ = false

def Phenomena.Presupposition.Studies.Sharvit2025.penniless : BProp W

"Mia is penniless" — presuppositionless.

Equations

• Phenomena.Presupposition.Studies.Sharvit2025.penniless Phenomena.Presupposition.Studies.Sharvit2025.W.pennyNotLend = true
• Phenomena.Presupposition.Studies.Sharvit2025.penniless Phenomena.Presupposition.Studies.Sharvit2025.W.pennyLend = true
• Phenomena.Presupposition.Studies.Sharvit2025.penniless x✝ = false

def Phenomena.Presupposition.Studies.Sharvit2025.proudOfMoney : Core.Presupposition.PrProp W

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

Equations

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

def Phenomena.Presupposition.Studies.Sharvit2025.shouldntLend : Core.Presupposition.PrProp W

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

Equations

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

def Phenomena.Presupposition.Studies.Sharvit2025.pennilessPr : Core.Presupposition.PrProp W

Presuppositionless version of penniless as PrProp.

Equations

• Phenomena.Presupposition.Studies.Sharvit2025.pennilessPr = Core.Presupposition.PrProp.ofBProp Phenomena.Presupposition.Studies.Sharvit2025.penniless

theorem Phenomena.Presupposition.Studies.Sharvit2025.penniless_entails_no_money (w : W) : penniless w = true → hasMoney w = false

Penniless entails ¬hasMoney: the presuppositions conflict.

theorem Phenomena.Presupposition.Studies.Sharvit2025.orFilter_undefined_at_penny : (pennilessPr.orFilter proudOfMoney).presup W.pennyNotLend = false

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 Phenomena.Presupposition.Studies.Sharvit2025.orFilter_defined_at_proud : (pennilessPr.orFilter proudOfMoney).presup W.proudNotLend = true

The disjunction IS defined at proud-worlds.

def Phenomena.Presupposition.Studies.Sharvit2025.existReading_KP : Core.Presupposition.PrProp W

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

Equations

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

def Phenomena.Presupposition.Studies.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 Phenomena.Presupposition.Studies.Sharvit2025.kp_exist_undefined_at_penny : existReading_KP.presup W.pennyNotLend = false ∧ existReading_KP.presup W.pennyLend = false

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

theorem Phenomena.Presupposition.Studies.Sharvit2025.kp_exist_defined_at_proud : existReading_KP.presup W.proudNotLend = true ∧ existReading_KP.presup W.proudLend = true

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

theorem Phenomena.Presupposition.Studies.Sharvit2025.kp_forall_first_cond_always_defined (w : W) : (Semantics.Conditionals.Presuppositional.ifKP allWorlds pennilessPr shouldntLend).presup w = true

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

theorem Phenomena.Presupposition.Studies.Sharvit2025.kp_forall_presup_eq_hasMoney (w : W) : forallReading_KP.presup w = hasMoney w

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

theorem Phenomena.Presupposition.Studies.Sharvit2025.kp_exist_assertion_excludes_penny : existReading_KP.presup W.proudNotLend = true ∧ (Semantics.Conditionals.Presuppositional.ifKP allWorlds pennilessPr shouldntLend).presup W.proudNotLend = true

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

def Phenomena.Presupposition.Studies.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 Phenomena.Presupposition.Studies.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 Phenomena.Presupposition.Studies.Sharvit2025.kpstar_penniless_always_defined (w : W) : cond_penniless.presup w = true

K/P* conditional with penniless: always defined.

theorem Phenomena.Presupposition.Studies.Sharvit2025.kpstar_proud_presup_eq_hasMoney (w : W) : cond_proud.presup w = hasMoney w

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

def Phenomena.Presupposition.Studies.Sharvit2025.existReading_KPstar : Core.Presupposition.PrProp W

K/P* ∃-reading.

Equations

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

def Phenomena.Presupposition.Studies.Sharvit2025.forallReading_KPstar : Core.Presupposition.PrProp W

K/P* ∀-reading.

Equations

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

theorem Phenomena.Presupposition.Studies.Sharvit2025.kpstar_exist_presup_eq (w : W) : existReading_KPstar.presup w = hasMoney w

Both K/P* readings have presupposition = hasMoney.

theorem Phenomena.Presupposition.Studies.Sharvit2025.kpstar_forall_presup_eq (w : W) : forallReading_KPstar.presup w = hasMoney w

theorem Phenomena.Presupposition.Studies.Sharvit2025.kpstar_assertions_agree (w : W) : existReading_KPstar.assertion w = forallReading_KPstar.assertion w

Both K/P* readings have identical assertions.

theorem Phenomena.Presupposition.Studies.Sharvit2025.kpstar_strawson_equiv : existReading_KPstar.strawsonEquiv forallReading_KPstar

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

theorem Phenomena.Presupposition.Studies.Sharvit2025.kp_exist_presup_eq (w : W) : existReading_KP.presup w = hasMoney w

theorem Phenomena.Presupposition.Studies.Sharvit2025.kp_orFilter_undefined_at_penny : (pennilessPr.orFilter proudOfMoney).presup W.pennyNotLend = false