Sharvit (2025): Rooth-Partee Conditionals and the Symmetry of Disjunction

This file formalizes the paper's case that or is inherently symmetric and its closest-worlds theory of the connectives. A Rooth-Partee conditional, If Mia is penniless or proud of her money, then Sue is, has an if-over-∃ reading, one conditional with a disjunctive antecedent, and a ∀-over-if reading, one conditional per disjunct with the ellipsis matched to it; the second reading presupposes that Sue has money if Mia does, and both readings survive swapping the disjuncts. A disjunction that projects its left disjunct's presupposition, the K+ connective under CON-asymmetry (16)–(17), cannot deliver this: swapping the disjuncts changes what the antecedent presupposes (orAsym_notAtIssue_ne), and the paper argues that accommodation does not repair it. Karttunen and Peters's symmetric disjunction (102) does (TwoDim.orKPSymmetric_comm), but its Karttunen conditional presupposition, the consequent's presupposition at the evaluation world if the antecedent is true there (100), is too weak for the ∀-over-if presupposition (ifKP_notAtIssue_of_not_atIssue), the Proviso Problem.

The proposal replaces the local presupposition by a closest-worlds one after Heim: a conditional presupposes its consequent's presupposition at the closest antecedent-worlds of the epistemic state (119), and conjunction and disjunction inherit the condition (127)–(128) (clos, ifKPstar, andKPstar, orKPstar, symmetric by construction, orKPstar_comm). A closest-worlds presupposition strengthens to an unconditional one wherever the laws in force allow the antecedent without it (presup_strengthens, the reasoning of (122)). For the ∀-over-if reading the conditional must quantify over the properties the antecedent disjoins (142), since a conditional over the disjunction itself checks only the closest disjunction-worlds and can miss a disjunct altogether (kpstarForallOverIf_notAtIssue_of_closest, the paper's Scenario I). The K/P** readings (143) come out as the paper states them (ifOverExists_atIssue, forallOverIf_notAtIssue, forallOverIf_atIssue), are invariant under swapping the disjuncts (forallOverIf_comm), and for Mia and Sue the ∀-over-if reading presupposes that Sue has money at the closest worlds where Mia is proud of hers (roothPartee_notAtIssue), which strengthens to if Mia has money, Sue has money (roothPartee_notAtIssue_strengthens). Under a strict conditional the ∀-over-if reading entails the if-over-∃ reading, the asymmetry of the responses (33) (forallOverIf_imp_ifOverExists).

Implementation notes

• Meanings are two-dimensional in Karttunen and Peters's way, an at-issue proposition paired with a presupposition (ConventionalImplicature.TwoDim), since the K/P connectives read a constituent's at-issue content where its presupposition fails; a property gives such a meaning for each individual (Property).
• The defined negation of a disjunct in (128) is read as presupposition-free (definedFalse); read as domain-restricted, the disjunction would presuppose both disjuncts' presuppositions at the evaluation world, against (134)–(135).
• The epistemic state EP and the similarity ordering the context supplies are parameters; the Limit Assumption built into CLOS (120) is not needed for the theorems stated.
• The type-flexible connectives are given at the two types the paper uses. The structured-proposition extension (153)–(157), the Cooperative Principle (123)–(124), and accommodation as conjunction are not formalized.

References

• [Sha25]
• [RP82]
• [KP79]
• [Hei92]

CON-asymmetry and the symmetry of or

def Sharvit2025.orAsym {W : Type u_1} (p q : ConventionalImplicature.TwoDim W (W → Prop)) : ConventionalImplicature.TwoDim W (W → Prop)

The K+ disjunction under CON-asymmetry (16c), (17), which presupposes exactly what its left disjunct presupposes.

Equations

• Sharvit2025.orAsym p q = { atIssue := p.atIssue ⊔ q.atIssue, notAtIssue := p.notAtIssue }

theorem Sharvit2025.orAsym_notAtIssue_ne {W : Type u_1} {p q : ConventionalImplicature.TwoDim W (W → Prop)} {w : W} (hp : p.notAtIssue w) (hq : ¬q.notAtIssue w) : (orAsym p q).notAtIssue w ∧ ¬(orAsym q p).notAtIssue w

Swapping the disjuncts of an asymmetric disjunction changes its presupposition wherever the disjuncts differ in it, so the LFs (62) and (64) are not equivalent.

Karttunen's conditional presupposition and the closest-worlds one

def Sharvit2025.ifKP {W : Type u_1} (EP : Set W) (p q : ConventionalImplicature.TwoDim W (W → Prop)) : ConventionalImplicature.TwoDim W (W → Prop)

The K/P conditional (100) presupposes the antecedent's presupposition, and the consequent's at the evaluation world if the antecedent is true there, and asserts that every antecedent-world of the epistemic state is a consequent-world.

Equations

• Sharvit2025.ifKP EP p q = { atIssue := fun (x : W) => ∀ w' ∈ EP, p.atIssue w' → q.atIssue w', notAtIssue := fun (w : W) => p.notAtIssue w ∧ (p.atIssue w → q.notAtIssue w) }

theorem Sharvit2025.ifKP_notAtIssue_of_not_atIssue {W : Type u_1} (EP : Set W) {p : ConventionalImplicature.TwoDim W (W → Prop)} (q : ConventionalImplicature.TwoDim W (W → Prop)) {w : W} (hp : p.notAtIssue w) (h : ¬p.atIssue w) : (ifKP EP p q).notAtIssue w

Where the antecedent is false, the K/P conditional presupposes nothing of its consequent, which is why the Proviso Problem finds its conditional presupposition too weak.

def Sharvit2025.clos {W : Type u_1} (EP : Set W) (sim : W → Preorder W) (w : W) (Y : Set W) : Set W

The closest worlds to w among the Y-worlds of the epistemic state, under the similarity ordering the context supplies (CLOS, (120)).

Equations

• Sharvit2025.clos EP sim w Y = (sim w).minimals (Y ∩ EP)

theorem Sharvit2025.clos_subset {W : Type u_1} (EP : Set W) (sim : W → Preorder W) (w : W) (Y : Set W) : clos EP sim w Y ⊆ Y

def Sharvit2025.ifKPstar {W : Type u_1} (EP : Set W) (sim : W → Preorder W) (p q : ConventionalImplicature.TwoDim W (W → Prop)) : ConventionalImplicature.TwoDim W (W → Prop)

The K/P* conditional (119) presupposes the antecedent's presupposition and the consequent's at the closest antecedent-worlds, and asserts that those are consequent-worlds.

Equations

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

def Sharvit2025.andKPstar {W : Type u_1} (EP : Set W) (sim : W → Preorder W) (p q : ConventionalImplicature.TwoDim W (W → Prop)) : ConventionalImplicature.TwoDim W (W → Prop)

The K/P* conjunction (127) presupposes the first conjunct's presupposition, and the second's at the evaluation world or at the closest worlds where the first is true.

Equations

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

def Sharvit2025.definedFalse {W : Type u_1} (p : ConventionalImplicature.TwoDim W (W → Prop)) : ConventionalImplicature.TwoDim W (W → Prop)

The presupposition-free proposition that p's presupposition holds and its at-issue content is false.

Equations

• Sharvit2025.definedFalse p = pure fun (w : W) => p.notAtIssue w ∧ ¬p.atIssue w

def Sharvit2025.orKPstar {W : Type u_1} (EP : Set W) (sim : W → Preorder W) (p q : ConventionalImplicature.TwoDim W (W → Prop)) : ConventionalImplicature.TwoDim W (W → Prop)

The K/P* disjunction (128) presupposes that one disjunct's presupposition holds and that each disjunct's defined negation conjoins with the other.

Equations

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

theorem Sharvit2025.orKPstar_notAtIssue {W : Type u_1} (EP : Set W) (sim : W → Preorder W) (p q : ConventionalImplicature.TwoDim W (W → Prop)) (w : W) : (orKPstar EP sim p q).notAtIssue w ↔ (p.notAtIssue w ∨ q.notAtIssue w) ∧ (q.notAtIssue w ∨ clos EP sim w {w' : W | p.notAtIssue w' ∧ ¬p.atIssue w'} ⊆ {w' : W | q.notAtIssue w'}) ∧ (p.notAtIssue w ∨ clos EP sim w {w' : W | q.notAtIssue w' ∧ ¬q.atIssue w'} ⊆ {w' : W | p.notAtIssue w'})

theorem Sharvit2025.orKPstar_comm {W : Type u_1} (EP : Set W) (sim : W → Preorder W) (p q : ConventionalImplicature.TwoDim W (W → Prop)) : orKPstar EP sim p q = orKPstar EP sim q p

The K/P* disjunction is symmetric by construction.

theorem Sharvit2025.presup_strengthens {W : Type u_1} (EP : Set W) (sim : W → Preorder W) {M P Q : Set W} (hlaw : ∀ w ∈ M, w ∉ Q → ¬clos EP sim w P ⊆ Q) (h : ∀ w ∈ M, clos EP sim w P ⊆ Q) (w : W) : w ∈ M → w ∈ Q

A closest-worlds presupposition CLOS_w(P) ⊆ Q holding throughout M strengthens to Q throughout M when the laws in force allow P without Q, so that from a ¬Q-world the closest P-worlds include ¬Q-worlds (122). This dissolves the Proviso Problem.

K/P**: the conditional quantifies over the disjoined properties

@[reducible, inline]

abbrev Sharvit2025.Property (W : Type u_3) (E : Type u_4) : Type (max u_4 u_3)

A property of individuals, a two-dimensional proposition for each individual.

Equations

• Sharvit2025.Property W E = (E → ConventionalImplicature.TwoDim W (W → Prop))

def Sharvit2025.orProps {W : Type u_1} {E : Type u_2} (EP : Set W) (sim : W → Preorder W) (α β : Property W E) (x : E) (Z : Property W E) : ConventionalImplicature.TwoDim W (W → Prop)

The type-flexible disjunction of two properties applied to x (142a), a partial function of properties Z defined for the two disjuncts where the propositional disjunction of the two applied to x is defined, and true of Z when x has Z.

Equations

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

def Sharvit2025.ifProps {W : Type u_1} {E : Type u_2} (EP : Set W) (sim : W → Preorder W) (O₁ O₂ : Property W E → ConventionalImplicature.TwoDim W (W → Prop)) : ConventionalImplicature.TwoDim W (W → Prop)

The type-flexible conditional over property-valued arguments (142b) requires, for every property the antecedent is defined for, that the consequent be defined at the closest antecedent-worlds and hold there.

Equations

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

def Sharvit2025.exists' {W : Type u_1} {E : Type u_2} (O : Property W E → ConventionalImplicature.TwoDim W (W → Prop)) : ConventionalImplicature.TwoDim W (W → Prop)

The existential closure of (144a).

Equations

• Sharvit2025.exists' O = { atIssue := fun (w : W) => ∃ (Z : Sharvit2025.Property W E), (O Z).atIssue w, notAtIssue := fun (w : W) => ∃ (Z : Sharvit2025.Property W E), (O Z).notAtIssue w }

def Sharvit2025.ifOverExists {W : Type u_1} {E : Type u_2} (EP : Set W) (sim : W → Preorder W) (α β : Property W E) (x y : E) : ConventionalImplicature.TwoDim W (W → Prop)

The if-over-∃ LF (143a), in which the conditional takes the existential closures of the disjoined properties applied to x and to y, the ellipsis resolved to the disjunction.

Equations

• Sharvit2025.ifOverExists EP sim α β x y = Sharvit2025.ifKPstar EP sim (Sharvit2025.exists' (Sharvit2025.orProps EP sim α β x)) (Sharvit2025.exists' (Sharvit2025.orProps EP sim α β y))

def Sharvit2025.forallOverIf {W : Type u_1} {E : Type u_2} (EP : Set W) (sim : W → Preorder W) (α β : Property W E) (x y : E) : ConventionalImplicature.TwoDim W (W → Prop)

The ∀-over-if LF (143b), in which the conditional quantifies over the disjoined properties, the ellipsis bound to each in turn.

Equations

• Sharvit2025.forallOverIf EP sim α β x y = Sharvit2025.ifProps EP sim (Sharvit2025.orProps EP sim α β x) fun (Z : Sharvit2025.Property W E) => Z y

theorem Sharvit2025.exists'_orProps_atIssue {W : Type u_1} {E : Type u_2} (EP : Set W) (sim : W → Preorder W) (α β : Property W E) (x : E) (w : W) : (exists' (orProps EP sim α β x)).atIssue w ↔ (α x).atIssue w ∨ (β x).atIssue w

theorem Sharvit2025.ifOverExists_atIssue {W : Type u_1} {E : Type u_2} (EP : Set W) (sim : W → Preorder W) (α β : Property W E) (x y : E) (w : W) : (ifOverExists EP sim α β x y).atIssue w ↔ clos EP sim w {w' : W | (α x).atIssue w' ∨ (β x).atIssue w'} ⊆ {w' : W | (α y).atIssue w' ∨ (β y).atIssue w'}

The if-over-∃ reading asserts that the closest worlds where x has one of the properties are worlds where y has one of them (145b).

theorem Sharvit2025.forallOverIf_notAtIssue {W : Type u_1} {E : Type u_2} (EP : Set W) (sim : W → Preorder W) (α β : Property W E) (x y : E) (w : W) : (forallOverIf EP sim α β x y).notAtIssue w ↔ (orKPstar EP sim (α x) (β x)).notAtIssue w ∧ clos EP sim w {w' : W | (α x).atIssue w'} ⊆ {w' : W | (α y).notAtIssue w'} ∧ clos EP sim w {w' : W | (β x).atIssue w'} ⊆ {w' : W | (β y).notAtIssue w'}

The ∀-over-if reading presupposes the disjunction of the antecedent and, for each disjoined property, that y's having it is defined at the closest worlds where x has it (146a).

theorem Sharvit2025.forallOverIf_atIssue {W : Type u_1} {E : Type u_2} (EP : Set W) (sim : W → Preorder W) (α β : Property W E) (x y : E) (w : W) (h : (orKPstar EP sim (α x) (β x)).notAtIssue w) : (forallOverIf EP sim α β x y).atIssue w ↔ clos EP sim w {w' : W | (α x).atIssue w'} ⊆ {w' : W | (α y).atIssue w'} ∧ clos EP sim w {w' : W | (β x).atIssue w'} ⊆ {w' : W | (β y).atIssue w'}

Where defined, the ∀-over-if reading asserts that, for each disjoined property, the closest worlds where x has it are worlds where y has it (146b).

theorem Sharvit2025.orProps_comm {W : Type u_1} {E : Type u_2} (EP : Set W) (sim : W → Preorder W) (α β : Property W E) (x : E) : orProps EP sim α β x = orProps EP sim β α x

The type-flexible disjunction is symmetric, the K/P* disjunction under it being so.

theorem Sharvit2025.forallOverIf_comm {W : Type u_1} {E : Type u_2} (EP : Set W) (sim : W → Preorder W) (α β : Property W E) (x y : E) : forallOverIf EP sim α β x y = forallOverIf EP sim β α x y

The disjunction being symmetric, If x is P or Q, then y is and If x is Q or P, then y is share their ∀-over-if reading.

theorem Sharvit2025.forallOverIf_imp_ifOverExists {W : Type u_1} {E : Type u_2} (EP : Set W) (sim : W → Preorder W) (hstrict : ∀ (w : W) (Y : Set W), clos EP sim w Y = Y ∩ EP) (α β : Property W E) (x y : E) (w : W) (h : (orKPstar EP sim (α x) (β x)).notAtIssue w) : (forallOverIf EP sim α β x y).atIssue w → (ifOverExists EP sim α β x y).atIssue w

Under a strict conditional, where the closest worlds are all the worlds of the epistemic state, the ∀-over-if reading entails the if-over-∃ reading. The responses (33) show that the converse fails, (33b) denying only the ∀-over-if reading.

Why the conditional must quantify over the disjuncts

def Sharvit2025.matched {W : Type u_1} {E : Type u_2} (α β : Property W E) (x y : E) : ConventionalImplicature.TwoDim W (W → Prop)

The consequent of (136) with the ellipsis resolved by the world-dependent property of (137b), saying that y has whichever disjoined property x has.

Equations

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

def Sharvit2025.kpstarForallOverIf {W : Type u_1} {E : Type u_2} (EP : Set W) (sim : W → Preorder W) (α β : Property W E) (x y : E) : ConventionalImplicature.TwoDim W (W → Prop)

The K/P* attempt at the ∀-over-if reading, (136) with (137b), a conditional over the disjunction itself.

Equations

• Sharvit2025.kpstarForallOverIf EP sim α β x y = Sharvit2025.ifKPstar EP sim (Sharvit2025.orKPstar EP sim (α x) (β x)) (Sharvit2025.matched α β x y)

theorem Sharvit2025.kpstarForallOverIf_notAtIssue_of_closest {W : Type u_1} {E : Type u_2} (EP : Set W) (sim : W → Preorder W) (α β : Property W E) (x y : E) (w : W) (hc : clos EP sim w {w' : W | (α x).atIssue w' ∨ (β x).atIssue w'} ⊆ {w' : W | (α x).atIssue w' ∧ ¬(β x).atIssue w'}) : (kpstarForallOverIf EP sim α β x y).notAtIssue w ↔ (orKPstar EP sim (α x) (β x)).notAtIssue w ∧ clos EP sim w {w' : W | (α x).atIssue w' ∨ (β x).atIssue w'} ⊆ {w' : W | (α y).notAtIssue w'}

When the closest worlds where x has one of the properties are all worlds where x has the first and not the second, as in Scenario I (141), the conditional over the disjunction presupposes nothing about y and the second property, which the ∀-over-if reading requires (146).

Mia and Sue (138)

def Sharvit2025.penniless {W : Type u_1} {E : Type u_2} (hasMoney : W → E → Prop) (x : E) : ConventionalImplicature.TwoDim W (W → Prop)

Penniless (138a), true of x when x has no money.

Equations

• Sharvit2025.penniless hasMoney x = pure fun (w : W) => ¬hasMoney w x

def Sharvit2025.proudOfMoney {W : Type u_1} {E : Type u_2} (hasMoney proudOf : W → E → Prop) (x : E) : ConventionalImplicature.TwoDim W (W → Prop)

Proud of her money (138b), which presupposes that x has money.

Equations

• Sharvit2025.proudOfMoney hasMoney proudOf x = { atIssue := fun (w : W) => proudOf w x, notAtIssue := fun (w : W) => hasMoney w x }

theorem Sharvit2025.orKPstar_penniless_proud {W : Type u_1} {E : Type u_2} (EP : Set W) (sim : W → Preorder W) (hasMoney proudOf : W → E → Prop) (x : E) (w : W) : (orKPstar EP sim (penniless hasMoney x) (proudOfMoney hasMoney proudOf x)).notAtIssue w

The disjunction penniless or proud of her money is presupposition-free, (134a) and (135a).

theorem Sharvit2025.roothPartee_notAtIssue {W : Type u_1} {E : Type u_2} (EP : Set W) (sim : W → Preorder W) (hasMoney proudOf : W → E → Prop) (mia sue : E) (w : W) : (forallOverIf EP sim (penniless hasMoney) (proudOfMoney hasMoney proudOf) mia sue).notAtIssue w ↔ clos EP sim w {w' : W | proudOf w' mia} ⊆ {w' : W | hasMoney w' sue}

The ∀-over-if reading of If Mia is penniless or proud of her money, then Sue is presupposes that Sue has money at the closest worlds where Mia is proud of hers, (146a) for Mia and Sue and (135a-iii) before strengthening.

theorem Sharvit2025.roothPartee_notAtIssue_strengthens {W : Type u_1} {E : Type u_2} (EP : Set W) (sim : W → Preorder W) (hasMoney proudOf : W → E → Prop) (mia sue : E) (hlaw : ∀ w ∈ EP ∩ {w : W | hasMoney w mia}, ¬hasMoney w sue → ¬clos EP sim w {w' : W | proudOf w' mia} ⊆ {w' : W | hasMoney w' sue}) (h : ∀ w ∈ EP, (forallOverIf EP sim (penniless hasMoney) (proudOfMoney hasMoney proudOf) mia sue).notAtIssue w) (w : W) : w ∈ EP ∩ {w : W | hasMoney w mia} → hasMoney w sue

Across the worlds of the epistemic state where Mia has money, if the laws allow Mia to be proud of her money while Sue has none, the reading presupposes that Sue has money, that is, if Mia has money, Sue has money ((146a-II), (135a-iii)).