Documentation

Linglib.Theories.Semantics.QBSML.Enrichment

Pragmatic enrichment for QBSML — Aloni & van Ormondt 2023 Definition 4.13 #

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

The first-order extension of BSML's pragmatic enrichment function [·]⁺ (Aloni 2022 Definition 7), adding quantifier cases.

Per Aloni & van Ormondt 2023 Definition 4.13, [·]⁺ recursively inserts NE conjuncts into every clause of an NE-free formula:

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

The intuition (from Aloni 2022'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 behavior-under-negation pattern via the QBSML facts in §5 of Aloni & van Ormondt 2023.

Why this lives in QBSML/ rather than as an extension of BSML's #

BSML's enrich operates on BSMLFormula Atom (no quantifiers, no pred). QBSML's enrich operates on QBSMLFormula Var Pred (with exi/univ and predicate atoms). The two are structurally parallel but operate on distinct formula types. A future unification would parameterise enrichment over an arbitrary "team-semantic formula language" with an NE constructor.

Status #

Slim file: just the recursive definition + enriched_support_implies_nonempty. The substrate FC theorems (universal narrowScopeFC, wideScopeFC, universalFC, etc., parallel to BSML's) are deferred to a future QBSML/FreeChoice.lean. The study file AloniVanOrmondt2023.lean proves facts directly on a concrete model.

source
def Semantics.QBSML.QBSMLFormula.enrich {Var : Type u_1} {Pred : Type u_2} :
QBSMLFormula Var Pred → QBSMLFormula Var Pred

Pragmatic enrichment [·]⁺ for QBSML formulas (Aloni & van Ormondt 2023 Definition 4.13). Recursively conjoins NE to every clause.

Equations
Instances For
    source
    theorem Semantics.QBSML.QBSMLFormula.enrich_pred {Var : Type u_1} {Pred : Type u_2} (P : Pred) (x : Var) :
    (pred P x).enrich = (pred P x).conj ne
    source
    theorem Semantics.QBSML.QBSMLFormula.enrich_neg {Var : Type u_1} {Pred : Type u_2} (φ : QBSMLFormula Var Pred) :
    φ.neg.enrich = φ.enrich.neg.conj ne
    source
    theorem Semantics.QBSML.QBSMLFormula.enrich_conj {Var : Type u_1} {Pred : Type u_2} (φ ψ : QBSMLFormula Var Pred) :
    (φ.conj ψ).enrich = (φ.enrich.conj ψ.enrich).conj ne
    source
    theorem Semantics.QBSML.QBSMLFormula.enrich_disj {Var : Type u_1} {Pred : Type u_2} (φ ψ : QBSMLFormula Var Pred) :
    (φ.disj ψ).enrich = (φ.enrich.disj ψ.enrich).conj ne
    source
    theorem Semantics.QBSML.QBSMLFormula.enrich_poss {Var : Type u_1} {Pred : Type u_2} (φ : QBSMLFormula Var Pred) :
    φ.poss.enrich = φ.enrich.poss.conj ne
    source
    theorem Semantics.QBSML.QBSMLFormula.enrich_exi {Var : Type u_1} {Pred : Type u_2} (x : Var) (φ : QBSMLFormula Var Pred) :
    (exi x φ).enrich = (exi x φ.enrich).conj ne
    source
    theorem Semantics.QBSML.QBSMLFormula.enrich_univ {Var : Type u_1} {Pred : Type u_2} (x : Var) (φ : QBSMLFormula Var Pred) :
    (univ x φ).enrich = (univ x φ.enrich).conj ne
    source
    theorem Semantics.QBSML.enriched_support_implies_nonempty {Var : Type u_1} {Pred : Type u_2} {W : Type u_3} {Domain : 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 : 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.

    source
    theorem Semantics.QBSML.antiSupport_strip_ne {Var : Type u_1} {Pred : Type u_2} {W : Type u_3} {Domain : 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 : antiSupport M (φ.conj QBSMLFormula.ne) s) :
    antiSupport M φ s

    Anti-support of φ ∧ NE implies anti-support of φ on the whole state. The split partitions the state into t₁ ∪ t₂ with antiSupport NE t₂ forcing t₂ = ∅, hence t₁ = s. The QBSML analogue of BSML/Enrichment.antiSupport_strip_ne; the workhorse of every Fact 7-10 derivation in QBSML/FreeChoice.lean and the AvO 2023 study file.

    source
    theorem Semantics.QBSML.antiSupport_conj_ne_of_antiSupport {Var : Type u_1} {Pred : Type u_2} {W : Type u_3} {Domain : 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 : 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.

    source
    theorem Semantics.QBSML.antiSupport_conj_ne_iff {Var : Type u_1} {Pred : Type u_2} {W : Type u_3} {Domain : 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)) :
    antiSupport M (φ.conj QBSMLFormula.ne) s ↔ antiSupport M φ s

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