Exhaustifying a disjunction whose alternatives are its sub-disjunctions

A disjunction ⋃ i ∈ I, p i whose alternatives are disjunctions over subsets of I — sub- disjunctions but no conjunctions — strengthens under exhIEII to their conjunction, provided some world verifies each disjunct alone and some world verifies all of them: nothing is innocently excludable, since a single-disjunct world is minimal, and everything is innocently includable, since the cell is consistent. With all sub-disjunctions present the result is the conjunction of the disjuncts; with only the disjunctions over subsets of size m it is that at least |I| + 1 - m disjuncts hold. This is the generalization behind free choice without a conjunctive alternative and behind the implicature account of homogeneity, where the disjuncts are the atoms of a plurality and pruning to the size-m alternatives gives the non-maximal readings.

References

• [bar-lev-2021]
• [BLF20]

def Exhaustification.subDisj {World : Type u_1} {ι : Type u_2} (p : ι → Set World) (S : Finset ι) : Set World

The disjunction over a subset.

Equations

• Exhaustification.subDisj p S = ⋃ i ∈ S, p i

@[reducible, inline]

abbrev Exhaustification.disj {World : Type u_1} {ι : Type u_2} (I : Finset ι) (p : ι → Set World) : Set World

The disjunction of the family over I.

Equations

• Exhaustification.disj I p = Exhaustification.subDisj p I

def Exhaustification.subDisjs {World : Type u_1} {ι : Type u_2} (I : Finset ι) (p : ι → Set World) : Set (Set World)

The disjunctions over the nonempty subsets of I.

Equations

• Exhaustification.subDisjs I p = {q : Set World | ∃ S ⊆ I, S.Nonempty ∧ q = Exhaustification.subDisj p S}

def Exhaustification.subDisjsOfCard {World : Type u_1} {ι : Type u_2} (I : Finset ι) (p : ι → Set World) (m : ℕ) : Set (Set World)

The disjunction over I together with the disjunctions over its subsets of size m.

Equations

• Exhaustification.subDisjsOfCard I p m = insert (Exhaustification.disj I p) {q : Set World | ∃ S ⊆ I, S.card = m ∧ q = Exhaustification.subDisj p S}

@[simp]

theorem Exhaustification.mem_subDisj {World : Type u_1} {ι : Type u_2} {p : ι → Set World} {S : Finset ι} {w : World} : w ∈ subDisj p S ↔ ∃ i ∈ S, w ∈ p i

theorem Exhaustification.subDisjsOfCard_subset_subDisjs {World : Type u_1} {ι : Type u_2} {I : Finset ι} {p : ι → Set World} (hI : I.Nonempty) {m : ℕ} (hm : 0 < m) : subDisjsOfCard I p m ⊆ subDisjs I p

theorem Exhaustification.isMinimal_of_single {World : Type u_1} {ι : Type u_2} {I : Finset ι} {p : ι → Set World} {A : Set (Set World)} {i : ι} (hi : i ∈ I) {w : World} (hA : ∀ q ∈ A, w ∈ q → ∃ S ⊆ I, q = subDisj p S) (hsplit : ∀ j ∈ I, j ≠ i → ∃ S ⊆ I, subDisj p S ∈ A ∧ j ∈ S ∧ i ∉ S) (hw : ∀ j ∈ I, w ∈ p j ↔ j = i) : IsMinimal A (disj I p) w

A world verifying exactly the disjunct i is minimal among the disjunction's worlds, relative to a family whose alternatives true at that world are sub-disjunctions and which separates every other index from i.

theorem Exhaustification.not_isInnocentlyExcludable_of_subDisjs {World : Type u_1} {ι : Type u_2} {I : Finset ι} {p : ι → Set World} {A : Set (Set World)} (hA : A ⊆ subDisjs I p) (hsplit : ∀ i ∈ I, ∀ j ∈ I, j ≠ i → ∃ S ⊆ I, subDisj p S ∈ A ∧ j ∈ S ∧ i ∉ S) (hsep : ∀ i ∈ I, ∃ (w : World), ∀ j ∈ I, w ∈ p j ↔ j = i) (q : Set World) : ¬IsInnocentlyExcludable A (disj I p) q

Nothing is innocently excludable: each sub-disjunction holds at the minimal world of one of its disjuncts.

theorem Exhaustification.cell_nonempty_of_subDisjs {World : Type u_1} {ι : Type u_2} {I : Finset ι} {p : ι → Set World} {A : Set (Set World)} (hA : A ⊆ subDisjs I p) (hsplit : ∀ i ∈ I, ∀ j ∈ I, j ≠ i → ∃ S ⊆ I, subDisj p S ∈ A ∧ j ∈ S ∧ i ∉ S) (hsep : ∀ i ∈ I, ∃ (w : World), ∀ j ∈ I, w ∈ p j ↔ j = i) (hI : I.Nonempty) (hall : ∃ (w : World), ∀ i ∈ I, w ∈ p i) : (cell A (disj I p)).Nonempty

With a world verifying every disjunct, the cell is consistent.

theorem Exhaustification.exhIEII_eq_sInter_of_subDisjs {World : Type u_1} {ι : Type u_2} {I : Finset ι} {p : ι → Set World} {A : Set (Set World)} (hA : A ⊆ subDisjs I p) (hsplit : ∀ i ∈ I, ∀ j ∈ I, j ≠ i → ∃ S ⊆ I, subDisj p S ∈ A ∧ j ∈ S ∧ i ∉ S) (hsep : ∀ i ∈ I, ∃ (w : World), ∀ j ∈ I, w ∈ p j ↔ j = i) (hI : I.Nonempty) (hall : ∃ (w : World), ∀ i ∈ I, w ∈ p i) : exhIEII A (disj I p) = disj I p ∩ ⋂₀ A

Exhaustification asserts the disjunction and every alternative.

theorem Exhaustification.hsplit_subDisjs {World : Type u_1} {ι : Type u_2} {I : Finset ι} {p : ι → Set World} (i : ι) : i ∈ I → ∀ j ∈ I, j ≠ i → ∃ S ⊆ I, subDisj p S ∈ subDisjs I p ∧ j ∈ S ∧ i ∉ S

theorem Exhaustification.exhIEII_subDisjs {World : Type u_1} {ι : Type u_2} {I : Finset ι} {p : ι → Set World} (hsep : ∀ i ∈ I, ∃ (w : World), ∀ j ∈ I, w ∈ p j ↔ j = i) (hI : I.Nonempty) (hall : ∃ (w : World), ∀ i ∈ I, w ∈ p i) : exhIEII (subDisjs I p) (disj I p) = ⋂ i ∈ I, p i

All the sub-disjunctions strengthen the disjunction to the conjunction.

theorem Exhaustification.hsplit_subDisjsOfCard {World : Type u_1} {ι : Type u_2} {I : Finset ι} {p : ι → Set World} [DecidableEq ι] {m : ℕ} (hm : 0 < m) (hmI : m < I.card) (i : ι) : i ∈ I → ∀ j ∈ I, j ≠ i → ∃ S ⊆ I, subDisj p S ∈ subDisjsOfCard I p m ∧ j ∈ S ∧ i ∉ S

theorem Exhaustification.forall_card_eq_exists_mem_iff {ι : Type u_2} {I : Finset ι} [DecidableEq ι] {T : Finset ι} (hT : T ⊆ I) {m : ℕ} : (∀ S ⊆ I, S.card = m → ∃ i ∈ S, i ∈ T) ↔ I.card < m + T.card

Every size-m subset of I meets T ⊆ I iff fewer than m elements of I lie outside T.

theorem Exhaustification.subDisjsOfCard_card {World : Type u_1} {ι : Type u_2} {I : Finset ι} {p : ι → Set World} : subDisjsOfCard I p I.card = {disj I p}

The size-|I| alternatives are the disjunction itself.

theorem Exhaustification.exhIEII_subDisjsOfCard {World : Type u_1} {ι : Type u_2} {I : Finset ι} {p : ι → Set World} [DecidableEq ι] [(w : World) → (i : ι) → Decidable (w ∈ p i)] (hsep : ∀ i ∈ I, ∃ (w : World), ∀ j ∈ I, w ∈ p j ↔ j = i) (hall : ∃ (w : World), ∀ i ∈ I, w ∈ p i) {m : ℕ} (hm : 0 < m) (hmI : m ≤ I.card) : exhIEII (subDisjsOfCard I p m) (disj I p) = {w : World | I.card < m + {i ∈ I | w ∈ p i}.card}

Keeping only the size-m alternatives strengthens the disjunction to "at least |I| + 1 - m disjuncts hold".

theorem Exhaustification.isInnocentlyExcludable_iInter_of_insert {World : Type u_1} {ι : Type u_2} {I : Finset ι} {p : ι → Set World} (hsep : ∀ i ∈ I, ∃ (w : World), ∀ j ∈ I, w ∈ p j ↔ j = i) (h2 : 2 ≤ I.card) : IsInnocentlyExcludable (insert (⋂ i ∈ I, p i) (subDisjs I p)) (disj I p) (⋂ i ∈ I, p i)

With the conjunction of the disjuncts among the alternatives, it is innocently excludable whenever there are two disjuncts: exhaustification then denies it.

theorem Exhaustification.isMinimalCover_pair {World : Type u_1} {φ d₁ d₂ c : Set World} {w₁ w₂ : World} (hcov : φ ⊆ d₁ ∪ d₂) (h₁ : w₁ ∈ φ ∩ d₁ ∧ w₁ ∉ d₂ ∪ c) (h₂ : w₂ ∈ φ ∩ d₂ ∧ w₂ ∉ d₁ ∪ c) : IsMinimalCover {φ, d₁, d₂, c} φ {w₁, w₂}

Two worlds verifying the prejacent with exactly one of two alternatives that cover it represent its minimal worlds.

theorem Exhaustification.exhIEII_pair {World : Type u_1} {φ d₁ d₂ c : Set World} (hcov : φ ⊆ d₁ ∪ d₂) (h₁ : ∃ w ∈ φ ∩ d₁, w ∉ d₂ ∪ c) (h₂ : ∃ w ∈ φ ∩ d₂, w ∉ d₁ ∪ c) (h : ∃ w ∈ φ ∩ d₁ ∩ d₂, w ∉ c) : exhIEII {φ, d₁, d₂, c} φ = (φ ∩ d₁ ∩ d₂) \ c

A prejacent covered by two alternatives, each verifiable alone, and a third alternative false wherever only one of them holds: exhaustification asserts both and denies the third, provided that is consistent — free choice and simplification of disjunctive antecedents.

theorem Exhaustification.exhIEII_pair_inter {World : Type u_1} {φ d₁ d₂ : Set World} (hcov : φ ⊆ d₁ ∪ d₂) (h₁ : ∃ w ∈ φ ∩ d₁, w ∉ d₂) (h₂ : ∃ w ∈ φ ∩ d₂, w ∉ d₁) : exhIEII {φ, d₁, d₂, d₁ ∩ d₂} φ = φ \ (d₁ ∩ d₂)

With the conjunction of the two alternatives itself among the alternatives, exhaustification denies it and includes nothing.

theorem Exhaustification.cell_pair_inter {World : Type u_1} {φ d₁ d₂ : Set World} (hcov : φ ⊆ d₁ ∪ d₂) (h₁ : ∃ w ∈ φ ∩ d₁, w ∉ d₂) (h₂ : ∃ w ∈ φ ∩ d₂, w ∉ d₁) : cell {φ, d₁, d₂, d₁ ∩ d₂} φ = ∅

The cell of a disjunction whose alternatives include the conjunction is contradictory.

theorem Exhaustification.II_pair {World : Type u_1} {φ d₁ d₂ c : Set World} (hcov : φ ⊆ d₁ ∪ d₂) (h₁ : ∃ w ∈ φ ∩ d₁, w ∉ d₂ ∪ c) (h₂ : ∃ w ∈ φ ∩ d₂, w ∉ d₁ ∪ c) (h : ∃ w ∈ φ ∩ d₁ ∩ d₂, w ∉ c) : II {φ, d₁, d₂, c} φ = {φ, d₁, d₂}

The includable alternatives are the prejacent and the two covering alternatives.

theorem Exhaustification.exhIEII_insert_range {World : Type u_1} {ι : Type u_2} {φ : Set World} {x : ι → Set World} (hcov : φ ⊆ ⋃ (i : ι), x i) (hsep : ∀ (i : ι), ∃ w ∈ φ ∩ x i, ∀ (j : ι), j ≠ i → w ∉ x j) (h : ∃ w ∈ φ, ∀ (i : ι), w ∈ x i) : exhIEII (insert φ (Set.range x)) φ = φ ∩ ⋂ (i : ι), x i

A prejacent covered by alternatives each verifiable alone: exhaustification asserts all of them, provided that is consistent.

theorem Exhaustification.exhIEII_quantified {World : Type u_1} {φ s₁ s₂ sb e e₁ e₂ eb : Set World} (hcov : ∀ w ∈ φ, w ∈ s₁ ∧ w ∈ e ∧ w ∈ e₁ ∨ w ∈ s₂ ∧ w ∈ e ∧ w ∈ e₂ ∨ w ∈ e ∧ w ∈ e₁ ∧ w ∈ e₂) (h₁ : ∃ w ∈ φ, w ∈ s₁ ∧ w ∈ e ∧ w ∈ e₁ ∧ w ∉ s₂ ∧ w ∉ sb ∧ w ∉ e₂ ∧ w ∉ eb) (h₂ : ∃ w ∈ φ, w ∈ s₂ ∧ w ∈ e ∧ w ∈ e₂ ∧ w ∉ s₁ ∧ w ∉ sb ∧ w ∉ e₁ ∧ w ∉ eb) (h₃ : ∃ w ∈ φ, w ∈ e ∧ w ∈ e₁ ∧ w ∈ e₂ ∧ w ∉ s₁ ∧ w ∉ s₂ ∧ w ∉ sb ∧ w ∉ eb) (h : ∃ w ∈ φ, w ∈ s₁ ∧ w ∈ s₂ ∧ w ∈ e ∧ w ∈ e₁ ∧ w ∈ e₂ ∧ w ∉ sb ∧ w ∉ eb) : exhIEII {φ, s₁, s₂, sb, e, e₁, e₂, eb} φ = (φ ∩ s₁ ∩ s₂ ∩ e ∩ e₁ ∩ e₂) \ (sb ∪ eb)

A disjunction under a quantifier, with alternatives replacing the disjunction by its disjuncts and their conjunction and the quantifier by a weaker one (s strong, e weak, b conjunctive). Each prejacent world verifies one of three patterns — one disjunct's strong alternative with the weak alternatives, or the weak alternatives alone — each pattern is realized exactly, and asserting both strong disjunct alternatives while denying the conjunctive ones is consistent: exhaustification then does exactly that — universal free choice.