Free choice from neglect-zero in BSML #
Aloni derives free-choice inferences from a neglect-zero tendency. Her pragmatic enrichment
[·]⁺ (BSML.enrich) conjoins NE to every subformula, so an enriched split disjunction needs
two non-empty witnesses, and under a possibility modal each witness is a live option. The paper's
free-choice facts are proved here for arbitrary NE-free α β, and its figures are checked by
decide on its four worlds w_∅, w_a, w_b, w_ab, each the set of atoms true at it, whose
running state is {w_a, w_b}.
Main results #
modalDisjunction,narrowScopeFC,wideScopeFC,dualProhibition,doubleNegationFC: Facts 3, 4, 5, 11 and 12.epistemicContradiction: the epistemic contradiction of §4.1.not_forall_support_neg_of_forall_disjoint: incompatibility does not define negation.not_negativeFC_poss,not_negativeFC_nec: BSML⁺ fails Negative FC (Fact 14).positiveFC_plus,not_positiveFC,addition,not_addition_plus,contraposition,not_contraposition_plus: Table 5's comparison of BSML∅ with BSML⁺.
Implementation notes #
Facts 1, 2, 9, 10, 13 and the BSML* half of Fact 14 are in Logic/Team/BSML/Enrichment.lean,
Facts 6–8 in Logic/Team/BSML/Negation.lean, and Fact 15 in Logic/Team/BSML/Classical.lean.
The first-order extension of §6.2, which Aloni and van Ormondt develop, and the BSML◇ conjecture
of §7 beyond its countermodel (63b) are out of scope.
References #
Free-choice facts #
An enriched split disjunction has a non-empty witness subteam for each disjunct,
[α ∨ β]⁺ ⊨ (α ∧ NE) ∨ (β ∧ NE).
Modal Disjunction (Fact 3) is [α ∨ β]⁺ ⊨ ◇α ∧ ◇β on a state-based R.
Narrow Scope FC (Fact 4) is [◇(α ∨ β)]⁺ ⊨ ◇α ∧ ◇β.
Free choice for logically dependent disjuncts is
[◇(α ∨ (α ∧ β))]⁺ ⊨ ◇α ∧ ◇(α ∧ β).
Wide Scope FC (Fact 5) is [◇α ∨ ◇β]⁺ ⊨ ◇α ∧ ◇β on an indisputable R.
Dual Prohibition (Fact 11) is [¬◇(α ∨ β)]⁺ ⊨ ¬◇α ∧ ¬◇β.
Double Negation (Fact 12) is [¬¬◇(α ∨ β)]⁺ ⊨ ◇α ∧ ◇β.
Epistemic contradiction (§4.1) says that on a state-based R, ◇φ ∧ ¬φ is supported
only by ∅, the sole team supporting the weak contradiction ⊥.
The four-world illustrations #
A world of the paper's figures is the set of atoms true at it: w_a is "a world where only a
is true, w_b only b, etc." (fn. 11, p. 5:14), so w_∅, w_a, w_b, w_ab are ∅, {a},
{b}, {a, b} and an atom holds at a world by membership. Each figNx fixes the accessibility
arrows drawn in Figure N(x), worlds without arrows seeing ∅.
Equations
- Aloni2022.instDecidableEqAtom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- Aloni2022.instFintypeAtom = { elems := { val := ↑Aloni2022.Atom.enumList, nodup := Aloni2022.Atom.enumList_nodup }, complete := Aloni2022.instFintypeAtom._proof_1 }
model R is the paper's Kripke model on the four worlds with accessibility R.
Equations
- Aloni2022.model R = { access := R, val := fun (p : Aloni2022.Atom) (w : Finset Aloni2022.Atom) => p ∈ w }
Instances For
Figures 1–2 draw no arrows, so only atoms and disjunction are evaluated.
Equations
- Aloni2022.propositional = Aloni2022.model fun (x : Finset Aloni2022.Atom) => ∅
Instances For
Figure 3(a) has R[w_a] = R[w_b] = {w_ab, w_∅}.
Equations
- Aloni2022.fig3a = Aloni2022.model fun (w : Finset Aloni2022.Atom) => if w ∈ Aloni2022.state then {{Aloni2022.Atom.a, Aloni2022.Atom.b}, ∅} else ∅
Instances For
Figure 3(b) has R[w_a] = R[w_b] = {w_a, w_b}.
Equations
- Aloni2022.fig3b = Aloni2022.model fun (w : Finset Aloni2022.Atom) => if w ∈ Aloni2022.state then Aloni2022.state else ∅
Instances For
Figure 3(c) has R[w_a] = {w_ab}, R[w_b] = {w_a, w_∅}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Figure 4(a) has R[w_ab] = {w_a}.
Equations
- Aloni2022.fig4a = Aloni2022.model fun (w : Finset Aloni2022.Atom) => if w = {Aloni2022.Atom.a, Aloni2022.Atom.b} then {{Aloni2022.Atom.a}} else ∅
Instances For
Figure 4(b) has R[w_ab] = {w_a, w_b}.
Equations
- Aloni2022.fig4b = Aloni2022.model fun (w : Finset Aloni2022.Atom) => if w = {Aloni2022.Atom.a, Aloni2022.Atom.b} then Aloni2022.state else ∅
Instances For
Figure 5(a) has R[w_a] = R[w_b] = {w_b}.
Equations
- Aloni2022.fig5a = Aloni2022.model fun (w : Finset Aloni2022.Atom) => if w ∈ Aloni2022.state then {{Aloni2022.Atom.b}} else ∅
Instances For
Figure 5(b) has R[w_a] = {w_a}, R[w_b] = {w_b}.
Equations
- Aloni2022.fig5b = Aloni2022.model fun (w : Finset Aloni2022.Atom) => if w ∈ Aloni2022.state then {w} else ∅
Instances For
Negation and incompatibility #
Incompatibility does not define negation, so the converse of Fact 7 fails (p. 5:31). The
state {w_b} is disjoint from every team supporting ¬((a ∧ NE) ∨ b) but does not support
its negation, since a is no open possibility in {w_b}.
Negative free choice (Fact 14) #
BSML⁺ validates neither ◇¬(α ∧ β) ⊨ ◇¬α nor ¬□(α ∧ β) ⊨ ¬□α — the paper's
(50), "Mary might not speak both Arabic and Bengali" ⇏ "she might not speak
Arabic". The countermodel is Figure 5(b)'s frame at the state {w_a}: inside
[¬(a ∧ b)]⁺ a zero witness anti-supports a, but no non-empty subteam of
R[w_a] = {w_a} anti-supports a. BSML* validates both inferences
(BSML.negativeFC_star_poss, BSML.negativeFC_star_nec).
The □ form follows from the ◇ form by the duality □φ := ¬◇¬φ.
BSML∅ against BSML⁺ (Table 5) #
Table 5 sets the NE-free fragment BSML∅, whose consequence is classical
(BSML.consequence_iff_classicalConsequence, Fact 15), against BSML⁺: Positive FC
holds only in BSML⁺, while Addition α ⊨ α ∨ β and Contraposition hold only in BSML∅.
The BSML∅ failure of Positive FC is Figure 4(a); the BSML⁺ failures are refuted on
Figure 5(a)'s frame and on the arrow-free model, the failing contrapositive being that
of Positive FC itself.
Positive FC holds in BSML⁺, ◇(α ∨ β) ⊨⁺ ◇α ∧ ◇β.
Positive FC fails in BSML∅, since Figure 4(a) supports ◇(a ∨ b) but not ◇b.
Addition holds in BSML∅, α ⊨ α ∨ β for NE-free α β, classically.
Addition fails in BSML⁺, [a]⁺ ⊭ [a ∨ b]⁺ at the zero-model {w_a}, where b has
no non-empty witness.
Contraposition holds in BSML∅, so for NE-free α β, α ⊨ β gives ¬β ⊨ ¬α.
Contraposition fails in BSML⁺. Positive FC holds, but its contrapositive
¬(◇a ∧ ◇b) ⊨⁺ ¬◇(a ∨ b) fails at {w_a} on Figure 5(a)'s frame, where R[w_a] = {w_b}
anti-supports a but not a ∨ b.