Bar-Lev and Fox 2020: Free choice, simplification, and Innocent Inclusion

Exhaustification with Innocent Inclusion returns the cell of the partition induced by the alternatives whenever that cell is consistent. Free-choice disjunction ◇(a ∨ b), whose alternatives are ◇a, ◇b and ◇(a ∧ b), strengthens to ◇a ∧ ◇b ∧ ¬◇(a ∧ b); plain a ∨ b, whose conjunctive alternative is the conjunction of the other two, only denies it. only presupposes the includable alternatives, so free choice under only projects. Free choice under a universal quantifier, its negative counterpart, the existential-over-universal case and most with a disjunctive restrictor are one computation over eight alternatives. Simplification of disjunctive antecedents is the same strengthening over a variably strict conditional: it fails when the consequent is one of the disjuncts, and an or both antecedent, exhaustified by Hurford's constraint, turns the conjunctive simplification from excluded into included.

Main results

• freeChoice, simpleDisjunction: the modal and the plain disjunction.
• II_fcAlts, isInnocentlyExcludable_fcAlts_iff: what free choice includes and excludes.
• support_only_fcAlts: free choice under only is presupposed.
• posExt_only_eq: without symmetric alternatives only agrees with the exclusive Focus.Particles.only.
• universalFreeChoice, negativeUniversalFreeChoice, freeChoiceOverUniversal, simplificationMost: instances of Exhaustification.exhIEII_quantified.
• sda, sda_consequent_disjunct, orBoth: simplification, its failure, and the switches.

References

• [BLF20]
• [Fox07]
• [Alx14]
• [Che09b]
• [Nou17]
• [McKVI77]
• [Nut80]
• [CZC18]
• [CFS12]

Free choice and simple disjunction

def BarLevFox2020.fcAlts {W : Type u_1} (R : SetRel W W) (a b : Set W) : Set (Set W)

The alternatives of ◇(a ∨ b) replace the disjunction by its disjuncts and their conjunction.

Equations

• BarLevFox2020.fcAlts R a b = {R.preimage (a ∪ b), R.preimage a, R.preimage b, R.preimage (a ∩ b)}

structure BarLevFox2020.FreeChoiceWitnesses {W : Type u_1} (R : SetRel W W) (a b : Set W) : Prop

Free choice needs a world permitting only a, one permitting only b, and one permitting each but not both.

• only_left : ∃ w ∈ R.preimage a, w ∉ R.preimage b
• only_right : ∃ w ∈ R.preimage b, w ∉ R.preimage a
• not_both : ∃ w ∈ R.preimage a ∩ R.preimage b, w ∉ R.preimage (a ∩ b)

theorem BarLevFox2020.freeChoice {W : Type u_1} {R : SetRel W W} {a b : Set W} (hF : FreeChoiceWitnesses R a b) : Exhaustification.exhIEII (fcAlts R a b) (R.preimage (a ∪ b)) = (R.preimage a ∩ R.preimage b) \ R.preimage (a ∩ b)

Given the witnesses, ◇(a ∨ b) strengthens to ◇a ∧ ◇b ∧ ¬◇(a ∧ b), free choice.

theorem BarLevFox2020.II_fcAlts {W : Type u_1} {R : SetRel W W} {a b : Set W} (hF : FreeChoiceWitnesses R a b) : Exhaustification.II (fcAlts R a b) (R.preimage (a ∪ b)) = {R.preimage (a ∪ b), R.preimage a, R.preimage b}

The includable alternatives of ◇(a ∨ b) are the prejacent and the disjunct alternatives.

theorem BarLevFox2020.isInnocentlyExcludable_fcAlts_iff {W : Type u_1} {R : SetRel W W} {a b : Set W} (hF : FreeChoiceWitnesses R a b) {q : Set W} : Exhaustification.IsInnocentlyExcludable (fcAlts R a b) (R.preimage (a ∪ b)) q ↔ q = R.preimage (a ∩ b)

The only excludable alternative of ◇(a ∨ b) is the conjunctive one.

theorem BarLevFox2020.simpleDisjunction {W : Type u_1} {a b : Set W} (h₁ : ∃ w ∈ a, w ∉ b) (h₂ : ∃ w ∈ b, w ∉ a) : Exhaustification.exhIEII {a ∪ b, a, b, a ∩ b} (a ∪ b) = (a ∪ b) \ (a ∩ b)

Without the modal the conjunctive alternative is the conjunction of the disjunct alternatives, so exhaustification denies it and includes neither disjunct.

theorem BarLevFox2020.simpleDisjunction_cell {W : Type u_1} {a b : Set W} (h₁ : ∃ w ∈ a, w ∉ b) (h₂ : ∃ w ∈ b, w ∉ a) : Exhaustification.cell {a ∪ b, a, b, a ∩ b} (a ∪ b) = ∅

The cell of simple disjunction is contradictory, so cell identification does not apply.

only

noncomputable def BarLevFox2020.only {W : Type u_1} (ALT : Set (Set W)) (φ : Set W) : W → SignType

only presupposes the innocently includable alternatives and asserts that the innocently excludable ones are false (32).

Equations

• BarLevFox2020.only ALT φ = {w : W | ∀ r ∈ Exhaustification.II ALT φ, w ∈ r}.indicator fun (w : W) => SignType.ofProp (∀ (q : Set W), Exhaustification.IsInnocentlyExcludable ALT φ q → w ∉ q)

theorem BarLevFox2020.support_only_fcAlts {W : Type u_1} {R : SetRel W W} {a b : Set W} (hF : FreeChoiceWitnesses R a b) : Function.support (only (fcAlts R a b) (R.preimage (a ∪ b))) = R.preimage a ∩ R.preimage b

Free choice under only is presupposed, since only ◇(a ∨ b) presupposes ◇a and ◇b.

theorem BarLevFox2020.posExt_only_eq {W : Type u_1} {ALT : Set (Set W)} {φ : Set W} (hφ : φ ∈ ALT) (hIE : ∀ (q : Set W), Exhaustification.IsInnocentlyExcludable ALT φ q ↔ q ∈ ALT ∧ ¬φ ⊆ q) (hII : Exhaustification.II ALT φ = {φ}) : Trivalent.posExt (only ALT φ) = Trivalent.posExt (Focus.Particles.only (fun (x1 x2 : Set W) => x1 ⊆ x2) ALT φ)

Where the prejacent is the only includable alternative and the excludable ones are exactly those it does not entail, only is true at the same worlds as the exclusive Focus.Particles.only on the entailment scale, the entry (29b) that Innocent Inclusion revises.

Simplification of disjunctive antecedents

def BarLevFox2020.sdaAlts {W : Type u_1} (ord : W → Preorder W) (p q r : Set W) : Set (Set W)

The alternatives of (p ∨ q) → r replace the antecedent's disjunction by its disjuncts and their conjunction.

Equations

• BarLevFox2020.sdaAlts ord p q r = {Conditional.closestImp ord (p ∪ q) r, Conditional.closestImp ord p r, Conditional.closestImp ord q r, Conditional.closestImp ord (p ∩ q) r}

theorem BarLevFox2020.sda {W : Type u_1} {ord : W → Preorder W} {p q r : Set W} (htot : ∀ (w : W), Std.Total LE.le) (h₁ : ∃ w ∈ Conditional.closestImp ord (p ∪ q) r, w ∉ Conditional.closestImp ord q r ∪ Conditional.closestImp ord (p ∩ q) r) (h₂ : ∃ w ∈ Conditional.closestImp ord (p ∪ q) r, w ∉ Conditional.closestImp ord p r ∪ Conditional.closestImp ord (p ∩ q) r) (h : ∃ w ∈ Conditional.closestImp ord p r ∩ Conditional.closestImp ord q r, w ∉ Conditional.closestImp ord (p ∩ q) r) : Exhaustification.exhIEII (sdaAlts ord p q r) (Conditional.closestImp ord (p ∪ q) r) = (Conditional.closestImp ord p r ∩ Conditional.closestImp ord q r) \ Conditional.closestImp ord (p ∩ q) r

Disjunctive antecedents simplify. Over total similarity preorders, given a world where only the first simplification holds, one where only the second does, and one where both hold but the conjunctive one fails, (p ∨ q) → r strengthens to (p → r) ∧ (q → r) ∧ ¬((p ∧ q) → r).

theorem BarLevFox2020.sda_consequent_disjunct {W : Type u_1} {ord : W → Preorder W} {p q : Set W} (h : ∃ w ∈ Conditional.closestImp ord (p ∪ q) p, w ∉ Conditional.closestImp ord q p) : Exhaustification.exhIEII (sdaAlts ord p q p) (Conditional.closestImp ord (p ∪ q) p) = Conditional.closestImp ord (p ∪ q) p \ Conditional.closestImp ord q p

Simplification fails when the consequent is one of the disjuncts (71), since the other simplification is the only contingent alternative and so is excluded.

def BarLevFox2020.orBothAlts {W : Type u_1} (ord : W → Preorder W) (p q r : Set W) : Set (Set W)

The alternatives of (Exh(p ∨ q) ∨ (p ∧ q)) → r, the or both antecedent parsed with an embedded exhaustifier by Hurford's constraint (80), are the antecedent's three cells.

Equations

• BarLevFox2020.orBothAlts ord p q r = {Conditional.closestImp ord (p ∪ q) r, Conditional.closestImp ord (p \ q) r, Conditional.closestImp ord (q \ p) r, Conditional.closestImp ord (p ∩ q) r}

theorem BarLevFox2020.orBoth {W : Type u_1} {ord : W → Preorder W} {p q r : Set W} (htot : ∀ (w : W), Std.Total LE.le) (h₁ : ∃ w ∈ Conditional.closestImp ord (p ∪ q) r ∩ Conditional.closestImp ord (p \ q) r, w ∉ Conditional.closestImp ord (q \ p) r ∪ Conditional.closestImp ord (p ∩ q) r) (h₂ : ∃ w ∈ Conditional.closestImp ord (p ∪ q) r ∩ Conditional.closestImp ord (q \ p) r, w ∉ Conditional.closestImp ord (p \ q) r ∪ Conditional.closestImp ord (p ∩ q) r) (h₃ : ∃ w ∈ Conditional.closestImp ord (p ∪ q) r ∩ Conditional.closestImp ord (p ∩ q) r, w ∉ Conditional.closestImp ord (p \ q) r ∪ Conditional.closestImp ord (q \ p) r) (h : ∃ w ∈ Conditional.closestImp ord (p ∪ q) r, w ∈ Conditional.closestImp ord (p \ q) r ∧ w ∈ Conditional.closestImp ord (q \ p) r ∧ w ∈ Conditional.closestImp ord (p ∩ q) r) : Exhaustification.exhIEII (orBothAlts ord p q r) (Conditional.closestImp ord (p ∪ q) r) = Conditional.closestImp ord (p ∪ q) r ∩ Conditional.closestImp ord (p \ q) r ∩ Conditional.closestImp ord (q \ p) r ∩ Conditional.closestImp ord (p ∩ q) r

With the antecedent's cells as alternatives nothing is excludable and, given a world verifying each cell's conditional alone and one verifying all three, everything is included, so (p ∨ q) → r asserts the conjunctive conditional it denied under sdaAlts (82).

The switches

structure BarLevFox2020.Switch : Type

A world of [CZC18]'s scenario records whether each switch is up, and the wiring of the light.

• up₁ : Bool
• up₂ : Bool
• light : Bool → Bool → Bool

def BarLevFox2020.instDecidableEqSwitch.decEq (x✝ x✝¹ : Switch) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance BarLevFox2020.instDecidableEqSwitch : DecidableEq Switch

Equations

• BarLevFox2020.instDecidableEqSwitch = BarLevFox2020.instDecidableEqSwitch.decEq

@[instance_reducible]

instance BarLevFox2020.instFintypeSwitch : Fintype Switch

Equations

• BarLevFox2020.instFintypeSwitch = Fintype.ofEquiv ((_ : Bool) × (_ : Bool) × (Bool → Bool → Bool)) BarLevFox2020.Switch.proxyTypeEquiv

def BarLevFox2020.Switch.rank (w₀ w : Switch) : ℕ

Worlds with a different wiring are farther than any with the same; among the latter, distance is the number of switches in another position.

Equations

• w₀.rank w = ((if w.light = w₀.light then 0 else 4) + if w.up₁ = w₀.up₁ then 0 else 1) + if w.up₂ = w₀.up₂ then 0 else 1

@[reducible, inline]

abbrev BarLevFox2020.Switch.sim (w₀ : Switch) : Preorder Switch

Similarity to w₀, ordered by rank.

Equations

• w₀.sim = Preorder.lift w₀.rank

theorem BarLevFox2020.Switch.sim_total (w₀ : Switch) : Std.Total LE.le

@[reducible, inline]

abbrev BarLevFox2020.Switch.down₁ : Set Switch

Switch A is down.

Equations

• BarLevFox2020.Switch.down₁ = {w : BarLevFox2020.Switch | w.up₁ = false}

@[reducible, inline]

abbrev BarLevFox2020.Switch.down₂ : Set Switch

Switch B is down.

Equations

• BarLevFox2020.Switch.down₂ = {w : BarLevFox2020.Switch | w.up₂ = false}

@[reducible, inline]

abbrev BarLevFox2020.Switch.off : Set Switch

The light is off.

Equations

• BarLevFox2020.Switch.off = {w : BarLevFox2020.Switch | w.light w.up₁ w.up₂ = false}

def BarLevFox2020.Switch.actual : Switch

Both switches up, and the light on exactly when the switches agree.

Equations

• BarLevFox2020.Switch.actual = { up₁ := true, up₂ := true, light := fun (x y : Bool) => x == y }

theorem BarLevFox2020.Switch.sda_actual : actual ∈ Exhaustification.exhIEII (sdaAlts sim down₁ down₂ off) (Conditional.closestImp sim (down₁ ∪ down₂) off)

If switch A or switch B were down, the light would be off (76) is true in the scenario, since its strengthening asserts both simplifications and denies the conjunctive one.

theorem BarLevFox2020.Switch.orBoth_actual : actual ∉ Exhaustification.exhIEII (orBothAlts sim down₁ down₂ off) (Conditional.closestImp sim (down₁ ∪ down₂) off)

If switch A or switch B or both were down, the light would be off (78) is false in the scenario, since its strengthening asserts the conjunctive conditional.

Free choice under quantifiers

def BarLevFox2020.universalAlts {W : Type u_1} {D : Type u_2} (P Q B : D → Set W) : Set (Set W)

The alternatives of ∀x(Px ∨ Qx) (41) replace the disjunction by its disjuncts and by their conjunctive counterpart B, and the universal by the existential.

Equations

• BarLevFox2020.universalAlts P Q B = {⋂ (x : D), P x ∪ Q x, ⋂ (x : D), P x, ⋂ (x : D), Q x, ⋂ (x : D), B x, ⋃ (x : D), P x ∪ Q x, ⋃ (x : D), P x, ⋃ (x : D), Q x, ⋃ (x : D), B x}

theorem BarLevFox2020.universalFreeChoice {W : Type u_1} {D : Type u_2} [Nonempty D] {P Q B : D → Set W} (hB : ∀ (x : D), B x ⊆ P x ∩ Q x) (h₁ : ∃ (w : W), (∀ (x : D), w ∈ P x) ∧ ∀ (x : D), w ∉ Q x) (h₂ : ∃ (w : W), (∀ (x : D), w ∈ Q x) ∧ ∀ (x : D), w ∉ P x) (h₃ : ∃ (w : W), (∀ (x : D), w ∈ P x ↔ w ∉ Q x) ∧ (∃ (x : D), w ∈ P x) ∧ ∃ (x : D), w ∈ Q x) (h : ∃ (w : W), (∀ (x : D), w ∈ P x) ∧ (∀ (x : D), w ∈ Q x) ∧ ∀ (x : D), w ∉ B x) : Exhaustification.exhIEII (universalAlts P Q B) (⋂ (x : D), P x ∪ Q x) = ((⋂ (x : D), P x) ∩ ⋂ (x : D), Q x) \ ⋃ (x : D), B x

Given a world where every individual has P and none Q, one the other way round, one where each has exactly one and both occur, and one where every individual has P and Q but none B, ∀x(Px ∨ Qx) strengthens to ∀x Px ∧ ∀x Qx ∧ ¬∃x Bx, universal free choice (44). With Px = ◇px and Bx = ◇(px ∧ qx) this is (36).

def BarLevFox2020.negativeUniversalAlts {W : Type u_1} {D : Type u_2} (R : SetRel W W) (p q : D → Set W) : Set (Set W)

The alternatives of ¬∃x □(px ∧ qx), no student is required to solve both (46), replace the conjunction by its conjuncts and their disjunction, and no by not every.

Equations

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

theorem BarLevFox2020.negativeUniversalFreeChoice {W : Type u_1} {D : Type u_2} [Nonempty D] {R : SetRel W W} {p q : D → Set W} (h₁ : ∃ (w : W), (∀ (x : D), w ∉ R.core (p x)) ∧ ∀ (x : D), w ∈ R.core (q x)) (h₂ : ∃ (w : W), (∀ (x : D), w ∉ R.core (q x)) ∧ ∀ (x : D), w ∈ R.core (p x)) (h₃ : ∃ (w : W), (∀ (x : D), w ∈ R.core (p x ∪ q x)) ∧ (∀ (x : D), w ∉ R.core (p x ∩ q x)) ∧ (∃ (x : D), w ∈ R.core (p x)) ∧ (∃ (x : D), w ∈ R.core (q x)) ∧ (∃ (x : D), w ∉ R.core (p x)) ∧ ∃ (x : D), w ∉ R.core (q x)) (h : ∃ (w : W), (∀ (x : D), w ∉ R.core (p x)) ∧ (∀ (x : D), w ∉ R.core (q x)) ∧ ∀ (x : D), w ∈ R.core (p x ∪ q x)) : Exhaustification.exhIEII (negativeUniversalAlts R p q) (⋃ (x : D), R.core (p x ∩ q x))ᶜ = (⋃ (x : D), R.core (p x))ᶜ ∩ (⋃ (x : D), R.core (q x))ᶜ ∩ ⋂ (x : D), R.core (p x ∪ q x)

The alternatives of ¬∃x □(px ∧ qx) stand in the entailment pattern of universal free choice, so with the corresponding worlds it strengthens to ¬∃x □px ∧ ¬∃x □qx ∧ ∀x □(px ∨ qx), negative universal free choice (47).

def BarLevFox2020.overUniversalAlts {W : Type u_1} {D : Type u_2} (R : SetRel W W) (p q : D → Set W) : Set (Set W)

The alternatives of ◇∀x(px ∨ qx) (55).

Equations

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

theorem BarLevFox2020.freeChoiceOverUniversal {W : Type u_1} {D : Type u_2} [Nonempty D] {R : SetRel W W} {p q : D → Set W} (h₁ : ∃ w ∈ R.preimage (⋂ (x : D), p x), w ∉ R.preimage (⋃ (x : D), q x)) (h₂ : ∃ w ∈ R.preimage (⋂ (x : D), q x), w ∉ R.preimage (⋃ (x : D), p x)) (h₃ : ∃ w ∈ R.preimage (⋂ (x : D), p x ∪ q x) ∩ R.preimage (⋃ (x : D), p x) ∩ R.preimage (⋃ (x : D), q x), w ∉ R.preimage (⋂ (x : D), p x) ∪ R.preimage (⋂ (x : D), q x) ∪ R.preimage (⋃ (x : D), p x ∩ q x)) (h : ∃ w ∈ R.preimage (⋂ (x : D), p x) ∩ R.preimage (⋂ (x : D), q x), w ∉ R.preimage (⋃ (x : D), p x ∩ q x)) : Exhaustification.exhIEII (overUniversalAlts R p q) (R.preimage (⋂ (x : D), p x ∪ q x)) = (R.preimage (⋂ (x : D), p x) ∩ R.preimage (⋂ (x : D), q x)) \ R.preimage (⋃ (x : D), p x ∩ q x)

Given the corresponding worlds, free choice with the existential modal over the universal (57), [Nou17]'s case, strengthens ◇∀x(px ∨ qx) to ◇∀x px ∧ ◇∀x qx ∧ ¬◇∃x(px ∧ qx), although ◇∀ does not distribute over disjunction.

Simplification with most

def BarLevFox2020.Most {D : Type u_2} [DecidableEq D] (P S : Finset D) : Prop

Most P S says that more than half of P lies in S (86).

Equations

• BarLevFox2020.Most P S = (P.card < 2 * (P ∩ S).card)

def BarLevFox2020.Overlaps {D : Type u_2} [DecidableEq D] (P S : Finset D) : Prop

Overlaps P S says that P and S meet.

Equations

• BarLevFox2020.Overlaps P S = (P ∩ S).Nonempty

theorem BarLevFox2020.Most.overlaps {D : Type u_2} [DecidableEq D] {P S : Finset D} (h : Most P S) : Overlaps P S

theorem BarLevFox2020.Overlaps.of_inter_left {D : Type u_2} [DecidableEq D] {P Q S : Finset D} (h : Overlaps (P ∩ Q) S) : Overlaps P S

theorem BarLevFox2020.Overlaps.of_inter_right {D : Type u_2} [DecidableEq D] {P Q S : Finset D} (h : Overlaps (P ∩ Q) S) : Overlaps Q S

theorem BarLevFox2020.overlaps_union_iff {D : Type u_2} [DecidableEq D] {P Q S : Finset D} : Overlaps (P ∪ Q) S ↔ Overlaps P S ∨ Overlaps Q S

theorem BarLevFox2020.Most.of_union {D : Type u_2} [DecidableEq D] {P Q S : Finset D} (h : Most (P ∪ Q) S) (hQ : ¬Overlaps Q S) : Most P S

Most is not monotone in its restrictor, but a restrictor that adds nothing to the scope can be dropped.

theorem BarLevFox2020.Most.of_union_right {D : Type u_2} [DecidableEq D] {P Q S : Finset D} (h : Most (P ∪ Q) S) (hP : ¬Overlaps P S) : Most Q S

def BarLevFox2020.mostAlts {W : Type u_1} {D : Type u_2} [DecidableEq D] (P Q S : W → Finset D) : Set (Set W)

The alternatives of most(P ∪ Q)(S) (87) replace the disjunctive restrictor by its disjuncts and their intersection, and most by some.

Equations

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

theorem BarLevFox2020.simplificationMost {W : Type u_1} {D : Type u_2} [DecidableEq D] {P Q S : W → Finset D} (h₁ : ∃ (w : W), Most (P w ∪ Q w) (S w) ∧ Most (P w) (S w) ∧ ¬Overlaps (Q w) (S w)) (h₂ : ∃ (w : W), Most (P w ∪ Q w) (S w) ∧ Most (Q w) (S w) ∧ ¬Overlaps (P w) (S w)) (h₃ : ∃ (w : W), Most (P w ∪ Q w) (S w) ∧ ¬Most (P w) (S w) ∧ ¬Most (Q w) (S w) ∧ Overlaps (P w) (S w) ∧ Overlaps (Q w) (S w) ∧ ¬Overlaps (P w ∩ Q w) (S w)) (h : ∃ (w : W), Most (P w ∪ Q w) (S w) ∧ Most (P w) (S w) ∧ Most (Q w) (S w) ∧ ¬Overlaps (P w ∩ Q w) (S w)) : Exhaustification.exhIEII (mostAlts P Q S) {w : W | Most (P w ∪ Q w) (S w)} = ({w : W | Most (P w ∪ Q w) (S w)} ∩ {w : W | Most (P w) (S w)} ∩ {w : W | Most (Q w) (S w)}) \ {w : W | Overlaps (P w ∩ Q w) (S w)}

Given a world where most of P ∪ Q and most of P are in S but nothing of Q is, one the other way round, one where most of P ∪ Q but of neither P nor Q is, and one where most of each is but nothing of P ∩ Q, most(P ∪ Q)(S) strengthens to most(P)(S) ∧ most(Q)(S) ∧ ¬some(P ∩ Q)(S), simplification with most (89).