BSML–CML Bridge

@cite{aloni-2022}

For NE-free formulas, BSML reduces to classical modal logic (CML) on singleton teams (Fact 15 from @cite{aloni-2022}). This module defines a classical evaluation function and proves the correspondence.

Key Result

Result	Statement
Classical Collapse (Fact 15)	For NE-free φ, {w} ⊨⁺ φ iff φ is classically true at w

Architecture

classicalEval evaluates BSML formulas as standard Kripke modal logic formulas: ∨ is pointwise (not split), ◇ is existential over accessible worlds, □ is universal. For NE-free formulas, this agrees with BSML's team semantics restricted to singleton teams.

def Semantics.BSML.classicalEval {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ : BSMLFormula Atom) (w : W) : Bool

Classical (Kripke) evaluation of a BSML formula at a single world. ∨ is pointwise, ◇ is existential, □ is universal — no team splitting. NE evaluates to true (singletons are non-empty).

Equations

• Semantics.BSML.classicalEval M (Semantics.BSML.BSMLFormula.atom p) w = M.val p w
• Semantics.BSML.classicalEval M Semantics.BSML.BSMLFormula.ne w = true
• Semantics.BSML.classicalEval M ψ.neg w = !Semantics.BSML.classicalEval M ψ w
• Semantics.BSML.classicalEval M (ψ₁.conj ψ₂) w = (Semantics.BSML.classicalEval M ψ₁ w && Semantics.BSML.classicalEval M ψ₂ w)
• Semantics.BSML.classicalEval M (ψ₁.disj ψ₂) w = (Semantics.BSML.classicalEval M ψ₁ w || Semantics.BSML.classicalEval M ψ₂ w)
• Semantics.BSML.classicalEval M ψ.poss w = decide (∃ v ∈ M.access w, Semantics.BSML.classicalEval M ψ v = true)

theorem Semantics.BSML.classicalCollapse {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ : BSMLFormula Atom) (w : W) (hNE : φ.isNEFree = true) : support M φ {w} ↔ classicalEval M φ w = true

Classical Collapse (Fact 15 from @cite{aloni-2022}).

For NE-free formulas, BSML support on a singleton team equals classical Kripke evaluation.

theorem Semantics.BSML.classicalCollapseAnti {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ : BSMLFormula Atom) (w : W) (hNE : φ.isNEFree = true) : antiSupport M φ {w} ↔ classicalEval M φ w = false

Anti-support collapse: singleton anti-support equals negation of classical evaluation.

theorem Semantics.BSML.neFree_flat {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ : BSMLFormula Atom) (t : Finset W) (hNE : φ.isNEFree = true) : support M φ t ↔ ∀ w ∈ t, classicalEval M φ w = true

NE-free formulas have flat support: team support = pointwise classical evaluation on all members.

Accessibility Type Bridge

BSMLModel.access : W → Finset W can be converted to a Prop-valued AccessRel W = W → W → Prop via fun w v => v ∈ M.access w, which is the canonical accessibility-relation type in Core.Logic.Intensional.

def Semantics.BSML.BSMLModel.toAccessRel {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) : Core.Logic.Intensional.AccessRel W

Convert BSML accessibility (Finset-valued) to a classical Prop-valued accessibility relation.

Equations

• M.toAccessRel w v = (v ∈ M.access w)

theorem Semantics.BSML.classicalEval_agrees_diamondR_poss {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ : BSMLFormula Atom) (w : W) : classicalEval M φ.poss w = true ↔ Core.Logic.Intensional.diamondR M.toAccessRel (fun (v : W) => classicalEval M φ v = true) w

classicalEval of ◇φ agrees with diamondR (Prop-valued possibility), connecting BSML's classical evaluation to the shared modal logic infrastructure from Core.Logic.Intensional.