Booth (2022a): Independent alternatives: Ross's puzzle and free choice

[Boo22a] explains Ross's puzzle and free choice permission by the Independence inferences: accepting □(p ∨ q) or ◇(p ∨ q) commits a speaker to ◇(p ∧ ¬q) and ◇(q ∧ ¬p), each disjunct an option independently of the other. These are strictly stronger than the Diversity inferences ◇p, ◇q of the standard analyses (§4), and they amount to the disjuncts' truth sets forming a minimal cover of the relevant worlds, where the Diversity inferences need only a super cover (§5). The minimal covering semantics of §6 validates them for inquisitive propositions; §7 notes that its unilateral version loses the duality of the modals and the distribution of negated modals over disjunction, and recovers both with bilateral propositions; §8 shows the truth-value gaps this creates are well placed. The semantics is the theory-layer MinimalCovering.

Main results

• truth_box_disj, truth_dia_disj: the target truth conditions of §5; box_diversity, truth_dia_conj_neg_subset: Independence is strictly stronger than Diversity, the gap witnessed by Figures.diversity_without_independence (Figure 1).
• truth_necessity_bang, truth_possibility_bang: over !φ the modals are the orthodox ModalLogic.Box and ModalLogic.Diamond (§6); box_bang_disj: the flexibility of (16)–(17).
• Unilateral.not_dia_disj, Unilateral.dia_right, Unilateral.box_neg_disj: the unilateral semantics of §6 invalidates Impossibility Distribution and duality (§7), and Unilateral.not_box_disj, Unilateral.box_right Unnecessity Distribution.
• Facts 1–7 of the appendix: box_independence_left, …, dia_independence_right (Fact 1); box_conditional_left, …, dia_conditional_right (Fact 2); Figures.ross_invalid (Fact 3); free_choice (Fact 4); box_eq_neg_diamond_neg, diamond_eq_neg_box_neg (Fact 5); impossibility_distribution_left, impossibility_distribution_right (Fact 6); unnecessity_distribution_left, unnecessity_distribution_right (Fact 7).
• dual_free_choice: the Dual Free Choice inference of fn. 32.
• §8: isCompl_truth_falsity (the modal-free fragment is classical), ross_gap, free_choice_gap, independence_gap and the card example CardGame.gap; Figures.not_contraposition: entailment is not closed under contraposition, the formal content of the "diplomatic resolution".

Implementation notes

• Validity over the admissible models of Def 1 is universal quantification over worlds, accessibility and valuation, with the hypothesis IncompRel (· ⊆ ·) (V p) (V q) for the two atoms each fact mentions. Def 1 as printed quantifies over all p, q ∈ At, which no model satisfies for p = q; it is read here for the pair at hand.
• The appendix prints [!φ] = (℘(info([φ]⁺)), ℘(info([ψ]⁻))), with ψ in the negative coordinate; this is a typo for φ, the only reading on which !φ is a bilateral proposition, and MinimalCovering.bang follows it.
• Fact 3 is non-validity: some admissible model has □p true and □(p ∨ q) not. The stronger pointwise claim of §8, that □p makes □(p ∨ q) neither true nor false, is ross_gap.

References

• [Boo22a]
• [Sim05]
• [CGR18]
• [Kra91]

Minimal covers and the Independence inferences (§§4–6)

theorem Booth2022a.truth_box_disj {W : Type u_1} {At : Type u_2} (V : At → Set W) (R : W → Set W) {p q : At} (h : IncompRel (fun (x1 x2 : Set W) => x1 ⊆ x2) (V p) (V q)) : (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).box).truth = {w : W | MinimalCovering.IsMinCover {V p, V q} (R w)}

The target truth conditions of □(p ∨ q) (§5): the truth sets of the disjuncts minimally cover the relevant worlds.

theorem Booth2022a.truth_dia_disj {W : Type u_1} {At : Type u_2} (V : At → Set W) (R : W → Set W) {p q : At} (h : IncompRel (fun (x1 x2 : Set W) => x1 ⊆ x2) (V p) (V q)) : (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).diamond).truth = {w : W | ∃ R' ⊆ R w, R'.Nonempty ∧ MinimalCovering.IsMinCover {V p, V q} R'}

The target truth conditions of ◇(p ∨ q) (§5): the truth sets of the disjuncts minimally cover a nonempty set of relevant worlds.

theorem Booth2022a.truth_box_atom {W : Type u_1} {At : Type u_2} (V : At → Set W) (R : W → Set W) (p : At) : (MinimalCovering.Formula.eval V R (MinimalCovering.Formula.atom p).box).truth = {w : W | (R w).Nonempty ∧ R w ⊆ V p}

An atom's necessity is orthodox: the relevant worlds are nonempty and inside its truth set.

theorem Booth2022a.truth_dia_atom {W : Type u_1} {At : Type u_2} (V : At → Set W) (R : W → Set W) (p : At) : (MinimalCovering.Formula.eval V R (MinimalCovering.Formula.atom p).diamond).truth = {w : W | (R w ∩ V p).Nonempty}

An atom's possibility is orthodox: some relevant world is in its truth set.

theorem Booth2022a.truth_dia_conj_neg {W : Type u_1} {At : Type u_2} (V : At → Set W) (R : W → Set W) (p q : At) : (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).conj (MinimalCovering.Formula.atom q).neg).diamond).truth = {w : W | (R w ∩ (V p \ V q)).Nonempty}

◇(p ∧ ¬q) is true where some relevant world is a p-without-q world.

theorem Booth2022a.box_meta_independence {W : Type u_1} {At : Type u_2} (V : At → Set W) (R : W → Set W) {p q : At} (h : IncompRel (fun (x1 x2 : Set W) => x1 ⊆ x2) (V p) (V q)) {w : W} (hw : w ∈ (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).box).truth) : (R w ∩ (V p \ V q)).Nonempty ∧ (R w ∩ (V q \ V p)).Nonempty

The meta-linguistic Independence inferences for □ (§4): the relevant worlds meet both relative complements.

theorem Booth2022a.dia_meta_independence {W : Type u_1} {At : Type u_2} (V : At → Set W) (R : W → Set W) {p q : At} (h : IncompRel (fun (x1 x2 : Set W) => x1 ⊆ x2) (V p) (V q)) {w : W} (hw : w ∈ (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).diamond).truth) : (R w ∩ (V p \ V q)).Nonempty ∧ (R w ∩ (V q \ V p)).Nonempty

The meta-linguistic Independence inferences for ◇ (§4).

theorem Booth2022a.box_diversity {W : Type u_1} {At : Type u_2} (V : At → Set W) (R : W → Set W) {p q : At} (h : IncompRel (fun (x1 x2 : Set W) => x1 ⊆ x2) (V p) (V q)) {w : W} (hw : w ∈ (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).box).truth) : (R w ∩ V p).Nonempty ∧ (R w ∩ V q).Nonempty

The meta-linguistic Diversity inferences follow (§4): the relevant worlds meet both truth sets.

theorem Booth2022a.truth_dia_conj_neg_subset {W : Type u_1} {At : Type u_2} (V : At → Set W) (R : W → Set W) (p q : At) : (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).conj (MinimalCovering.Formula.atom q).neg).diamond).truth ⊆ (MinimalCovering.Formula.eval V R (MinimalCovering.Formula.atom p).diamond).truth

◇(p ∧ ¬q) entails ◇p, so the Independence inferences are at least as strong as the Diversity inferences (§4); Figures.diversity_without_independence shows they are stronger.

theorem Booth2022a.truth_necessity_bang {W : Type u_1} (R : W → Set W) (φ : MinimalCovering.BilatInqProp W) : (MinimalCovering.necessity R (MinimalCovering.bang φ)).truth = {w : W | (R w).Nonempty ∧ ModalLogic.Box (SetRel.ofSuccessors R) (fun (x : W) => x ∈ φ.truth) w}

Over !φ, necessity is the orthodox universal modal over the relevant worlds ([Kra91]), given that they are nonempty (§6, and fn. 13 on the presupposition of nonempty domains).

theorem Booth2022a.truth_possibility_bang {W : Type u_1} (R : W → Set W) (φ : MinimalCovering.BilatInqProp W) : (MinimalCovering.possibility R (MinimalCovering.bang φ)).truth = {w : W | ModalLogic.Diamond (SetRel.ofSuccessors R) (fun (x : W) => x ∈ φ.truth) w}

Over !φ, possibility is the orthodox existential modal over the relevant worlds (§6).

theorem Booth2022a.box_bang_disj {W : Type u_1} {At : Type u_2} (V : At → Set W) (R : W → Set W) (p q : At) : (MinimalCovering.Formula.eval V R (MinimalCovering.Formula.atom p).box).truth ⊆ (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).bang.box).truth

Flexibility (§6, (16)–(17)): □p entails □!(p ∨ q), in every model.

The unilateral semantics loses duality and distribution (§7)

In the unilateral semantics of §6 a sentence denotes one inquisitive proposition, negation is the pseudocomplement ᶜ of Question W (the states disjoint from the informative content), and the modals are box and dia. Booth's scenario: in all relevant worlds Alicia burns the letter. Then ¬◇(M ∨ B) is true, since there is no relevant mailing-without-burning world, yet ◇B is true and □¬(M ∨ B) is not. The worlds record whether Alicia mails (M) and whether she burns (B) the letter; the relevant worlds are the two burning worlds, one of them a mailing world.

def Booth2022a.Unilateral.vM : Set (Bool × Bool)

Alicia mails the letter.

Equations

• Booth2022a.Unilateral.vM = {w : Bool × Bool | w.1 = true}

def Booth2022a.Unilateral.vB : Set (Bool × Bool)

Alicia burns the letter.

Equations

• Booth2022a.Unilateral.vB = {w : Bool × Bool | w.2 = true}

def Booth2022a.Unilateral.rB : Bool × Bool → Set (Bool × Bool)

The relevant worlds are the burning worlds.

Equations

• Booth2022a.Unilateral.rB x✝ = Booth2022a.Unilateral.vB

theorem Booth2022a.Unilateral.vM_ne_vB : vM ≠ vB

theorem Booth2022a.Unilateral.alt_disj : (Question.ofSet vM ⊔ Question.ofSet vB).alt = {vM, vB}

theorem Booth2022a.Unilateral.not_dia_disj (w : Bool × Bool) : w ∈ (MinimalCovering.dia rB (Question.ofSet vM ⊔ Question.ofSet vB))ᶜ.info

¬◇(M ∨ B) is true: no nonempty set of burning worlds contains a mailing-without-burning world, as a minimal cover by {M, B} would need.

theorem Booth2022a.Unilateral.dia_right (w : Bool × Bool) : w ∉ (MinimalCovering.dia rB (Question.ofSet vB))ᶜ.info

¬◇B is not true: some relevant world is a burning world. Impossibility Distribution (19) fails.

theorem Booth2022a.Unilateral.box_neg_disj (w : Bool × Bool) : w ∉ (MinimalCovering.box rB (Question.ofSet vM ⊔ Question.ofSet vB)ᶜ).info

□¬(M ∨ B) is not true while ¬◇(M ∨ B) is: duality (21) fails.

theorem Booth2022a.Unilateral.not_box_disj (w : Bool × Bool) : w ∈ (MinimalCovering.box rB (Question.ofSet vM ⊔ Question.ofSet vB))ᶜ.info

¬□(M ∨ B) is true: the burning worlds hold no mailing-without-burning world.

theorem Booth2022a.Unilateral.box_right (w : Bool × Bool) : w ∉ (MinimalCovering.box rB (Question.ofSet vB))ᶜ.info

¬□B is not true: all relevant worlds are burning worlds. Unnecessity Distribution (20) fails.

theorem Booth2022a.Unilateral.bilateral_not_neg_dia_disj (w : Bool × Bool) : w ∉ (MinimalCovering.possibility rB (MinimalCovering.atom vM ⊔ MinimalCovering.atom vB))ᶜ.truth

In the bilateral semantics ¬◇(M ∨ B) is not true in the same scenario: its truth needs a relevant world where both are false.

The facts of the appendix

theorem Booth2022a.box_independence_left {W : Type u_1} {At : Type u_2} {V : At → Set W} {R : W → Set W} {p q : At} (h : IncompRel (fun (x1 x2 : Set W) => x1 ⊆ x2) (V p) (V q)) : (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).box).truth ⊆ (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).conj (MinimalCovering.Formula.atom q).neg).diamond).truth

Fact 1, □(p ∨ q) ⊨ ◇(p ∧ ¬q).

theorem Booth2022a.box_independence_right {W : Type u_1} {At : Type u_2} {V : At → Set W} {R : W → Set W} {p q : At} (h : IncompRel (fun (x1 x2 : Set W) => x1 ⊆ x2) (V p) (V q)) : (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).box).truth ⊆ (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom q).conj (MinimalCovering.Formula.atom p).neg).diamond).truth

Fact 1, □(p ∨ q) ⊨ ◇(q ∧ ¬p).

theorem Booth2022a.dia_independence_left {W : Type u_1} {At : Type u_2} {V : At → Set W} {R : W → Set W} {p q : At} (h : IncompRel (fun (x1 x2 : Set W) => x1 ⊆ x2) (V p) (V q)) : (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).diamond).truth ⊆ (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).conj (MinimalCovering.Formula.atom q).neg).diamond).truth

Fact 1, ◇(p ∨ q) ⊨ ◇(p ∧ ¬q).

theorem Booth2022a.dia_independence_right {W : Type u_1} {At : Type u_2} {V : At → Set W} {R : W → Set W} {p q : At} (h : IncompRel (fun (x1 x2 : Set W) => x1 ⊆ x2) (V p) (V q)) : (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).diamond).truth ⊆ (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom q).conj (MinimalCovering.Formula.atom p).neg).diamond).truth

Fact 1, ◇(p ∨ q) ⊨ ◇(q ∧ ¬p).

theorem Booth2022a.updateAccess_neg_atom {W : Type u_1} {At : Type u_2} {V : At → Set W} {R : W → Set W} (p : At) (w : W) : MinimalCovering.updateAccess R (MinimalCovering.Formula.eval V R (MinimalCovering.Formula.atom p).neg) w = R w \ V p

The accessibility updated by ¬p keeps the relevant worlds where p is false.

theorem Booth2022a.box_conditional_left {W : Type u_1} {At : Type u_2} {V : At → Set W} {R : W → Set W} {p q : At} (h : IncompRel (fun (x1 x2 : Set W) => x1 ⊆ x2) (V p) (V q)) : (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).box).truth ⊆ (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).neg.cond (MinimalCovering.Formula.atom q).box)).truth

Fact 2, □(p ∨ q) ⊨ ¬p → □q.

theorem Booth2022a.box_conditional_right {W : Type u_1} {At : Type u_2} {V : At → Set W} {R : W → Set W} {p q : At} (h : IncompRel (fun (x1 x2 : Set W) => x1 ⊆ x2) (V p) (V q)) : (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).box).truth ⊆ (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom q).neg.cond (MinimalCovering.Formula.atom p).box)).truth

Fact 2, □(p ∨ q) ⊨ ¬q → □p.

theorem Booth2022a.dia_conditional_left {W : Type u_1} {At : Type u_2} {V : At → Set W} {R : W → Set W} {p q : At} (h : IncompRel (fun (x1 x2 : Set W) => x1 ⊆ x2) (V p) (V q)) : (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).diamond).truth ⊆ (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).neg.cond (MinimalCovering.Formula.atom q).diamond)).truth

Fact 2, ◇(p ∨ q) ⊨ ¬p → ◇q.

theorem Booth2022a.dia_conditional_right {W : Type u_1} {At : Type u_2} {V : At → Set W} {R : W → Set W} {p q : At} (h : IncompRel (fun (x1 x2 : Set W) => x1 ⊆ x2) (V p) (V q)) : (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).diamond).truth ⊆ (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom q).neg.cond (MinimalCovering.Formula.atom p).diamond)).truth

Fact 2, ◇(p ∨ q) ⊨ ¬q → ◇p.

theorem Booth2022a.free_choice {W : Type u_1} {At : Type u_2} {V : At → Set W} {R : W → Set W} {p q : At} (h : IncompRel (fun (x1 x2 : Set W) => x1 ⊆ x2) (V p) (V q)) : (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).diamond).truth ⊆ (MinimalCovering.Formula.eval V R (MinimalCovering.Formula.atom p).diamond).truth

Fact 4, Free Choice: ◇(p ∨ q) ⊨ ◇p.

theorem Booth2022a.free_choice_right {W : Type u_1} {At : Type u_2} {V : At → Set W} {R : W → Set W} {p q : At} (h : IncompRel (fun (x1 x2 : Set W) => x1 ⊆ x2) (V p) (V q)) : (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).diamond).truth ⊆ (MinimalCovering.Formula.eval V R (MinimalCovering.Formula.atom q).diamond).truth

Free Choice for the right disjunct, ◇(p ∨ q) ⊨ ◇q.

theorem Booth2022a.box_eq_neg_diamond_neg {W : Type u_1} {At : Type u_2} (V : At → Set W) (R : W → Set W) (φ : MinimalCovering.Formula At) : MinimalCovering.Formula.eval V R φ.box = MinimalCovering.Formula.eval V R φ.neg.diamond.neg

Fact 5, modal duality: [□φ] = [¬◇¬φ].

theorem Booth2022a.diamond_eq_neg_box_neg {W : Type u_1} {At : Type u_2} (V : At → Set W) (R : W → Set W) (φ : MinimalCovering.Formula At) : MinimalCovering.Formula.eval V R φ.diamond = MinimalCovering.Formula.eval V R φ.neg.box.neg

Fact 5, modal duality: [◇φ] = [¬□¬φ].

theorem Booth2022a.impossibility_distribution_left {W : Type u_1} {At : Type u_2} (V : At → Set W) (R : W → Set W) (p q : At) : (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).diamond.neg).truth ⊆ (MinimalCovering.Formula.eval V R (MinimalCovering.Formula.atom p).diamond.neg).truth

Fact 6, Impossibility Distribution: ¬◇(p ∨ q) ⊨ ¬◇p.

theorem Booth2022a.impossibility_distribution_right {W : Type u_1} {At : Type u_2} (V : At → Set W) (R : W → Set W) (p q : At) : (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).diamond.neg).truth ⊆ (MinimalCovering.Formula.eval V R (MinimalCovering.Formula.atom q).diamond.neg).truth

Fact 6, Impossibility Distribution: ¬◇(p ∨ q) ⊨ ¬◇q.

theorem Booth2022a.unnecessity_distribution_left {W : Type u_1} {At : Type u_2} (V : At → Set W) (R : W → Set W) (p q : At) : (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).box.neg).truth ⊆ (MinimalCovering.Formula.eval V R (MinimalCovering.Formula.atom p).box.neg).truth

Fact 7, Unnecessity Distribution: ¬□(p ∨ q) ⊨ ¬□p.

theorem Booth2022a.unnecessity_distribution_right {W : Type u_1} {At : Type u_2} (V : At → Set W) (R : W → Set W) (p q : At) : (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).box.neg).truth ⊆ (MinimalCovering.Formula.eval V R (MinimalCovering.Formula.atom q).box.neg).truth

Fact 7, Unnecessity Distribution: ¬□(p ∨ q) ⊨ ¬□q.

theorem Booth2022a.dual_free_choice {W : Type u_1} {At : Type u_2} {V : At → Set W} {R : W → Set W} {p q : At} (h : IncompRel (fun (x1 x2 : Set W) => x1 ⊆ x2) (V p) (V q)) : (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).conj (MinimalCovering.Formula.atom q)).box.neg).truth ⊆ (MinimalCovering.Formula.eval V R (MinimalCovering.Formula.atom p).neg.diamond).truth

Dual Free Choice (fn. 32): ¬□(p ∧ q) ⊨ ◇¬p, by duality, De Morgan and Free Choice for the negated atoms. Booth notes the inference is controversial and traces it to the De Morgan law for the negative coordinate of conjunction.

Truth-value gaps (§8)

def Booth2022a.IsModalFree {At : Type u_2} : MinimalCovering.Formula At → Prop

The modal-free sentences: those without □ or ◇.

Equations

• Booth2022a.IsModalFree (MinimalCovering.Formula.atom p) = True
• Booth2022a.IsModalFree φ.neg = Booth2022a.IsModalFree φ
• Booth2022a.IsModalFree (φ.conj ψ) = (Booth2022a.IsModalFree φ ∧ Booth2022a.IsModalFree ψ)
• Booth2022a.IsModalFree (φ.disj ψ) = (Booth2022a.IsModalFree φ ∧ Booth2022a.IsModalFree ψ)
• Booth2022a.IsModalFree φ.bang = Booth2022a.IsModalFree φ
• Booth2022a.IsModalFree (φ.cond ψ) = (Booth2022a.IsModalFree φ ∧ Booth2022a.IsModalFree ψ)
• Booth2022a.IsModalFree φ.box = False
• Booth2022a.IsModalFree φ.diamond = False

theorem Booth2022a.isCompl_truth_falsity {W : Type u_1} {At : Type u_2} (V : At → Set W) (R : W → Set W) (φ : MinimalCovering.Formula At) (hφ : IsModalFree φ) : IsCompl (MinimalCovering.Formula.eval V R φ).truth (MinimalCovering.Formula.eval V R φ).falsity

The modal-free fragment is classical (§8): a modal-free sentence is false exactly where it is not true. No sentence is both (BilatInqProp.disjoint_truth_falsity); only modals create gaps.

theorem Booth2022a.ross_gap {W : Type u_1} {At : Type u_2} {V : At → Set W} {R : W → Set W} {p q : At} (h : IncompRel (fun (x1 x2 : Set W) => x1 ⊆ x2) (V p) (V q)) {w : W} (hw : w ∈ (MinimalCovering.Formula.eval V R (MinimalCovering.Formula.atom p).box).truth) : w ∉ (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).box).truth ∧ w ∉ (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).box).falsity

The Ross gap (§8, fn. 35): if □p is true, □(p ∨ q) is neither true nor false.

theorem Booth2022a.free_choice_gap {W : Type u_1} {At : Type u_2} {V : At → Set W} {R : W → Set W} {p q : At} (h : IncompRel (fun (x1 x2 : Set W) => x1 ⊆ x2) (V p) (V q)) {w : W} (hp : w ∈ (MinimalCovering.Formula.eval V R (MinimalCovering.Formula.atom p).diamond).truth) (hq : w ∉ (MinimalCovering.Formula.eval V R (MinimalCovering.Formula.atom q).diamond).truth) : w ∉ (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).diamond).truth ∧ w ∉ (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).diamond).falsity

The Free Choice gap (§8): if p is possible and q is not, ◇(p ∨ q) is neither true (Free Choice would make q possible) nor false (Impossibility Distribution would make p impossible).

theorem Booth2022a.independence_gap {W : Type u_1} {At : Type u_2} {V : At → Set W} {R : W → Set W} {p q : At} (h : IncompRel (fun (x1 x2 : Set W) => x1 ⊆ x2) (V p) (V q)) {w : W} (hp : w ∈ (MinimalCovering.Formula.eval V R (MinimalCovering.Formula.atom p).diamond).truth) (hind : w ∉ (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).conj (MinimalCovering.Formula.atom q).neg).diamond).truth) : w ∉ (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).diamond).truth ∧ w ∉ (MinimalCovering.Formula.eval V R ((MinimalCovering.Formula.atom p).disj (MinimalCovering.Formula.atom q)).diamond).falsity

The Independence gap (§8): if p is possible but not independently of q, ◇(p ∨ q) is neither true nor false. Booth's case, ◇p and ◇q true but ◇(p ∧ ¬q) not, is an instance.

The card game of (12)

The only permitted option is to take the ace and the ten of diamonds together. "You may take the ace or the ten" (12) and its negation (12′) are both untrue.

def Booth2022a.CardGame.val : Bool → Set (Bool × Bool)

Whether the ace, and whether the ten, is taken.

Equations

• Booth2022a.CardGame.val true = {w : Bool × Bool | w.1 = true}
• Booth2022a.CardGame.val false = {w : Bool × Bool | w.2 = true}

def Booth2022a.CardGame.acc : Bool × Bool → Set (Bool × Bool)

The only permitted option: take both.

Equations

• Booth2022a.CardGame.acc x✝ = {(true, true)}

theorem Booth2022a.CardGame.incomp : IncompRel (fun (x1 x2 : Set (Bool × Bool)) => x1 ⊆ x2) (val true) (val false)

theorem Booth2022a.CardGame.gap (w : Bool × Bool) : w ∉ (MinimalCovering.Formula.eval val acc ((MinimalCovering.Formula.atom true).disj (MinimalCovering.Formula.atom false)).diamond).truth ∧ w ∉ (MinimalCovering.Formula.eval val acc ((MinimalCovering.Formula.atom true).disj (MinimalCovering.Formula.atom false)).diamond).falsity

(12) is neither true nor false.

Figures 1 and 2

Four worlds, the valuations of p and q. Where the relevant worlds are the three p ∨ q-worlds, {⟦p⟧, ⟦q⟧} minimally covers them (Figure 2, Independence). Where they are the two p-worlds, the pair is a super cover but not a minimal one (Figure 1): the Diversity inferences hold without the Independence inferences, and the premises □M, ◇P of the extended Ross argument (8) are true while its conclusion is not.

@[reducible, inline]

abbrev Booth2022a.Figures.W4 : Type

Worlds: the truth values of p and q.

Equations

• Booth2022a.Figures.W4 = (Bool × Bool)

def Booth2022a.Figures.vp : Set W4

p is true at the worlds whose first coordinate is true.

Equations

• Booth2022a.Figures.vp = {w : Booth2022a.Figures.W4 | w.1 = true}

def Booth2022a.Figures.vq : Set W4

q is true at the worlds whose second coordinate is true.

Equations

• Booth2022a.Figures.vq = {w : Booth2022a.Figures.W4 | w.2 = true}

def Booth2022a.Figures.val : Bool → Set W4

The valuation: true is p, false is q.

Equations

• Booth2022a.Figures.val true = Booth2022a.Figures.vp
• Booth2022a.Figures.val false = Booth2022a.Figures.vq

def Booth2022a.Figures.r₃ : W4 → Set W4

The relevant worlds are the three p ∨ q-worlds (Figure 2).

Equations

• Booth2022a.Figures.r₃ x✝ = Booth2022a.Figures.vp ∪ Booth2022a.Figures.vq

def Booth2022a.Figures.rP : W4 → Set W4

The relevant worlds are the two p-worlds (Figure 1).

Equations

• Booth2022a.Figures.rP x✝ = Booth2022a.Figures.vp

theorem Booth2022a.Figures.incomp : IncompRel (fun (x1 x2 : Set W4) => x1 ⊆ x2) vp vq

theorem Booth2022a.Figures.incomp_val : IncompRel (fun (x1 x2 : Set W4) => x1 ⊆ x2) (val true) (val false)

The model is admissible for p and q.

theorem Booth2022a.Figures.isMinCover_r₃ : MinimalCovering.IsMinCover {vp, vq} (r₃ (true, true))

Figure 2: {⟦p⟧, ⟦q⟧} minimally covers the three p ∨ q-worlds.

theorem Booth2022a.Figures.diversity_without_independence : MinimalCovering.IsSuperCover {vp, vq} (rP (true, true)) ∧ ¬MinimalCovering.IsMinCover {vp, vq} (rP (true, true))

Figure 1: on the two p-worlds {⟦p⟧, ⟦q⟧} is a super cover but not a minimal one.

theorem Booth2022a.Figures.box_pOrQ : (true, true) ∈ (MinimalCovering.Formula.eval val r₃ ((MinimalCovering.Formula.atom true).disj (MinimalCovering.Formula.atom false)).box).truth

Figure 2: □(p ∨ q) is true.

theorem Booth2022a.Figures.box_p : (true, true) ∈ (MinimalCovering.Formula.eval val rP (MinimalCovering.Formula.atom true).box).truth

Figure 1: □p is true.

theorem Booth2022a.Figures.diamond_q : (true, true) ∈ (MinimalCovering.Formula.eval val rP (MinimalCovering.Formula.atom false).diamond).truth

Figure 1: ◇q is true.

theorem Booth2022a.Figures.not_diamond_qAndNotP : (true, true) ∉ (MinimalCovering.Formula.eval val rP ((MinimalCovering.Formula.atom false).conj (MinimalCovering.Formula.atom true).neg).diamond).truth

Figure 1: ◇(q ∧ ¬p) is not true, so the Diversity inference ◇q holds without its Independence counterpart.

theorem Booth2022a.Figures.extended_ross : (true, true) ∈ (MinimalCovering.Formula.eval val rP (MinimalCovering.Formula.atom true).box).truth ∩ (MinimalCovering.Formula.eval val rP (MinimalCovering.Formula.atom false).diamond).truth ∧ (true, true) ∉ (MinimalCovering.Formula.eval val rP ((MinimalCovering.Formula.atom true).disj (MinimalCovering.Formula.atom false)).box).truth

The extended Ross argument (8) is invalid: □p and ◇q are true on Figure 1, □(p ∨ q) is not.

theorem Booth2022a.Figures.ross_invalid : ¬∀ (W : Type) (r : W → Set W) (v : Bool → Set W), IncompRel (fun (x1 x2 : Set W) => x1 ⊆ x2) (v true) (v false) → (MinimalCovering.Formula.eval v r (MinimalCovering.Formula.atom true).box).truth ⊆ (MinimalCovering.Formula.eval v r ((MinimalCovering.Formula.atom true).disj (MinimalCovering.Formula.atom false)).box).truth

Fact 3: the Ross inference □p ⊭ □(p ∨ q) is not valid over the admissible models; the model of Figure 1 refutes it.

theorem Booth2022a.Figures.not_contraposition : (MinimalCovering.Formula.eval val rP ((MinimalCovering.Formula.atom true).disj (MinimalCovering.Formula.atom false)).box.neg).truth ⊆ (MinimalCovering.Formula.eval val rP (MinimalCovering.Formula.atom true).box.neg).truth ∧ ¬(MinimalCovering.Formula.eval val rP (MinimalCovering.Formula.atom true).box).truth ⊆ (MinimalCovering.Formula.eval val rP ((MinimalCovering.Formula.atom true).disj (MinimalCovering.Formula.atom false)).box).truth

Entailment is not closed under contraposition, the formal content of Booth's "diplomatic resolution" (§8): ¬□(p ∨ q) ⊨ ¬□p (Fact 7) while □p ⊭ □(p ∨ q) (Fact 3).