Pragmatic enrichment in BSML

This file defines the pragmatic enrichment [·]⁺ of a BSML formula and proves how it interacts with support, negation and the variant BSML*. Enrichment conjoins the non-emptiness atom NE to every subformula, so a team supports an enriched formula only when each subformula is witnessed by a non-empty team. Aloni introduces it to model the neglect-zero tendency, the disposition of language users to disregard models that verify a sentence through an empty witness, and derives the free-choice inferences of Studies/Aloni2022.lean from it. BSML⁺ is BSML with enrichment applied globally, and BSML* is BSML with the empty team removed from the possible states.

Main definitions

• BSML.enrich: the enrichment function [·]⁺.
• BSML.ConsequencePlus: BSML⁺ consequence, consequence between the enriched formulas.

Main results

• BSML.eval_of_eval_enrich: on NE-free formulas enrichment strengthens in both polarities (Fact 1); BSML.support_conj_ne_of_support_enrich is [α]⁺ ⊨ α ∧ NE (Fact 2).
• BSML.antiSupport_enrich_iff: on positive formulas enrichment is vacuous under a single negation (Fact 9).
• BSML.support_neg_enrich_neg_iff, BSML.not_equivalent_neg_neg_enrich: under a double negation it is not (Fact 10).
• BSML.consequenceStar_iff_consequencePlus: BSML* and BSML⁺ consequence coincide on classical positive formulas (Fact 13).
• BSML.negativeFC_star_poss, BSML.negativeFC_star_nec: BSML* validates negative free choice (Fact 14); its failure in BSML⁺ is proved in the study.

Implementation notes

Aloni defines [·]⁺ on the NE-free fragment only. enrich is total and sends NE to itself, and □ abbreviates ¬◇¬, so it has no clause of its own. Fact 1 is one induction over the polarity parameter of BSML.eval, which is the paper's double induction.

References

• [Alo22] Aloni, Logic and Conversation: The Case of Free Choice

Enrichment

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

The pragmatic enrichment [φ]⁺ conjoins NE to every subformula of φ.

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.nonempty_of_support_enrich {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

A team supporting an enriched formula is non-empty.

theorem BSML.antiSupport_conj_ne {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

Only the empty team anti-supports NE, so anti-support of φ ∧ NE reduces to anti-support of φ.

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

[¬¬φ]⁺ and [φ]⁺ have the same support, since the two NE conjuncts added by the negations are absorbed.

Enrichment strengthens (Facts 1 and 2)

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

Enrichment strengthens an NE-free formula in both polarities (Fact 1).

theorem BSML.support_of_support_enrich {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

[α]⁺ ⊨ α for NE-free α, the support half of Fact 1.

theorem BSML.antiSupport_of_antiSupport_enrich {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

The anti-support half of Fact 1.

theorem BSML.support_conj_ne_of_support_enrich {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

[α]⁺ ⊨ α ∧ NE for NE-free α (Fact 2).

Enrichment under negation (Facts 9 and 10)

theorem BSML.antiSupport_enrich_iff {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

Enrichment is vacuous under a single negation, ¬[α]⁺ ≡ ¬α, for positive α (Fact 9).

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

¬[¬φ]⁺ ≡ ¬¬[φ]⁺, the equivalence half of Fact 10.

theorem BSML.not_equivalent_neg_neg_enrich {W : Type u_1} [DecidableEq W] {Atom : Type u_2} {φ : Formula Atom} (hNE : φ.NEFree) : ¬Equivalent (enrich φ).neg.neg φ.neg.neg

Enrichment is not vacuous under a double negation, ¬¬[α]⁺ ≢ ¬¬α for NE-free α (Fact 10). The empty team supports ¬¬α but not ¬¬[α]⁺.

BSML⁺ and BSML* (Facts 13 and 14)

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

BSML⁺ consequence is consequence between the enriched formulas, α ⊨⁺ β iff [α]⁺ ⊨ [β]⁺.

Equations

• BSML.ConsequencePlus φ ψ = BSML.Consequence (BSML.enrich φ) (BSML.enrich ψ)

theorem BSML.support_enrich_iff_supportStar {W : Type u_1} [DecidableEq W] {Atom : Type u_2} {M : ModalLogic.KripkeModel W Atom} {φ : Formula Atom} {t : Finset W} (hNE : φ.NEFree) (hPos : φ.Positive) : support M (enrich φ) t ↔ supportStar M φ t ∧ t.Nonempty

On classical positive formulas, those with neither NE nor negation, support of the enrichment is BSML* support on a non-empty team. The NE conjunct at each subformula is the exclusion of ∅ from each split.

theorem BSML.consequenceStar_iff_consequencePlus {W : Type u_1} [DecidableEq W] {Atom : Type u_2} {φ ψ : Formula Atom} (hφ : φ.NEFree) (hφ' : φ.Positive) (hψ : ψ.NEFree) (hψ' : ψ.Positive) : ConsequenceStar φ ψ ↔ ConsequencePlus φ ψ

BSML* and BSML⁺ consequence coincide on classical positive formulas (Fact 13). Excluding the empty team from the states and excluding it syntactically through [·]⁺ agree.

theorem BSML.negativeFC_star_poss {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (α β : Formula Atom) : ConsequenceStar (α.conj β).neg.poss α.neg.poss

Negative free choice holds in BSML*, ◇¬(α ∧ β) ⊨* ◇¬α (Fact 14). A BSML* anti-support split of α ∧ β has two non-empty parts, and the part anti-supporting α is the witness.

theorem BSML.negativeFC_star_nec {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (α β : Formula Atom) : ConsequenceStar (α.conj β).nec.neg α.nec.neg

The □ form of negative free choice in BSML*, ¬□(α ∧ β) ⊨* ¬□α (Fact 14), by the duality □φ := ¬◇¬φ.