BSML Free Choice Theorems #
Pragmatic enrichment combined with split disjunction derives free choice inferences. This module proves the core FC results from [Alo22] for arbitrary NE-free formulas.
Key Results #
| Result | Statement |
|---|---|
| Modal Disjunction (Fact 3) | [α ∨ β]⁺ ⊨_S ◇α ∧ ◇β (NE-free α,β; R state-based) |
| Narrow Scope FC (Fact 4) | [◇(α ∨ β)]⁺ ⊨ ◇α ∧ ◇β (NE-free α,β) |
| Wide Scope FC (Fact 5) | [◇α ∨ ◇β]⁺ ⊨ ◇α ∧ ◇β (NE-free α,β; R indisputable) |
| Dual Prohibition (Fact 11) | [¬◇(α ∨ β)]⁺ ⊨ ¬◇α ∧ ¬◇β (NE-free α,β) |
| Double Negation FC (Fact 12) | [¬¬◇(α ∨ β)]⁺ ⊨ ◇α ∧ ◇β (NE-free α,β) |
| Negative FC failure (Fact 14) | ◇¬(α∧β) ⊭{BSML+} ◇¬α; ¬□(α∧β) ⊭{BSML+} ¬□α |
Proof Architecture #
Free choice is DERIVED from three independent principles:
- Split disjunction: team is partitioned for ∨
- NE enrichment: [·]⁺ adds non-emptiness constraints recursively
- NE non-flatness: empty teams fail NE, so both parts must be non-empty
Downward closure of atom and NE primitives #
Atoms are downward-closed. Per-primitive isolation of the atom case of
Core.Logic.Modal.BSML.isLowerSet_support_of_isNEFree.
NE is NOT downward-closed: an inhabited team supports NE but ∅ doesn't.
This is the obstruction that prevents
isFlat_support_of_isNEFree from extending to NE-bearing formulas.
Narrow-scope Free Choice: [◇(α ∨ β)]⁺ ⊨ ◇α ∧ ◇β (for NE-free α, β)
(Fact 4 from [Alo22])
The enriched disjunction inside ◇ splits the accessible subteam into
two non-empty parts (by enrichment + NE). Each part supports its
respective disjunct (by enrichment_strengthens_support), and each
is a subset of R[w] (via the union), yielding ◇α and ◇β.
Wide-scope Free Choice: [◇α ∨ ◇β]⁺ ⊨ ◇α ∧ ◇β (for NE-free α, β with indisputable R)
(Fact 5 from [Alo22])
The disjunction splits t = t₁ ∪ t₂. From t₁ pick w₁ — it has a subteam s_a ⊆ R[w₁] supporting α. By indisputability R[w] = R[w₁] for all w ∈ t, so s_a ⊆ R[w], yielding ◇α at every world. Symmetrically for β.
Modal Disjunction: [α ∨ β]⁺ ⊨_S ◇α ∧ ◇β (for NE-free α, β with state-based R)
(Fact 3 from [Alo22])
Plain disjunction under enrichment, with state-based accessibility, derives possibility of each disjunct — without needing ◇ in the formula. The proof: enriched disjunction splits into two non-empty substates (by enrichment + NE). By state-basedness R[w] = t, so each substate is a non-empty subset of R[w], yielding ◇α and ◇β.
Dual Prohibition: [¬◇(α ∨ β)]⁺ ⊨ ¬◇α ∧ ¬◇β (for NE-free α, β)
(Fact 11 from [Alo22])
Under negation, FC is correctly cancelled: the enriched prohibition
of the disjunction entails prohibition of each disjunct. The proof
strips enrichment from the anti-supported disjuncts using Fact 1
(enrichment_strengthens_antiSupport).
Double Negation FC: [¬¬◇(α ∨ β)]⁺ ⊨ ◇α ∧ ◇β (for NE-free α, β)
(Fact 12 from [Alo22])
Under double negation, FC effects re-emerge. Stripping the enrichment
around ¬ reveals support M (enrich (◇(α∨β))) t (by bilateral negation
swap), and narrow-scope FC (Fact 4) applies.
◇¬(a ∧ b): enriched premise IS supported on the counterexample team.
◇¬a: enriched conclusion is NOT supported on the counterexample team.
Fact 14 (◇ version): ◇¬(α ∧ β) ⊭_{BSML+} ◇¬α. Negative FC does not hold under pragmatic enrichment.
¬□(a ∧ b): enriched premise IS supported on the counterexample team.
¬□a: enriched conclusion is NOT supported on the counterexample team.
Fact 14 (□ version): ¬□(α ∧ β) ⊭_{BSML+} ¬□α. Negative FC with necessity also fails under pragmatic enrichment.