Booth 2022 — Bilateral inquisitive minimal-cover semantics for □

@cite{booth-2022}

A self-contained study file formalizing the bilateral inquisitive semantics of @cite{booth-2022} for necessity-modal-with-disjunction sentences (□(p ∨ q)). The novel content is the minimal-cover requirement on □'s positive interpretation, which derives the Independence inferences

□(p ∨ q) ⊨ ◇(p ∧ ¬q) and □(p ∨ q) ⊨ ◇(q ∧ ¬p)

(Booth Fact 9). Pure-bilateral analyses without minimal-cover (BSML+, @cite{aloni-2022}) do not derive Independence; pure-inquisitive analyses without bilateral negation (@cite{ciardelli-groenendijk-roelofsen-2018}) do not derive the duality between □ and ◇. Booth's bilateral inquisitive propositions combine both.

Substrate alignment

• Question W (Core/Question/Basic.lean) supplies subset-closed families of states with ∅-membership — Booth Definition 10's P° constraint becomes a Question. BilatInqProp is then paired Questions plus a no-substantive-overlap field.
• Question.declarative is exactly Booth's ↓{·} (Def 11 with a singleton input); Question.info is exactly info(·) (Def 12); Question.alt is exactly alt (Def 13).
• IsBilateral (Core/Logic/Bilateral/Defs.lean) supplies the bilateral-substrate predicate. The BilatInqProp instance is rfl-trivial — bilateral negation is bundled-record swap. This is the sixth consumer of the IsBilateral substrate (BSML, QBSML, BUS, ICDRT, Truthmaker propositions, and now Booth bilateral inquisitive).
• IsMinCover is expressed as Minimal (IsCover · S) C using mathlib's Minimal predicate, mirroring how Question.alt uses Maximal (Booth's alt is the dual of his m-cover).

Out of scope

• The collectivity heuristic of @cite{booth-2022} §4 is a discourse-level proposal not formalized here.
• Booth's restrictor conditional and accessibility-update operator (Definitions 15–16) are out of scope for this initial formalization.
• The general Independence theorem (Booth Fact 9) for arbitrary φ requires Compactness-of-Alternatives over the full BSML language. We prove it for atomic disjunctions (atom Vp ∨ atom Vq) over arbitrary R and W (independence_p_not_q), which captures the structural content. Generalizing to φ ∨ ψ for arbitrary φ, ψ requires a separate Compactness lemma we don't yet have.

§1 Cover and minimal cover (Booth Section 2.1)

Booth's □φ differs from Kratzerian necessity by requiring not just that the alternatives of ⟦φ⟧⁺ cover R(w), but that they form a minimal cover — no proper subset of the alternatives still covers R(w). This is what derives Independence inferences (Fact 9): each alternative must be "needed", so no single alternative dominates.

Expressed via mathlib's Minimal predicate (mirrors Question.alt's use of Maximal — Booth's alt and m-cover are dual instances of the order-theoretic extremality pattern).

def Phenomena.Modality.Studies.Booth2022.IsCover {W : Type u_1} (C : Set (Set W)) (S : Set W) : Prop

Booth §2.1: C covers S iff S ⊆ ⋃C.

Equations

• Phenomena.Modality.Studies.Booth2022.IsCover C S = (S ⊆ ⋃₀ C)

def Phenomena.Modality.Studies.Booth2022.IsMinCover {W : Type u_1} (C : Set (Set W)) (S : Set W) : Prop

Booth §2.1: C is a minimal cover (m-cover) of S iff C covers S and no proper subfamily C' ⊂ C covers S. Expressed via mathlib's Minimal.

Equations

• Phenomena.Modality.Studies.Booth2022.IsMinCover C S = Minimal (fun (X : Set (Set W)) => Phenomena.Modality.Studies.Booth2022.IsCover X S) C

theorem Phenomena.Modality.Studies.Booth2022.IsMinCover.isCover {W : Type u_1} {C : Set (Set W)} {S : Set W} (h : IsMinCover C S) : IsCover C S

§2 Bilateral inquisitive propositions (Booth Def 10)

structure Phenomena.Modality.Studies.Booth2022.BilatInqProp (W : Type u_2) : Type u_2

Booth Def 10: a bilateral inquisitive proposition is a paired pos/neg : Question W with no substantive overlap — only the inconsistent (empty) state may both verify and falsify φ. The subset-closure and ∅-membership requirements (Booth Def 10 bullets 2 and the implicit ∅ ∈ P°) are baked into Question.

• pos : Core.Question W

  Positive interpretation: states verifying the formula.

• neg : Core.Question W

  Negative interpretation: states falsifying the formula.

• no_overlap (s : Set W) : s ∈ self.pos → s ∈ self.neg → s = ∅

  No substantive overlap: pos.props ∩ neg.props ⊆ {∅}. The reverse {∅} ⊆ pos.props ∩ neg.props holds for free since both Questions contain ∅ (Question.contains_empty).

def Phenomena.Modality.Studies.Booth2022.BilatInqProp.negate {W : Type u_1} (φ : BilatInqProp W) : BilatInqProp W

Booth Def 14, ¬-clause: bilateral negation is the bundled-record swap. Self-inverse syntactically (negate (negate φ) = φ by rfl).

Equations

• φ.negate = { pos := φ.neg, neg := φ.pos, no_overlap := ⋯ }

@[simp]

theorem Phenomena.Modality.Studies.Booth2022.BilatInqProp.negate_pos {W : Type u_1} (φ : BilatInqProp W) : φ.negate.pos = φ.neg

@[simp]

theorem Phenomena.Modality.Studies.Booth2022.BilatInqProp.negate_neg {W : Type u_1} (φ : BilatInqProp W) : φ.negate.neg = φ.pos

@[simp]

theorem Phenomena.Modality.Studies.Booth2022.BilatInqProp.negate_negate {W : Type u_1} (φ : BilatInqProp W) : φ.negate.negate = φ

theorem Phenomena.Modality.Studies.Booth2022.BilatInqProp.isBilateral {W : Type u_1} : Core.Logic.Bilateral.IsBilateral (fun (φ : BilatInqProp W) => φ.pos) (fun (φ : BilatInqProp W) => φ.neg) negate

BilatInqProp is a bilateral structure in the sense of Core.Logic.Bilateral.IsBilateral. The instance is rfl-trivial because negate is bundled-record swap. Sixth consumer of the IsBilateral substrate (alongside BSML, QBSML, BUS, ICDRT, Truthmaker BilProp).

def Phenomena.Modality.Studies.Booth2022.BilatInqProp.atom {W : Type u_1} (V : Set W) : BilatInqProp W

Booth Def 14, atomic clause: ⟦p⟧⁺ = ↓{V(p)}, ⟦p⟧⁻ = ↓{W \ V(p)}. Encoded with Question.declarative since ↓{X} = declarative X.

Equations

• Phenomena.Modality.Studies.Booth2022.BilatInqProp.atom V = { pos := Core.Question.declarative V, neg := Core.Question.declarative Vᶜ, no_overlap := ⋯ }

def Phenomena.Modality.Studies.Booth2022.BilatInqProp.disj {W : Type u_1} (φ ψ : BilatInqProp W) : BilatInqProp W

Booth Def 14, ∨-clause: ⟦φ ∨ ψ⟧⁺ = ⟦φ⟧⁺ ∪ ⟦ψ⟧⁺ (inquisitive disjunction at the props level, = Question.⊔); ⟦φ ∨ ψ⟧⁻ = ⟦φ⟧⁻ ∩ ⟦ψ⟧⁻ (= Question.⊓).

Equations

• φ.disj ψ = { pos := φ.pos ⊔ ψ.pos, neg := φ.neg ⊓ ψ.neg, no_overlap := ⋯ }

def Phenomena.Modality.Studies.Booth2022.BilatInqProp.conj {W : Type u_1} (φ ψ : BilatInqProp W) : BilatInqProp W

Booth Def 14, ∧-clause via the derivation ⟦φ ∧ ψ⟧ = ⟦¬(¬φ ∨ ¬ψ)⟧ — direct unfolding gives pos = φ.pos ⊓ ψ.pos, neg = φ.neg ⊔ ψ.neg. The Booth-equivalence conj φ ψ = negate (disj (negate φ) (negate ψ)) holds by rfl.

Equations

• φ.conj ψ = { pos := φ.pos ⊓ ψ.pos, neg := φ.neg ⊔ ψ.neg, no_overlap := ⋯ }

§3 Necessity and possibility (Booth Def 14)

R : W → Set W is the relevant-worlds accessibility relation (equivalent in expressive power to Core.Logic.Intensional.AccessRel W = W → W → Prop; Booth uses the curried W → Set W form throughout his Def 14, which we mirror).

def Phenomena.Modality.Studies.Booth2022.BilatInqProp.necessity {W : Type u_1} (R : W → Set W) (φ : BilatInqProp W) : BilatInqProp W

Booth Def 14, □-clause: ⟦□φ⟧⁺ = ↓{ {w | R(w) ≠ ∅ ∧ alt⁺(⟦φ⟧) m-covers R(w)} }, ⟦□φ⟧⁻ = ↓{ {w | ∃ R' ⊆ R(w), R' ≠ ∅ ∧ alt⁻(⟦φ⟧) m-covers R'} }.

The no-overlap proof structurally inducts via φ.no_overlap: any non-empty state s in both polarities yields a world w ∈ s, hence a witness v ∈ R(w) covered by both alt⁺(φ.pos) and alt⁻(φ.neg) — giving alternatives α ∈ φ.pos.props and β ∈ φ.neg.props containing v. Downward closure gives {v} ∈ φ.pos ∩ φ.neg, contradicting φ.no_overlap.

Equations

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

def Phenomena.Modality.Studies.Booth2022.BilatInqProp.possibility {W : Type u_1} (R : W → Set W) (φ : BilatInqProp W) : BilatInqProp W

Booth Def 14, ◇-clause via duality: ⟦◇φ⟧ = ⟦¬□¬φ⟧.

Equations

• Phenomena.Modality.Studies.Booth2022.BilatInqProp.possibility R φ = (Phenomena.Modality.Studies.Booth2022.BilatInqProp.necessity R φ.negate).negate

§4 Truth and falsity (Booth Def 17)

A world w makes φ true in model (W, R, V) iff {w} ∈ ⟦φ⟧⁺, and false iff {w} ∈ ⟦φ⟧⁻. Since Questions are subset-closed, this is equivalent to ∃ s ∈ ⟦φ⟧°, w ∈ s for a non-empty witness.

def Phenomena.Modality.Studies.Booth2022.isTrue {W : Type u_1} (φ : BilatInqProp W) (w : W) : Prop

Booth Def 17: world w is true at φ iff the singleton {w} verifies φ.

Equations

• Phenomena.Modality.Studies.Booth2022.isTrue φ w = ({w} ∈ φ.pos)

def Phenomena.Modality.Studies.Booth2022.isFalse {W : Type u_1} (φ : BilatInqProp W) (w : W) : Prop

Booth Def 17: world w is false at φ iff the singleton {w} falsifies φ.

Equations

• Phenomena.Modality.Studies.Booth2022.isFalse φ w = ({w} ∈ φ.neg)

theorem Phenomena.Modality.Studies.Booth2022.not_isTrue_and_isFalse {W : Type u_1} (φ : BilatInqProp W) (w : W) : ¬(isTrue φ w ∧ isFalse φ w)

Truth and falsity are mutually exclusive (no world is both true and false), since by no_overlap any state in both polarities is ∅.

theorem Phenomena.Modality.Studies.Booth2022.isTrue_possibility_iff {W : Type u_1} (R : W → Set W) (φ : BilatInqProp W) (w : W) : isTrue (BilatInqProp.possibility R φ) w ↔ ∃ R' ⊆ R w, R'.Nonempty ∧ IsMinCover φ.pos.alt R'

Characterization of isTrue for possibility: world w makes ◇φ true iff there exists a non-empty R' ⊆ R w minimally covered by alt φ.pos. The possibility := negate ∘ necessity ∘ negate derivation cancels the two negations, exposing φ.pos directly. Used to bypass the verbose show block in proofs about possibility.

§5 Per-constructor algebra of alt (Booth Compactness substrate)

Per-constructor equations for Question.alt on BilatInqProp's positive interpretation. Used by the worked example (§6), the general Independence theorem (§7), and downstream Booth Compactness (eq_iSup_declarative_alt_of_exists_alt) consumers. The atomic-case private corollaries (alt_disj_atom_eq_pair, alt_conj_atom_negate_eq_singleton) are derived from the public generalizations.

theorem Phenomena.Modality.Studies.Booth2022.alt_atom_pos {W : Type u_1} (V : Set W) : (BilatInqProp.atom V).pos.alt = {V}

alt of atom V is the singleton {V}. Direct corollary of Question.alt_declarative.

theorem Phenomena.Modality.Studies.Booth2022.alt_negate_pos {W : Type u_1} (φ : BilatInqProp W) : φ.negate.pos.alt = φ.neg.alt

alt of negate φ's positive interpretation is alt of φ's negative interpretation. By definition of negate, structural rfl.

theorem Phenomena.Modality.Studies.Booth2022.alt_necessity_pos {W : Type u_1} (R : W → Set W) (φ : BilatInqProp W) : (BilatInqProp.necessity R φ).pos.alt = {{w : W | (R w).Nonempty ∧ IsMinCover φ.pos.alt (R w)}}

alt of necessity R φ's positive interpretation is the singleton of the witness w-set, since necessity uses Question.declarative.

theorem Phenomena.Modality.Studies.Booth2022.alt_disj_pos_eq_union {W : Type u_1} (φ ψ : BilatInqProp W) (hφψ : ∀ a ∈ φ.pos.alt, a ∉ ψ.pos.props) (hψφ : ∀ b ∈ ψ.pos.alt, b ∉ φ.pos.props) : (φ.disj ψ).pos.alt = φ.pos.alt ∪ ψ.pos.alt

General non-Hurford alt of disjunction: when no φ-alt entails ψ and no ψ-alt entails φ (the "non-Hurford" condition lifted from atoms to arbitrary subformulas), alt (disj φ ψ).pos = alt φ.pos ∪ alt ψ.pos. The atomic case (alt_disj_atom_eq_pair) is a specialization.

§6 Worked example: Independence inference on a 3-world model

A concrete witness that the m-cover semantics derives Booth Fact 9 (Independence Inferences). We work on W₄ = Bool × Bool (subsets of {p, q}), with V p = {(true, _)} and V q = {(_, true)}, and constant accessibility R₃ w := V(p) ∪ V(q) (the 3 worlds where p ∨ q is true).

In this model {V(p), V(q)} minimally covers R₃ w because removing either alternative leaves a gap (V(p) alone misses (false, true); V(q) alone misses (true, false)). Thus □(p ∨ q) is true, and the Vp-only world (true, false) lies in R₃ w, witnessing the existential in ◇(p ∧ ¬q)'s positive-side definition.

@[reducible, inline]

abbrev Phenomena.Modality.Studies.Booth2022.BoothExample.W4 : Type

4-world model: subsets of {p, q} indexed by Bool × Bool.

Equations

• Phenomena.Modality.Studies.Booth2022.BoothExample.W4 = (Bool × Bool)

def Phenomena.Modality.Studies.Booth2022.BoothExample.Vp : Set W4

Valuation: p true at worlds with first coordinate true.

Equations

• Phenomena.Modality.Studies.Booth2022.BoothExample.Vp = {w : Phenomena.Modality.Studies.Booth2022.BoothExample.W4 | w.1 = true}

def Phenomena.Modality.Studies.Booth2022.BoothExample.Vq : Set W4

Valuation: q true at worlds with second coordinate true.

Equations

• Phenomena.Modality.Studies.Booth2022.BoothExample.Vq = {w : Phenomena.Modality.Studies.Booth2022.BoothExample.W4 | w.2 = true}

def Phenomena.Modality.Studies.Booth2022.BoothExample.p_atom : BilatInqProp W4

The atomic bilateral inquisitive propositions for p and q.

Equations

• Phenomena.Modality.Studies.Booth2022.BoothExample.p_atom = Phenomena.Modality.Studies.Booth2022.BilatInqProp.atom Phenomena.Modality.Studies.Booth2022.BoothExample.Vp

def Phenomena.Modality.Studies.Booth2022.BoothExample.q_atom : BilatInqProp W4

Equations

• Phenomena.Modality.Studies.Booth2022.BoothExample.q_atom = Phenomena.Modality.Studies.Booth2022.BilatInqProp.atom Phenomena.Modality.Studies.Booth2022.BoothExample.Vq

def Phenomena.Modality.Studies.Booth2022.BoothExample.p_or_q : BilatInqProp W4

The disjunction p ∨ q.

Equations

• Phenomena.Modality.Studies.Booth2022.BoothExample.p_or_q = Phenomena.Modality.Studies.Booth2022.BoothExample.p_atom.disj Phenomena.Modality.Studies.Booth2022.BoothExample.q_atom

def Phenomena.Modality.Studies.Booth2022.BoothExample.p_and_not_q : BilatInqProp W4

The conjunction p ∧ ¬q.

Equations

• Phenomena.Modality.Studies.Booth2022.BoothExample.p_and_not_q = Phenomena.Modality.Studies.Booth2022.BoothExample.p_atom.conj Phenomena.Modality.Studies.Booth2022.BoothExample.q_atom.negate

def Phenomena.Modality.Studies.Booth2022.BoothExample.R₃ : W4 → Set W4

Constant 3-world accessibility: R₃ w = Vp ∪ Vq, the worlds where p ∨ q is true (excluding (false, false)).

Equations

• Phenomena.Modality.Studies.Booth2022.BoothExample.R₃ x✝ = Phenomena.Modality.Studies.Booth2022.BoothExample.Vp ∪ Phenomena.Modality.Studies.Booth2022.BoothExample.Vq

Pivotal world facts

Question-algebraic helpers (specializations of §5 helpers)

The Independence-witness theorems

theorem Phenomena.Modality.Studies.Booth2022.BoothExample.boothExample_necessity_holds : isTrue (BilatInqProp.necessity R₃ p_or_q) (true, true)

□(p ∨ q) holds at (true, true) in the 3-world model. Both (R₃ w).Nonempty and IsMinCover {Vp, Vq} (Vp ∪ Vq) are discharged: the latter requires that any cover-subset must contain both Vp (witnessed by (true, false) ∈ Vp \ Vq) and Vq (witnessed by (false, true) ∈ Vq \ Vp).

theorem Phenomena.Modality.Studies.Booth2022.BoothExample.boothExample_possibility_holds : isTrue (BilatInqProp.possibility R₃ p_and_not_q) (true, true)

◇(p ∧ ¬q) holds at (true, true) in the 3-world model. The Vp-only world (true, false) witnesses the existential in the possibility's positive-side def: it lies in R₃ (true, true) and {(true, false)} is m-covered by {Vp ∩ Vqᶜ}.

theorem Phenomena.Modality.Studies.Booth2022.BoothExample.boothExample_independence : isTrue (BilatInqProp.necessity R₃ p_or_q) (true, true) ∧ isTrue (BilatInqProp.possibility R₃ p_and_not_q) (true, true)

Independence inference on the 3-world model: □(p ∨ q) and ◇(p ∧ ¬q) are jointly true at (true, true). This is a concrete witness that the m-cover semantics derives Booth Fact 9 — Kratzerian cover semantics on the same model would validate □(p ∨ q) but leave ◇(p ∧ ¬q) underivable.

§7 Compactness equations (Booth Fact 5) per constructor

For each BilatInqProp constructor, the compactness equation (... constructor ...).pos = ⨆ p ∈ alt _.pos, declarative p (and the dual .neg form where it differs). Each proof discharges the ∀ p ∈ Q.props, ∃ q ∈ alt Q, p ⊆ q hypothesis of Question.eq_iSup_declarative_alt_of_exists_alt.

These are the building blocks for proving compactness of any specific BilatInqProp formula. (The fully general statement for arbitrary formulas requires an inductive BSMLFormula type with an interpretation function; that's deferred.)

theorem Phenomena.Modality.Studies.Booth2022.pos_eq_iSup_alt_atom {W : Type u_1} (V : Set W) : (BilatInqProp.atom V).pos = ⨆ p ∈ (BilatInqProp.atom V).pos.alt, Core.Question.declarative p

Compactness equation for atom V's positive interpretation. (atom V).pos = declarative V, with alt = {V}; every prop ⊆ V extends to V trivially.

theorem Phenomena.Modality.Studies.Booth2022.neg_eq_iSup_alt_atom {W : Type u_1} (V : Set W) : (BilatInqProp.atom V).neg = ⨆ p ∈ (BilatInqProp.atom V).neg.alt, Core.Question.declarative p

Dual of pos_eq_iSup_alt_atom for .neg.

theorem Phenomena.Modality.Studies.Booth2022.pos_eq_iSup_alt_negate {W : Type u_1} (φ : BilatInqProp W) (hφ : φ.neg = ⨆ p ∈ φ.neg.alt, Core.Question.declarative p) : φ.negate.pos = ⨆ p ∈ φ.negate.pos.alt, Core.Question.declarative p

Compactness for negate φ's positive interpretation reduces to compactness of φ.neg (since (negate φ).pos = φ.neg by rfl).

theorem Phenomena.Modality.Studies.Booth2022.neg_eq_iSup_alt_negate {W : Type u_1} (φ : BilatInqProp W) (hφ : φ.pos = ⨆ p ∈ φ.pos.alt, Core.Question.declarative p) : φ.negate.neg = ⨆ p ∈ φ.negate.neg.alt, Core.Question.declarative p

Dual of pos_eq_iSup_alt_negate.

theorem Phenomena.Modality.Studies.Booth2022.pos_eq_iSup_alt_necessity {W : Type u_1} (R : W → Set W) (φ : BilatInqProp W) : (BilatInqProp.necessity R φ).pos = ⨆ p ∈ (BilatInqProp.necessity R φ).pos.alt, Core.Question.declarative p

Compactness equation for necessity R φ's positive interpretation: a single declarative whose alt is the singleton witness w-set.

theorem Phenomena.Modality.Studies.Booth2022.alt_necessity_neg {W : Type u_1} (R : W → Set W) (φ : BilatInqProp W) : (BilatInqProp.necessity R φ).neg.alt = {{w : W | ∃ R' ⊆ R w, R'.Nonempty ∧ IsMinCover φ.neg.alt R'}}

The alt of necessity's .neg is the singleton of the existential witness w-set (same shape as alt_necessity_pos with the existential substituted for the m-cover R(w) form).

theorem Phenomena.Modality.Studies.Booth2022.neg_eq_iSup_alt_necessity {W : Type u_1} (R : W → Set W) (φ : BilatInqProp W) : (BilatInqProp.necessity R φ).neg = ⨆ p ∈ (BilatInqProp.necessity R φ).neg.alt, Core.Question.declarative p

Dual of pos_eq_iSup_alt_necessity for .neg.

theorem Phenomena.Modality.Studies.Booth2022.pos_eq_iSup_alt_disj {W : Type u_1} (φ ψ : BilatInqProp W) (hφ : ∀ p ∈ φ.pos.props, ∃ q ∈ φ.pos.alt, p ⊆ q) (hψ : ∀ p ∈ ψ.pos.props, ∃ q ∈ ψ.pos.alt, p ⊆ q) (hφψ : ∀ a ∈ φ.pos.alt, a ∉ ψ.pos.props) (hψφ : ∀ b ∈ ψ.pos.alt, b ∉ φ.pos.props) : (φ.disj ψ).pos = ⨆ p ∈ (φ.disj ψ).pos.alt, Core.Question.declarative p

Compactness for disj φ ψ's positive interpretation under summand pos-compactness + non-Hurford on alts. The alt of the disj is the union of summand alts (alt_disj_pos_eq_union); each prop in the disj's pos comes from one summand's pos and lifts to its alt.

theorem Phenomena.Modality.Studies.Booth2022.pos_eq_iSup_alt_possibility {W : Type u_1} (R : W → Set W) (φ : BilatInqProp W) : (BilatInqProp.possibility R φ).pos = ⨆ p ∈ (BilatInqProp.possibility R φ).pos.alt, Core.Question.declarative p

Compactness for possibility R φ's positive interpretation. Direct via duality: (possibility R φ).pos = (necessity R (negate φ)).neg, and the latter is compact via neg_eq_iSup_alt_necessity.

§8 The Independence inference, general meta-language form (Booth Fact 9)

The headline theorem of @cite{booth-2022}: when p ∨ q is non-Hurford (neither disjunct entails the other), □(p ∨ q) ⊨ ◇(p ∧ ¬q) and □(p ∨ q) ⊨ ◇(q ∧ ¬p).

We prove this for atomic disjunctions atom Vp ∨ atom Vq over an arbitrary accessibility relation R and arbitrary world type W. The proof uses minimality of the {Vp, Vq} cover to derive ∃ v ∈ R w, v ∈ Vp \ Vq — exactly the witness needed for the possibility existential. (Booth Fact 9 in full generality requires Compactness-of-Alternatives over arbitrary φ; the atomic case here captures the structural content for □ on disjunctions of atoms.)

theorem Phenomena.Modality.Studies.Booth2022.independence_p_not_q {W : Type u_1} (R : W → Set W) (Vp Vq : Set W) (h_non_hurford : ¬Vp ⊆ Vq ∧ ¬Vq ⊆ Vp) (w : W) : isTrue (BilatInqProp.necessity R ((BilatInqProp.atom Vp).disj (BilatInqProp.atom Vq))) w → isTrue (BilatInqProp.possibility R ((BilatInqProp.atom Vp).conj (BilatInqProp.atom Vq).negate)) w

Booth Fact 9 (Object-Language Independence, atomic case): when p ∨ q is non-Hurford (¬ Vp ⊆ Vq ∧ ¬ Vq ⊆ Vp), the truth of □(p ∨ q) at w entails the truth of ◇(p ∧ ¬q) at w.

Proof: from IsMinCover {Vp, Vq} (R w), minimality forces {Vq} alone to NOT cover R w (else by Minimal.le_of_le, {Vp, Vq} ⊆ {Vq}, so Vp = Vq, contradicting non-Hurford). Hence ∃ v ∈ R w, v ∉ Vq. Combined with the cover R w ⊆ Vp ∪ Vq, we get v ∈ Vp \ Vq. Then R' := {v} witnesses the existential in ◇(p ∧ ¬q)'s positive-side definition.