Exhaustifying a disjunction with a conjunctive disjunct

A disjunction (a ∧ b) ∨ c strengthens under innocent exclusion, against its substitution alternatives — the connective replacements and the subconstituents — to its strongly exhaustive reading (a ∧ b ∧ ¬c) ∨ (c ∧ ¬a ∧ ¬b), each disjunct exclusive of the material of the other. With that reading, the second premise a of the illusory inference from disjunction makes its conclusion b classically valid: the scalar-implicature route to the illusion. Against the four-member Sauerland set the strengthening does not arise — innocent exclusion only denies the conjunction of the disjuncts — so the subconstituent alternatives are load-bearing.

References

• [Spe07b]
• [Sau04]
• [SMM22]
• [BPCM22]

def Exhaustification.conjDisjAlternatives {W : Type u_1} (a b c : Set W) : Set (Set W)

The alternatives of (a ∧ b) ∨ c by substitution of connectives and of subconstituents.

Equations

• Exhaustification.conjDisjAlternatives a b c = {a ∩ b ∪ c, a ∩ b ∩ c, a ∪ c, b ∪ c, a ∩ c, b ∩ c, a ∩ b, a, b, c}

theorem Exhaustification.exhIE_conjDisjAlternatives {W : Type u_1} {a b c : Set W} (hab : ((a ∩ b) \ c).Nonempty) (hc : (c \ (a ∪ b)).Nonempty) : exhIE (conjDisjAlternatives a b c) (a ∩ b ∪ c) = (a ∩ b) \ c ∪ c \ (a ∪ b)

Exhaustifying (a ∧ b) ∨ c against its substitution alternatives yields the strongly exhaustive reading (a ∧ b ∧ ¬c) ∨ (c ∧ ¬a ∧ ¬b), given a world of each disjunct without the other.

theorem Exhaustification.stronglyExhaustive_inter_subset {W : Type u_1} {a b c : Set W} : ((a ∩ b) \ c ∪ c \ (a ∪ b)) ∩ a ⊆ b

With the strongly exhaustive reading, the conclusion of the illusory inference follows classically from the second premise.