Documentation

Linglib.Core.Logic.Modal.BSML.Enrichment

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 #

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.

source
def Core.Logic.Modal.BSML.enrich {Atom : Type u_2} :
BSMLFormula Atom → BSMLFormula 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
Instances For
    source
    theorem Core.Logic.Modal.BSML.enrich_neg_structure {Atom : Type u_2} (φ : BSMLFormula Atom) :
    enrich φ.neg = (enrich φ).neg.conj BSMLFormula.ne
    source
    theorem Core.Logic.Modal.BSML.enrich_conj_structure {Atom : Type u_2} (φ ψ : BSMLFormula Atom) :
    enrich (φ.conj ψ) = ((enrich φ).conj (enrich ψ)).conj BSMLFormula.ne
    source
    theorem Core.Logic.Modal.BSML.enrich_disj_structure {Atom : Type u_2} (φ ψ : BSMLFormula Atom) :
    enrich (φ.disj ψ) = ((enrich φ).disj (enrich ψ)).conj BSMLFormula.ne
    source
    theorem Core.Logic.Modal.BSML.enrich_poss_structure {Atom : Type u_2} (φ : BSMLFormula Atom) :
    enrich φ.poss = (enrich φ).poss.conj BSMLFormula.ne
    source
    theorem Core.Logic.Modal.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.

    source
    theorem Core.Logic.Modal.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.

    source
    theorem Core.Logic.Modal.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.

    source
    theorem Core.Logic.Modal.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.

    source
    theorem Core.Logic.Modal.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, ∅).

    source
    theorem Core.Logic.Modal.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 φ.

    source
    theorem Core.Logic.Modal.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.

    source
    theorem Core.Logic.Modal.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 [Alo22]).

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

    source
    theorem Core.Logic.Modal.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).

    source
    theorem Core.Logic.Modal.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 [Alo22]: [α]⁺ ⊨ α ∧ NE for NE-free α.

    source
    theorem Core.Logic.Modal.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 [Alo22]).

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

    source
    theorem Core.Logic.Modal.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.

    source
    def Core.Logic.Modal.BSML.consequencePlus {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (φ ψ : BSMLFormula Atom) :
    Prop

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Core.Logic.Modal.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 ([Alo22] Fact 13).

      Equations
      Instances For
        source
        theorem Core.Logic.Modal.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 [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).

        source
        theorem Core.Logic.Modal.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 [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).