BSML Pragmatic Enrichment

[Alo22]

Pragmatic enrichment [·]⁺ (Definition 6) adds non-emptiness constraints recursively to every subformula, capturing the "neglect-zero" tendency in human cognition: speakers/hearers ignore empty witness sets.

Key Properties

• Fact 1: Enrichment strengthens — [α]⁺ ⊨ α (support + anti-support) for NE-free α
• Fact 2: Enriched formula entails original plus NE — [α]⁺ ⊨ α ∧ NE for NE-free α
• Fact 9: Enrichment vacuous under single negation — ¬[α]⁺ ≡ ¬α for positive α
• Fact 10: Enrichment NOT vacuous under double negation — ¬¬[p]⁺ ≢ ¬¬p

Architecture

Enrichment is the bridge between BSML's split disjunction (a semantic mechanism) and free choice (a pragmatic inference). The enrichment function transforms a formula so that empty teams are excluded at every level, and the combination with split disjunction forces both disjuncts to have non-empty witnesses — yielding free choice.

def BSML.enrich {Atom : Type u_2} : Formula Atom → Formula Atom

Pragmatic enrichment [·]⁺ (Definition 6 from [Alo22]).

Recursively adds non-emptiness constraints at every level:

• [p]⁺ = p ∧ NE
• [NE]⁺ = NE
• [¬φ]⁺ = ¬[φ]⁺ ∧ NE
• [φ ∧ ψ]⁺ = ([φ]⁺ ∧ [ψ]⁺) ∧ NE
• [φ ∨ ψ]⁺ = ([φ]⁺ ∨ [ψ]⁺) ∧ NE
• [◇φ]⁺ = ◇[φ]⁺ ∧ NE
• [□φ]⁺ = □[φ]⁺ ∧ NE

Equations

• BSML.enrich (BSML.Formula.atom p) = (BSML.Formula.atom p).conj BSML.Formula.ne
• BSML.enrich BSML.Formula.ne = BSML.Formula.ne
• BSML.enrich φ.neg = (BSML.enrich φ).neg.conj BSML.Formula.ne
• BSML.enrich (φ.conj ψ) = ((BSML.enrich φ).conj (BSML.enrich ψ)).conj BSML.Formula.ne
• BSML.enrich (φ.disj ψ) = ((BSML.enrich φ).disj (BSML.enrich ψ)).conj BSML.Formula.ne
• BSML.enrich φ.poss = (BSML.enrich φ).poss.conj BSML.Formula.ne

theorem BSML.enrich_neg_structure {Atom : Type u_2} (φ : Formula Atom) : enrich φ.neg = (enrich φ).neg.conj Formula.ne

theorem BSML.enrich_conj_structure {Atom : Type u_2} (φ ψ : Formula Atom) : enrich (φ.conj ψ) = ((enrich φ).conj (enrich ψ)).conj Formula.ne

theorem BSML.enrich_disj_structure {Atom : Type u_2} (φ ψ : Formula Atom) : enrich (φ.disj ψ) = ((enrich φ).disj (enrich ψ)).conj Formula.ne

theorem BSML.enrich_poss_structure {Atom : Type u_2} (φ : Formula Atom) : enrich φ.poss = (enrich φ).poss.conj Formula.ne

theorem BSML.enriched_support_implies_nonempty {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) (h : support M (enrich φ) t) : t.Nonempty

If an enriched formula is supported, the team is non-empty.

theorem BSML.split_exists {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) (φ ψ : Formula Atom) (t : Finset W) (h : support M (φ.disj ψ) t) : ∃ (t₁ : Finset W) (t₂ : Finset W), support M φ t₁ ∧ support M ψ t₂

If disjunction is supported, there exists a split where both parts support their disjuncts.

theorem BSML.enriched_split_forces_both_nonempty {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) (φ ψ : Formula Atom) (t : Finset W) (h : support M ((enrich φ).disj (enrich ψ)) t) : ∃ (t₁ : Finset W) (t₂ : Finset W), t₁.Nonempty ∧ t₂.Nonempty ∧ support M (enrich φ) t₁ ∧ support M (enrich ψ) t₂

Enriched disjunction forces both parts of split to be non-empty.

theorem BSML.antiSupport_strip_ne {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) (h : antiSupport M (φ.conj Formula.ne) t) : antiSupport M φ t

Anti-support of (φ ∧ NE) implies anti-support of φ. From the SPLIT, one part anti-supports φ and the other (anti-supporting NE) is empty, so the first part is the whole team.

theorem BSML.antiSupport_conj_ne_of_antiSupport {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) (h : antiSupport M φ t) : antiSupport M (φ.conj Formula.ne) t

Anti-support of φ implies anti-support of (φ ∧ NE). Use the trivial split (t, ∅).

theorem BSML.antiSupport_conj_ne_iff {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) : antiSupport M (φ.conj Formula.ne) t ↔ antiSupport M φ t

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

theorem BSML.antiSupport_poss_weaken {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) (φ ψ : Formula Atom) (t : Finset W) (hmono : ∀ (t' : Finset W), antiSupport M φ t' → antiSupport M ψ t') (h : antiSupport M φ.poss t) : antiSupport M ψ.poss t

Anti-support monotonicity for ◇: if antiSupport of φ implies antiSupport of ψ for all teams, then ◇φ anti-support implies ◇ψ anti-support.

theorem BSML.enrichment_strengthens_support {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) (hNE : φ.NEFree) (h : support M (enrich φ) t) : support M φ t

Enrichment strengthens: [α]⁺ ⊨ α (Fact 1 from [Alo22]).

For NE-free α, if a team supports the enriched formula [α]⁺, it also supports the original α.

theorem BSML.enrichment_strengthens_antiSupport {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) (hNE : φ.NEFree) (h : antiSupport M (enrich φ) t) : antiSupport M φ t

Enrichment strengthens (anti-support direction of Fact 1).

theorem BSML.enrichment_entails_conj_ne {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) (hNE : φ.NEFree) (h : support M (enrich φ) t) : support M (φ.conj Formula.ne) t

Fact 2 from [Alo22]: [α]⁺ ⊨ α ∧ NE for NE-free α.

theorem BSML.enrichment_vacuous_under_negation {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) (hPos : φ.Positive) : antiSupport M (enrich φ) t ↔ antiSupport M φ t

Pragmatic enrichment is vacuous under single negation for positive formulas (Fact 9 from [Alo22]).

For positive α (no negation): ¬[α]⁺ ≡ ¬α (both support and anti-support).

theorem BSML.enrichment_vacuous_under_negation_support {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) (hPos : φ.Positive) : support M (enrich φ).neg t ↔ support M φ.neg t

Fact 9, support direction: support M (.neg (enrich φ)) t ↔ support M (.neg φ) t.

def BSML.consequencePlus {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (φ ψ : Formula Atom) : Prop

BSML+ consequence: consequence between enriched formulas. α ⊨{BSML+} β iff [α]⁺ ⊨{BSML} [β]⁺ ([Alo22] §6.3.1).

Equations

• BSML.consequencePlus φ ψ = ∀ (M : ModalLogic.KripkeModel W Atom) (t : Finset W), BSML.support M (BSML.enrich φ) t → BSML.support M (BSML.enrich ψ) t

def BSML.Formula.ClassicalPositive {Atom : Type u_2} (φ : Formula Atom) : Prop

Formula.ClassicalPositive φ holds when φ has no NE and no negation — the fragment on which BSML* and BSML+ consequence coincide.

Equations

• φ.ClassicalPositive = (φ.NEFree ∧ φ.Positive)

@[instance_reducible]

instance BSML.instDecidableClassicalPositive {Atom : Type u_2} (φ : Formula Atom) : Decidable φ.ClassicalPositive

Equations

• BSML.instDecidableClassicalPositive φ = BSML.instDecidableClassicalPositive._aux_1 φ

theorem BSML.negativeFC_star {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) (α β : Formula Atom) (t : Finset W) (h : supportStar M (α.conj β).neg.poss t) : supportStar M α.neg.poss t

Negative free choice in BSML* ([Alo22] Fact 14): ◇¬(α ∧ β) ⊨ ◇¬α in the star system. The conjunction anti-support split requires two non-empty parts, so an accessible team anti-supporting α ∧ β yields a non-empty sub-team anti-supporting α. BSML+ does not validate this inference.

theorem BSML.bsmlStar_iff_bsmlPlus {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (φ ψ : Formula Atom) (hφ : φ.ClassicalPositive) (hψ : ψ.ClassicalPositive) : consequenceStar φ ψ ↔ consequencePlus φ ψ

For classical positive formulas, BSML* and BSML+ consequence coincide (Fact 13 from [Alo22]).

If we restrict to positive formulas without NE or ¬, then ruling out the empty state syntactically (via [·]⁺ enrichment) is equivalent to ruling it out model-theoretically (via BSML* non-empty restriction).

theorem BSML.enrichment_not_vacuous_under_double_negation : ∃ (W : Type) (x : DecidableEq W) (x_1 : Fintype W) (M : ModalLogic.KripkeModel W String) (t : Finset W), support M (Formula.atom "p").neg.neg t ∧ ¬support M (enrich (Formula.atom "p")).neg.neg t

Pragmatic enrichment is NOT vacuous under double negation (Fact 10 from [Alo22]).

While Fact 9 shows ¬[α]⁺ ≡ ¬α for positive α (enrichment is vacuous under single negation), under double negation enrichment has a non-trivial effect: ¬¬[p]⁺ = ¬¬(p ∧ NE) = p ∧ NE ≢ p = ¬¬p.

The counterexample is the empty team: ∅ vacuously supports p but does not support p ∧ NE (the NE conjunct fails).