QBSML free-choice facts #
The free-choice, ignorance, distribution and negation facts of QBSML ([AvO23] §5), as universal theorems over arbitrary QBSML models — the framework's account of why pragmatically enriched disjunctions under modals license both disjuncts:
| Fact | Statement |
|---|---|
| 3 | [Pa ∨ Pb]⁺ ⊨_epi ◇Pa ∧ ◇Pb (ignorance, R state-based) |
| 5 | card(s)=1 ⇒ M, s ⊨ [∀x(Px ∨ Qx)]⁺ ⇒ M, s ⊨ ∃xPx ∧ ∃xQx |
| 6 | [∀x(Px ∨ Qx)]⁺ ⊨_epi ∃x◇Px ∧ ∃x◇Qx (distribution◇) |
| 7 | [□(Pa ∨ Pb)]⁺ ⊨ ◇Pa ∧ ◇Pb (□-free choice) |
| 8 | [◇(Pa ∨ Pb)]⁺ ⊨ ◇Pa ∧ ◇Pb (◇-free choice) |
| 9 | [∀x◇(Px ∨ Qx)]⁺ ⊨ ∀x◇Px ∧ ∀x◇Qx (universal FC; [Che09b]) |
| 10 | [¬(Pa ∨ Pb)]⁺ ⊨ ¬Pa ∧ ¬Pb (negation; ignorance disappears) |
plus the quantified □-FC composite [□∃x(α ∨ β)]⁺ ⊨ ◇∃xα ∧ ◇∃xβ
(boxExiFC) behind [Yan23]'s Asher and Heim solutions. Fact 4
(obviation) is a countermodel claim and lives with the concrete model in
Studies/AloniVanOrmondt2023.lean, which instantiates the frame-free facts
(5, 7–10) there; the epistemic Facts 3 and 6 require a state-based R and
stay substrate-level.
Main declarations #
diamond_split— the shared core: an enriched split disjunction supported on a modal pairing yields a non-empty world-set witness for each disjunct.narrowScopeFC,boxFC,universalFC— the free-choice facts.boxExiFC— quantified □-FC ([Yan23] §4.4.3).ignorance,distribution,distributionEpi,negationStrip.
Implementation notes #
- Enrichment strengthens (
enrichment_strengthens_support,Logic/Team/QBSML/Enrichment.lean): the enriched form entails the original on the NE-free fragment. - Diamond split (
diamond_split): the splitt₁ ∪ t₂ = modalLift X gsupports the enriched disjuncts on its pieces; each piece is recovered from its world projection, which serves as theFinset Wwitness. - NE strips:
support_enrich_nec_iffpeels the derived□'s enrichment;antiSupport_strip_nethe remainingNEconjuncts. - Witness reconstruction (
support_exi_of_update_closure,Logic/Team/QBSML/Properties.lean): existential witnesses for the quantified facts.
The negation fact requires no frame condition on R ([AvO23]
page 564 proof of Fact 10: "Assume M, s ⊨ [¬(Pa ∨ Pb)]⁺. It follows that
s ≠ ∅ and M, s ⫤ [Pa ∨ Pb]⁺" — frame conditions on R are not invoked);
Facts 7 and the quantified composite hold with the derived □ even though
its enrichment differs from the paper's primitive [□φ]⁺ = □[φ]⁺ ∧ NE.
The diamond split #
The shared core of the free-choice facts: an enriched split disjunction
supported on a modal pairing yields a non-empty world-set witness for
each disjunct — poss_of_subset_modalLift on each half of the split.
Free choice (Facts 7, 8 and 9) #
Fact 8 (◇-free choice / narrow-scope FC) of [AvO23] (the first-order analogue of [Alo22] Fact 4):
[◇(α ∨ β)]⁺ ⊨ ◇α ∧ ◇β for NE-free α, β.
Projects the diamond clause of the enrichment and applies the per-index
core possFC_on at s.
Fact 9 (universal free choice) of [AvO23], the pattern attested experimentally by [Che09b]:
[∀x◇(α ∨ β)]⁺ ⊨ ∀x◇α ∧ ∀x◇β for NE-free α, β.
The enriched premise evaluates the enriched diamond at the universal
extension s[x], so the conclusion is possFC_on at s[x] — the same
per-index argument as Fact 8, one extension up.
Fact 7 (□-free choice) of [AvO23]:
[□(α ∨ β)]⁺ ⊨ ◇α ∧ ◇β for NE-free α, β.
□ is derived (Formula.nec), so the enrichment here is the
negation-clause enrichment of ¬◇¬(α ∨ β) rather than the paper's
primitive [□φ]⁺ = □[φ]⁺ ∧ NE — but the fact holds all the same:
support_enrich_nec_iff puts the enriched disjunction on each index's
full accessible lift R(wᵢ)[gᵢ], and diamond_split produces the
witnesses.
Quantified □-free choice #
[□∃x(α ∨ β)]⁺ ⊨ ◇∃xα ∧ ◇∃xβ — the composite of Fact 7 with an
existential under the modal, which is the form [Yan23]'s Asher and Heim
solutions invoke (its §4.4.3; see Studies/Yan2023.lean).
Quantified □-free choice: [□∃x(α ∨ β)]⁺ ⊨ ◇∃xα ∧ ◇∃xβ for
NE-free α, β. The shape behind [Yan23]'s Asher and Heim
solutions: the enriched premise puts the enriched split disjunction on
each index's full accessible lift's functional extension; each
non-empty half yields a ◇∃x-witness by
poss_exi_of_subset_extendFunctional.
Ignorance (Fact 3) #
Fact 3 (ignorance) of [AvO23]: on epistemic models
(state-based R),
[Pc₁ ∨ Qc₂]⁺ ⊨_epi ◇Pc₁ ∧ ◇Qc₂.
Stated for constant atoms, as in the paper's Pa ∨ Pb: the transplant
argument of poss_predc_of_stateBased needs assignment-invariance —
with a free variable in place of the constant the statement is false
(the transplanted indices carry the wrong assignments).
Negation behaviour (Fact 10) #
Fact 10 (negation behaviour) of [AvO23]:
[¬(α ∨ β)]⁺ ⊨ ¬α ∧ ¬β for NE-free α, β.
Three NE-strips compose: outer (¬enrich(α ∨ β)) ∧ NE, then disj-anti
splits to (antiSupport enrich α) ∧ (antiSupport enrich β), then
enrichment_strengthens_antiSupport for each disjunct.
No frame condition on R — the proof goes through for every model.
Negation cancels ignorance (paper §5.5): the Nonempty hypothesis is
discharged by the three NE-strips, leaving classical anti-support on
each disjunct.
Distribution (Facts 5 and 6) #
Fact 5 (distribution at maximal information) of
[AvO23]: on a state of maximal information
(card s = 1, here s = {i}),
[∀x(α ∨ β)]⁺ ⊨ ∃xα ∧ ∃xβ for NE-free α, β.
The enriched premise splits the universal extension {i}[x] into
non-empty parts supporting the enriched disjuncts; because the state is
a singleton, every part extends the same index, so each part is the
image of a functional extension witnessing the existential.
Fact 6 (distribution◇) of [AvO23]: on epistemic
models (state-based R),
[∀x(Px ∨ Qx)]⁺ ⊨ ∃x◇Px ∧ ∃x◇Qx.
Stated for atoms, as in the paper (the proof evaluates the atom pointwise at a single transplanted world; the paper notes the result "can easily be generalised", which for arbitrary NE-free formulas would route through flatness).