QBSML free-choice theorems — Aloni & van Ormondt 2023 §5

@cite{aloni-vanormondt-2023} @cite{aloni-2022}

The first-order analogues of BSML/FreeChoice.lean's theorems. Pragmatic enrichment (Aloni & van Ormondt 2023 Definition 4.13) combined with split disjunction (§3.1) and bilateral evaluation (§4) derives ignorance, free-choice, distribution, obviation, and behaviour-under-negation inferences as universal substrate facts — applicable to any QBSML model satisfying the relevant frame conditions.

Status

This file currently lands the negation fact (Fact 10) as a universal substrate theorem, plus the enrichment_strengthens_* engine that powers the rest of the §5 facts. Future additions:

• narrowScopeFC_Q (Fact 8) — needs world-projection lemmas for State.modalLift
• universalFC_Q (Fact 9) — needs State.extendUniversal lemmas + the modal pattern from narrowScopeFC_Q
• modalDisjunction_Q (Fact 3) — needs state-based frame condition handling
• The wide-scope variants

The negation fact is the cleanest standalone result — it requires no frame condition on R (Aloni & van Ormondt 2023 page 564 proof: "We assume that M, s ⊨ [¬(Pa ∨ Pb)]⁺. This means that s ≠ ∅ and M, s ⊧ [Pa ∨ Pb]⁺. ..." — frame conditions on R are not invoked).

Proof architecture (mirrors BSML/FreeChoice.lean)

1. Joint enrichment-strengthens (enrichment_strengthens_both): simultaneous induction on QBSMLFormula proving both support enrich φ → support φ and antiSupport enrich φ → antiSupport φ for NE-free φ. The mutual structure handles negation: support (¬ψ) = antiSupport ψ, so the two directions interleave.

2. Negation strip (negationStrip_Q): for NE-free α, β, [¬(α ∨ β)]⁺ ⊨ ¬α ∧ ¬β. Composes antiSupport_strip_ne (in Enrichment.lean) with the antiSupport-disj clause and enrichment_strengthens_antiSupport.

theorem Semantics.QBSML.enrichment_strengthens_support {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} {Pred : Type u_4} [DecidableEq W] [Fintype W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : QBSMLModel W Domain Pred) (φ : QBSMLFormula Var Pred) (s : Finset (Index W Var Domain)) (hNE : φ.isNEFree = true) (h : support M φ.enrich s) : support M φ s

Enrichment strengthens (support direction) — Aloni 2022 Fact 1 extended to QBSML. For NE-free φ, supporting the enriched form implies supporting the original.

theorem Semantics.QBSML.enrichment_strengthens_antiSupport {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} {Pred : Type u_4} [DecidableEq W] [Fintype W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : QBSMLModel W Domain Pred) (φ : QBSMLFormula Var Pred) (s : Finset (Index W Var Domain)) (hNE : φ.isNEFree = true) (h : antiSupport M φ.enrich s) : antiSupport M φ s

Enrichment strengthens (anti-support direction).

theorem Semantics.QBSML.negationStrip_Q {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} {Pred : Type u_4} [DecidableEq W] [Fintype W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : QBSMLModel W Domain Pred) (α β : QBSMLFormula Var Pred) (s : Finset (Index W Var Domain)) (hα : α.isNEFree = true) (hβ : β.isNEFree = true) (h : support M (α.disj β).neg.enrich s) : support M α.neg s ∧ support M β.neg s

Fact 10 (negation behaviour) of @cite{aloni-vanormondt-2023}:

[¬(α ∨ β)]⁺ ⊨ ¬α ∧ ¬β 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.

theorem Semantics.QBSML.narrowScopeFC_Q {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} {Pred : Type u_4} [DecidableEq W] [Fintype W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : QBSMLModel W Domain Pred) (α β : QBSMLFormula Var Pred) (s : Finset (Index W Var Domain)) (hα : α.isNEFree = true) (hβ : β.isNEFree = true) (h : support M (α.disj β).poss.enrich s) : support M α.poss s ∧ support M β.poss s

Fact 8 (◇-free choice / narrow-scope FC) of @cite{aloni-vanormondt-2023} (the first-order analogue of @cite{aloni-2022} Fact 4):

[◇(α ∨ β)]⁺ ⊨ ◇α ∧ ◇β for NE-free α, β.

Per-index i ∈ s: the enriched ◇ provides a non-empty X ⊆ R(i.world) with split t₁ ∪ t₂ = modalLift X i.assign, each part supporting the enriched disjunct on its piece. Project each piece's worlds back via s.image Prod.fst and use modalLift_image_fst_subset to recover a Finset W witness. enrichment_strengthens_support discharges the enrichment to plain support of α, β.