Pragmatic enrichment for QBSML

[AvO23] [Alo22]

The first-order extension of BSML's pragmatic enrichment function [·]⁺ ([Alo22] Definition 6), adding quantifier cases. Per [AvO23] Definition 4.13, [·]⁺ recursively inserts NE conjuncts into every clause of an NE-free formula:

[Pt₁...tₙ]⁺  =  Pt₁...tₙ ∧ NE
[¬φ]⁺        =  ¬[φ]⁺ ∧ NE
[φ ∧ ψ]⁺     =  ([φ]⁺ ∧ [ψ]⁺) ∧ NE
[φ ∨ ψ]⁺     =  ([φ]⁺ ∨ [ψ]⁺) ∧ NE
[◇φ]⁺        =  ◇[φ]⁺ ∧ NE
[∃xφ]⁺       =  ∃x[φ]⁺ ∧ NE
[∀xφ]⁺       =  ∀x[φ]⁺ ∧ NE

(□ is derived as ¬◇¬, so it carries no separate enrichment clause here.)

The intuition ([Alo22]'s "neglect-zero" hypothesis): conversational participants systematically ignore empty configurations when interpreting, so each clause must witness a non-empty state. Combined with split disjunction, this derives ignorance, distribution, free choice, and the behaviour-under-negation pattern — the QBSML free-choice facts of Core/Logic/Modal/QBSML/FreeChoice.lean.

Main declarations

• QBSMLFormula.enrich — the enrichment function [·]⁺.
• enriched_support_implies_nonempty — a state supporting an enriched formula is non-empty (the NE conjunct guards every clause).
• antiSupport_strip_ne, antiSupport_conj_ne_iff — anti-support of φ ∧ NE reduces to anti-support of φ; the workhorse of the free-choice derivations.
• enrichment_strengthens_support, enrichment_strengthens_antiSupport — [Alo22] Fact 1 extended to QBSML: on the NE-free fragment, the enriched form entails the original, bilaterally.
• support_enrich_nec_iff — support of the enriched derived □ unfolds to pointwise enriched support at the accessible lifts, plus non-emptiness.

Implementation notes

enrich is total on QBSMLFormula for definitional convenience, but [·]⁺ is defined only on the NE-free fragment in both papers, so the .ne case is a filler convention. The construction is structurally identical to BSML's Core/Logic/Modal/BSML/Enrichment.lean but operates on QBSMLFormula Var Const Pred (quantifiers, predicate atoms) rather than BSMLFormula Atom. The two are kept parallel rather than unified: a shared "team-semantic formula language with an NE constructor" abstraction awaits a third instance, per the family roadmap in Core/Logic/Team/Algebra.lean.

The enrichment function

def Core.Logic.Modal.QBSML.QBSMLFormula.enrich {Var : Type u_1} {Const : Type u_2} {Pred : Type u_3} : QBSMLFormula Var Const Pred → QBSMLFormula Var Const Pred

Pragmatic enrichment [·]⁺ for QBSML formulas ([AvO23] Definition 4.13). Recursively conjoins NE to every clause.

Equations

• (Core.Logic.Modal.QBSML.QBSMLFormula.pred P x_1).enrich = (Core.Logic.Modal.QBSML.QBSMLFormula.pred P x_1).conj Core.Logic.Modal.QBSML.QBSMLFormula.ne
• (Core.Logic.Modal.QBSML.QBSMLFormula.predc P c).enrich = (Core.Logic.Modal.QBSML.QBSMLFormula.predc P c).conj Core.Logic.Modal.QBSML.QBSMLFormula.ne
• Core.Logic.Modal.QBSML.QBSMLFormula.ne.enrich = Core.Logic.Modal.QBSML.QBSMLFormula.ne
• φ.neg.enrich = φ.enrich.neg.conj Core.Logic.Modal.QBSML.QBSMLFormula.ne
• (φ.conj ψ).enrich = (φ.enrich.conj ψ.enrich).conj Core.Logic.Modal.QBSML.QBSMLFormula.ne
• (φ.disj ψ).enrich = (φ.enrich.disj ψ.enrich).conj Core.Logic.Modal.QBSML.QBSMLFormula.ne
• φ.poss.enrich = φ.enrich.poss.conj Core.Logic.Modal.QBSML.QBSMLFormula.ne
• (Core.Logic.Modal.QBSML.QBSMLFormula.exi x_1 φ).enrich = (Core.Logic.Modal.QBSML.QBSMLFormula.exi x_1 φ.enrich).conj Core.Logic.Modal.QBSML.QBSMLFormula.ne
• (Core.Logic.Modal.QBSML.QBSMLFormula.univ x_1 φ).enrich = (Core.Logic.Modal.QBSML.QBSMLFormula.univ x_1 φ.enrich).conj Core.Logic.Modal.QBSML.QBSMLFormula.ne

Enriched support forces non-emptiness

theorem Core.Logic.Modal.QBSML.enriched_support_implies_nonempty {Var : Type u_1} {Const : Type u_2} {Pred : Type u_3} {W : Type u_4} {Domain : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : QBSMLModel W Domain Const Pred) (φ : QBSMLFormula Var Const Pred) (s : Finset (Index W Var Domain)) (h : support M φ.enrich s) : s.Nonempty

A QBSML state supporting an enriched formula must be non-empty. The NE conjunct guards every clause of enrich φ, forcing the witnessing state to satisfy Nonempty.

Stripping NE from anti-support

theorem Core.Logic.Modal.QBSML.antiSupport_strip_ne {Var : Type u_1} {Const : Type u_2} {Pred : Type u_3} {W : Type u_4} {Domain : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : QBSMLModel W Domain Const Pred) (φ : QBSMLFormula Var Const Pred) (s : Finset (Index W Var Domain)) (h : antiSupport M (φ.conj QBSMLFormula.ne) s) : antiSupport M φ s

Anti-support of φ ∧ NE implies anti-support of φ. The split partitions the state as t₁ ∪ t₂ with antiSupport NE t₂ forcing t₂ = ∅, hence t₁ = s. The QBSML analogue of BSML/Enrichment's antiSupport_strip_ne; the workhorse of the free-choice derivations in Studies/AloniVanOrmondt2023.lean.

theorem Core.Logic.Modal.QBSML.antiSupport_conj_ne_of_antiSupport {Var : Type u_1} {Const : Type u_2} {Pred : Type u_3} {W : Type u_4} {Domain : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : QBSMLModel W Domain Const Pred) (φ : QBSMLFormula Var Const Pred) (s : Finset (Index W Var Domain)) (h : antiSupport M φ s) : antiSupport M (φ.conj QBSMLFormula.ne) s

Anti-support of φ implies anti-support of φ ∧ NE via the trivial split (s, ∅). The reverse direction of antiSupport_strip_ne.

theorem Core.Logic.Modal.QBSML.antiSupport_conj_ne_iff {Var : Type u_1} {Const : Type u_2} {Pred : Type u_3} {W : Type u_4} {Domain : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : QBSMLModel W Domain Const Pred) (φ : QBSMLFormula Var Const Pred) (s : Finset (Index W Var Domain)) : antiSupport M (φ.conj QBSMLFormula.ne) s ↔ antiSupport M φ s

Anti-support of φ ∧ NE ↔ anti-support of φ.

Enrichment strengthens (joint bilateral induction)

theorem Core.Logic.Modal.QBSML.enrichment_strengthens_support {Var : Type u_1} {Const : Type u_2} {Pred : Type u_3} {W : Type u_4} {Domain : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : QBSMLModel W Domain Const Pred) (φ : QBSMLFormula Var Const Pred) (s : Finset (Index W Var Domain)) (hNE : φ.IsNEFree) (h : support M φ.enrich s) : support M φ s

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

theorem Core.Logic.Modal.QBSML.enrichment_strengthens_antiSupport {Var : Type u_1} {Const : Type u_2} {Pred : Type u_3} {W : Type u_4} {Domain : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : QBSMLModel W Domain Const Pred) (φ : QBSMLFormula Var Const Pred) (s : Finset (Index W Var Domain)) (hNE : φ.IsNEFree) (h : antiSupport M φ.enrich s) : antiSupport M φ s

Enrichment strengthens (anti-support direction).

The enriched derived □

theorem Core.Logic.Modal.QBSML.support_enrich_nec_iff {Var : Type u_1} {Const : Type u_2} {Pred : Type u_3} {W : Type u_4} {Domain : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : QBSMLModel W Domain Const Pred) (φ : QBSMLFormula Var Const Pred) (s : Finset (Index W Var Domain)) : support M φ.nec.enrich s ↔ (∀ i ∈ s, support M φ.enrich (State.modalLift (M.access i.world) i.assign)) ∧ s.Nonempty

Support of the enriched derived □ is pointwise enriched support at the full accessible lifts, plus non-emptiness: the two NE-strips that peel [□φ]⁺ = [¬◇¬φ]⁺ down to [φ]⁺ at each R(wᵢ)[gᵢ], packaged once for the □-free-choice derivations (Core/Logic/Modal/QBSML/FreeChoice.lean).