Documentation

Linglib.Theories.Semantics.BSML.Enrichment

BSML Pragmatic Enrichment #

@cite{aloni-2022}

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 Semantics.BSML.enrich {Atom : Type u_2} :

BSMLFormula Atom → BSMLFormula Atom

Pragmatic enrichment [·]⁺ (Definition 6 from @cite{aloni-2022}).

Recursively adds non-emptiness constraints at every level:

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

Equations

Instances For

theorem Semantics.BSML.enrich_neg_structure {Atom : Type u_2} (φ : BSMLFormula Atom) :

enrich φ.neg = (enrich φ).neg.conj BSMLFormula.ne

theorem Semantics.BSML.enrich_conj_structure {Atom : Type u_2} (φ ψ : BSMLFormula Atom) :

enrich (φ.conj ψ) = ((enrich φ).conj (enrich ψ)).conj BSMLFormula.ne

theorem Semantics.BSML.enrich_disj_structure {Atom : Type u_2} (φ ψ : BSMLFormula Atom) :

enrich (φ.disj ψ) = ((enrich φ).disj (enrich ψ)).conj BSMLFormula.ne

theorem Semantics.BSML.enrich_poss_structure {Atom : Type u_2} (φ : BSMLFormula Atom) :

enrich φ.poss = (enrich φ).poss.conj BSMLFormula.ne

theorem Semantics.BSML.enriched_support_implies_nonempty {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ : BSMLFormula Atom) (t : Finset W) (h : support M (enrich φ) t) :

t.Nonempty

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

theorem Semantics.BSML.split_exists {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ ψ : BSMLFormula 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 Semantics.BSML.enriched_split_forces_both_nonempty {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ ψ : BSMLFormula 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 Semantics.BSML.antiSupport_strip_ne {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ : BSMLFormula Atom) (t : Finset W) (h : antiSupport M (φ.conj BSMLFormula.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 Semantics.BSML.antiSupport_conj_ne_of_antiSupport {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ : BSMLFormula Atom) (t : Finset W) (h : antiSupport M φ t) :

antiSupport M (φ.conj BSMLFormula.ne) t

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

theorem Semantics.BSML.antiSupport_conj_ne_iff {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ : BSMLFormula Atom) (t : Finset W) :

antiSupport M (φ.conj BSMLFormula.ne) t ↔ antiSupport M φ t

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

theorem Semantics.BSML.antiSupport_poss_weaken {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ ψ : BSMLFormula 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 Semantics.BSML.enrichment_strengthens_support {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ : BSMLFormula Atom) (t : Finset W) (hNE : φ.isNEFree = true) (h : support M (enrich φ) t) :

support M φ t

Enrichment strengthens: [α]⁺ ⊨ α (Fact 1 from @cite{aloni-2022}).

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

theorem Semantics.BSML.enrichment_strengthens_antiSupport {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ : BSMLFormula Atom) (t : Finset W) (hNE : φ.isNEFree = true) (h : antiSupport M (enrich φ) t) :

antiSupport M φ t

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

theorem Semantics.BSML.enrichment_entails_conj_ne {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ : BSMLFormula Atom) (t : Finset W) (hNE : φ.isNEFree = true) (h : support M (enrich φ) t) :

support M (φ.conj BSMLFormula.ne) t

Fact 2 from @cite{aloni-2022}: [α]⁺ ⊨ α ∧ NE for NE-free α.

theorem Semantics.BSML.enrichment_vacuous_under_negation {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ : BSMLFormula Atom) (t : Finset W) (hPos : φ.isPositive = true) :

antiSupport M (enrich φ) t ↔ antiSupport M φ t

Pragmatic enrichment is vacuous under single negation for positive formulas (Fact 9 from @cite{aloni-2022}).

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

theorem Semantics.BSML.enrichment_vacuous_under_negation_support {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ : BSMLFormula Atom) (t : Finset W) (hPos : φ.isPositive = true) :

support M (enrich φ).neg t ↔ support M φ.neg t

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

def Semantics.BSML.consequencePlus {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (φ ψ : BSMLFormula Atom) :

BSML+ consequence: consequence between enriched formulas. α ⊨{BSML+} β iff [α]⁺ ⊨{BSML} [β]⁺ (@cite{aloni-2022} §6.3.1).

Equations

One or more equations did not get rendered due to their size.

Instances For

def Semantics.BSML.BSMLFormula.isClassicalPositive {Atom : Type u_2} (φ : BSMLFormula Atom) :

Bool

A formula is classical positive: no NE atom and no negation. These are the formulas for which BSML* and BSML+ consequence coincide (@cite{aloni-2022} Fact 13).

Equations

φ.isClassicalPositive = (φ.isNEFree && φ.isPositive)

Instances For

theorem Semantics.BSML.bsmlStar_iff_bsmlPlus {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (φ ψ : BSMLFormula Atom) (hφ : φ.isClassicalPositive = true) (hψ : ψ.isClassicalPositive = true) :

consequenceStar φ ψ ↔ consequencePlus φ ψ

For classical positive formulas, BSML* and BSML+ consequence coincide (Fact 13 from @cite{aloni-2022}).

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 Semantics.BSML.enrichment_not_vacuous_under_double_negation :

∃ (W : Type) (x : DecidableEq W) (x_1 : Fintype W) (M : BSMLModel W String) (t : Finset W), support M (BSMLFormula.atom "p").neg.neg t ∧ ¬support M (enrich (BSMLFormula.atom "p")).neg.neg t

Pragmatic enrichment is NOT vacuous under double negation (Fact 10 from @cite{aloni-2022}).

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).