Spector (2016): Comparing Exhaustivity Operators

This file formalizes the worked cases of [Spe16], which compares the exhaustivity operator based on minimal worlds, exhMW, with the operator of [Fox07] based on innocent exclusion, exhIE. The paper's general results live in the substrate: the minimal-world operator entails the innocent-exclusion operator, an alternative is innocently excludable exactly when the minimal worlds falsify it, closing the alternatives under conjunction makes the two operators coincide (exhMW_eq_exhIE_of_infClosed), and closing them under disjunction changes neither (exhIE_sUnion_image_powerset). Here are the illustrations and the practical consequences. With a single alternative the operators agree (elementary). For a disjunction with only its disjuncts as alternatives, the minimal-world operator returns the exclusive reading while innocent exclusion is vacuous (exhMW_or, exhIE_or); adding the conjunction as an alternative leaves the order on worlds, and so the minimal worlds, unchanged (leALT_or_and_iff) and makes innocent exclusion exclusive too (exhIE_or_and). The paper's shortcut for computing innocent exclusion over a large alternative set, running the minimal-world operator over the elementary propositions instead, is illustrated on either Mary came, or both Peter and Sue did (exhMW_or_and_three). Finally, a vacuous minimal-world operator makes innocent exclusion vacuous (exhIE_eq_of_exhMW_eq), which settles the infinite case of there are at least n stars against the alternatives exactly m and at least m for every m ([Sch13]): every world with at least n stars, or infinitely many, is minimal (exhMW_stars, exhIE_stars).

Implementation notes

The third operator the paper compares, which denies every non-entailed alternative, and the theorem that innocent exclusion over the alternatives of [Sau04] equals the minimal-world operator over the elementary sentences are not formalized; the shortcut is shown by computing the minimal worlds directly. Independence of the disjuncts is the existence of a world verifying one disjunct alone, assumed only where a case needs it. The alternative sets of the illustrations are the paper's, without the prejacent, which the substrate's compatible sets carry separately.

References

• [Spe16]
• [Fox07]
• [Sau04]
• [Sch13]

The elementary case

theorem Spector2016.exhMW_pair {World : Type u_1} {φ ψ : Set World} (hne : (φ \ ψ).Nonempty) : Exhaustification.exhMW {φ, ψ} φ = φ \ ψ

With one alternative some prejacent world falsifies, the minimal worlds are the prejacent worlds falsifying it.

theorem Spector2016.elementary {World : Type u_1} {φ ψ : Set World} (hne : (φ \ ψ).Nonempty) : Exhaustification.exhMW {φ, ψ} φ = φ \ ψ ∧ Exhaustification.exhIE {φ, ψ} φ = φ \ ψ

In the elementary case both operators deny the single alternative.

Disjunction with and without a conjunctive alternative

theorem Spector2016.exhMW_or {World : Type u_1} {A B : Set World} (hA : (A \ B).Nonempty) : Exhaustification.exhMW {A, B} (A ∪ B) = A \ B ∪ B \ A

Against the disjuncts alone, the minimal worlds of a disjunction are those verifying exactly one disjunct, the exclusive reading.

theorem Spector2016.exhIE_or {World : Type u_1} {A B : Set World} (hA : (A \ B).Nonempty) (hB : (B \ A).Nonempty) : Exhaustification.exhIE {A, B} (A ∪ B) = A ∪ B

Against the disjuncts alone, innocent exclusion is vacuous, since each disjunct is verified by some minimal world, so neither is innocently excludable.

theorem Spector2016.exhMW_congr {World : Type u_1} {ALT ALT' : Set (Set World)} (φ : Set World) (h : ∀ (u v : World), Exhaustification.leALT ALT u v ↔ Exhaustification.leALT ALT' u v) : Exhaustification.exhMW ALT φ = Exhaustification.exhMW ALT' φ

Minimal worlds depend only on the preorder the alternatives induce.

theorem Spector2016.leALT_or_and_iff {World : Type u_1} {A B : Set World} (u v : World) : Exhaustification.leALT {A, B, A ∩ B} u v ↔ Exhaustification.leALT {A, B} u v

Adding the conjunction as an alternative leaves the order on worlds unchanged, since it holds exactly where both disjuncts do.

theorem Spector2016.exhMW_or_and {World : Type u_1} {A B : Set World} (hA : (A \ B).Nonempty) : Exhaustification.exhMW {A, B, A ∩ B} (A ∪ B) = A \ B ∪ B \ A

With the conjunction among the alternatives the minimal worlds are as before.

theorem Spector2016.exhIE_or_and {World : Type u_1} {A B : Set World} (hA : (A \ B).Nonempty) (hB : (B \ A).Nonempty) : Exhaustification.exhIE {A, B, A ∩ B} (A ∪ B) = A \ B ∪ B \ A

With the conjunction among the alternatives innocent exclusion denies it, and the two operators agree on the exclusive reading.

The shortcut

theorem Spector2016.exhMW_or_and_three {World : Type u_1} {m p s : Set World} (hm : ∃ w ∈ m, w ∉ p ∧ w ∉ s) : Exhaustification.exhMW {m, p, s} (m ∪ p ∩ s) = m \ (p ∪ s) ∪ (p ∩ s) \ m

For Either Mary came, or both Peter and Sue did, over the elementary alternatives the minimal worlds are those where only Mary came and those where Peter and Sue came without Mary, which by the paper's results is what innocent exclusion returns over the full alternative set.

Infinitely many alternatives

theorem Spector2016.exhIE_eq_of_exhMW_eq {World : Type u_1} {ALT : Set (Set World)} {φ : Set World} (h : Exhaustification.exhMW ALT φ = φ) : Exhaustification.exhIE ALT φ = φ

A vacuous minimal-world operator makes innocent exclusion vacuous.

@[reducible, inline]

abbrev Spector2016.Stars : Type

Worlds with a number of stars, or infinitely many.

Equations

• Spector2016.Stars = WithTop ℕ

def Spector2016.exactly (n : ℕ) : Set Stars

There are exactly n stars.

Equations

• Spector2016.exactly n = {w : Spector2016.Stars | w = ↑n}

def Spector2016.atLeast (n : ℕ) : Set Stars

There are at least n stars.

Equations

• Spector2016.atLeast n = {w : Spector2016.Stars | ↑n ≤ w}

def Spector2016.starsALT : Set (Set Stars)

The alternatives of at least n are every exactly m and every at least m.

Equations

• Spector2016.starsALT = Set.range Spector2016.exactly ∪ Set.range Spector2016.atLeast

theorem Spector2016.eq_of_leALT_stars {u v : Stars} (h : Exhaustification.leALT starsALT u v) : u = v

No world verifies strictly fewer of these alternatives than another, since exactly n holds only at the n-star world, and every at least m holds only at the world with infinitely many stars.

theorem Spector2016.exhMW_stars (n : ℕ) : Exhaustification.exhMW starsALT (atLeast n) = atLeast n

Every world verifying at least n is minimal, so the operator is vacuous.

theorem Spector2016.exhIE_stars (n : ℕ) : Exhaustification.exhIE starsALT (atLeast n) = atLeast n

And so is innocent exclusion, without computing a maximal compatible set.