BSML Free Choice Theorems #

@cite{aloni-2022}

Pragmatic enrichment and free choice derivations in BSML.

Key Results #

Result	Statement
Narrow Scope FC	[◇(α ∨ β)]⁺ ⊨ ◇α ∧ ◇β
Wide Scope FC	[◇α ∨ ◇β]⁺ ⊨ ◇α ∧ ◇β (if R indisputable)
Dual Prohibition	[¬◇(α ∨ β)]⁺ ⊨ ¬◇α ∧ ¬◇β

Proof Architecture #

Free choice is DERIVED from three independent principles:

Split disjunction: team is partitioned for ∨
NE enrichment: [·]⁺ adds non-emptiness constraints recursively
NE non-flatness: empty teams fail NE, so both parts must be non-empty

source

def Semantics.Dynamic.BSML.isFlat {W : Type u_1} (prop : TeamSemantics.Team W → Bool) (worlds : List W) :

Prop

A team proposition is flat if support is downward closed under subset

Equations

Semantics.Dynamic.BSML.isFlat prop worlds = ∀ (t t' : Semantics.Dynamic.TeamSemantics.Team W), t'.subset t worlds = true → prop t = true → prop t' = true

Instances For

source

theorem Semantics.Dynamic.BSML.atom_is_flat {W : Type u_1} [DecidableEq W] (M : BSMLModel W) (p : String) :

isFlat (fun (t : TeamSemantics.Team W) => support M (BSMLFormula.atom p) t) M.worlds

Atoms are flat: if all worlds in t satisfy p, then all worlds in t' ⊆ t satisfy p

source

theorem Semantics.Dynamic.BSML.ne_not_flat {W : Type u_1} [DecidableEq W] [Inhabited W] (worlds : List W) (hWorlds : worlds ≠ []) :

¬isFlat (fun (t : TeamSemantics.Team W) => support (BSMLModel.universal worlds) BSMLFormula.ne t) worlds

NE is NOT flat: the empty team doesn't support NE, but is a subset of any team that does

source

def Semantics.Dynamic.BSML.enrich :

BSMLFormula → BSMLFormula

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

The key insight: add non-emptiness constraints recursively. This captures the "neglect-zero" tendency in human cognition.

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

Equations

Instances For

source

theorem Semantics.Dynamic.BSML.enrich_neg_structure (φ : BSMLFormula) :

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

Enrichment of negation is negation of enrichment, conjoined with NE

source

theorem Semantics.Dynamic.BSML.enrich_conj_structure (φ ψ : BSMLFormula) :

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

Enrichment of conjunction is conjunction of enrichments (no extra NE)

source

theorem Semantics.Dynamic.BSML.enrich_disj_structure (φ ψ : BSMLFormula) :

enrich (φ.disj ψ) = (enrich φ).disj (enrich ψ)

Enrichment of disjunction is disjunction of enrichments (no extra NE)

source

theorem Semantics.Dynamic.BSML.enrich_poss_structure (φ : BSMLFormula) :

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

Enrichment of possibility is possibility of enrichment, conjoined with NE

source

theorem Semantics.Dynamic.BSML.enriched_support_implies_nonempty {W : Type u_1} [DecidableEq W] (M : BSMLModel W) (φ : BSMLFormula) (t : TeamSemantics.Team W) (h : support M (enrich φ) t = true) :

t.isNonEmpty M.worlds = true

If an enriched formula (other than NE) is supported, the team is non-empty.

For atoms, negation, and modals this follows from the top-level NE conjunct. For conjunction and disjunction (which lack top-level NE in Definition 6), non-emptiness is inherited from the enriched sub-formulas.

source

theorem Semantics.Dynamic.BSML.split_exists {W : Type u_1} [DecidableEq W] (M : BSMLModel W) (φ ψ : BSMLFormula) (t : TeamSemantics.Team W) (h : support M (φ.disj ψ) t = true) :

∃ (t₁ : TeamSemantics.Team W), ∃ (t₂ : TeamSemantics.Team W), support M φ t₁ = true ∧ support M ψ t₂ = true

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

source

theorem Semantics.Dynamic.BSML.enriched_split_forces_both_nonempty {W : Type u_1} [DecidableEq W] (M : BSMLModel W) (φ ψ : BSMLFormula) (t : TeamSemantics.Team W) (h : support M (enrich (φ.disj ψ)) t = true) :

∃ (t₁ : TeamSemantics.Team W), ∃ (t₂ : TeamSemantics.Team W), t₁.isNonEmpty M.worlds = true ∧ t₂.isNonEmpty M.worlds = true ∧ support M (enrich φ) t₁ = true ∧ support M (enrich ψ) t₂ = true

THE CORE LEMMA: Enriched disjunction forces both parts of split to be non-empty.

This is the derivation of free choice from first principles:

Split disjunction partitions the team
Enrichment adds NE to each disjunct
NE being non-flat means each part must be genuinely non-empty
Therefore both alternatives are "live" (FC!)

source

theorem Semantics.Dynamic.BSML.antiSupport_disj_is_conj {W : Type u_1} [DecidableEq W] (M : BSMLModel W) (φ ψ : BSMLFormula) (t : TeamSemantics.Team W) :

antiSupport M (φ.disj ψ) t = (antiSupport M φ t && antiSupport M ψ t)

Anti-support of disjunction is conjunction of anti-supports (no split!)

source

theorem Semantics.Dynamic.BSML.support_antiSupport_asymmetry {W : Type u_1} [DecidableEq W] (M : BSMLModel W) (φ ψ : BSMLFormula) (t : TeamSemantics.Team W) :

(support M (φ.disj ψ) t = true ↔ ((generateSplits t M.worlds).any fun (x : TeamSemantics.Team W × TeamSemantics.Team W) => match x with | (t1, t2) => support M φ t1 && support M ψ t2) = true) ∧ (antiSupport M (φ.disj ψ) t = true ↔ antiSupport M φ t = true ∧ antiSupport M ψ t = true)

The asymmetry: disjunction support uses existential (split), anti-support uses universal (conj)

Why FC Requires Atomic Formulas #

The FC theorems below are restricted to atomic α and β. The general version (for arbitrary BSMLFormula) is FALSE: enrichment [φ]⁺ does not entail φ for formulas containing □ under negation, because the NE added by enrichment creates "escape hatches" via empty accessibility sets.

source

instance Semantics.Dynamic.BSML.instDecidableEqCexWorld :

DecidableEq Semantics.Dynamic.BSML.CexWorld✝

Equations