Bilateral State-based Modal Logic (BSML) — Core Definitions

@cite{aloni-2022}

BSML is a bilateral, state-based modal logic in which formulas are evaluated against teams (sets of worlds):

• Support (⊨⁺): positive evaluation
• Anti-support (⊨⁻): negative evaluation
• Negation: swaps support and anti-support → DNE is definitional

Key innovations over classical modal logic:

• Split disjunction: t ⊨⁺ φ ∨ ψ iff ∃t₁,t₂: t₁ ∪ t₂ = t ∧ t₁ ⊨⁺ φ ∧ t₂ ⊨⁺ ψ
• Split conjunction (anti-support): t ⊨⁻ φ ∧ ψ iff ∃t₁,t₂: t₁ ∪ t₂ = t ∧ t₁ ⊨⁻ φ ∧ t₂ ⊨⁻ ψ
• Non-emptiness atom (NE): t ⊨⁺ NE iff t ≠ ∅

Despite being state-based, BSML is a static logic (not dynamic): formulas are evaluated against teams, not updated by them (@cite{aloni-2022} p. 22).

Atom polymorphism

Both BSMLFormula and BSMLModel are parameterized over an atom type Atom : Type*. This eliminates the silent typo trap of String-keyed valuations and aligns with the predicate-level extension in QBSML (@cite{aloni-vanormondt-2023}), which generalizes atoms to typed predicates with terms.

Substrate dependencies

The split-disjunction predicate splitsAs and the frame-condition predicates isStateBased / isIndisputable live in Core.Logic.Team (theory-neutral Finset combinatorics) and are consumed below. This is the same machinery QBSML reuses via the s↓ projection from Finset (W × Assignment) to Finset W.

Bilateral Symmetry

The support and anti-support clauses exhibit a striking duality:

Connective	Support (⊨⁺)	Anti-support (⊨⁻)
p (atom)	∀w∈s: V(w,p)=1	∀w∈s: V(w,p)=0
¬φ	s ⊨⁻ φ	s ⊨⁺ φ
φ ∧ ψ	s ⊨⁺ φ ∧ s ⊨⁺ ψ	∃t,u: t∪u=s ∧ t ⊨⁻ φ ∧ u ⊨⁻ ψ
φ ∨ ψ	∃t,u: t∪u=s ∧ t ⊨⁺ φ ∧ u ⊨⁺ ψ	s ⊨⁻ φ ∧ s ⊨⁻ ψ
◇φ	∀w∈s: ∃ ne t⊆R[w]: t ⊨⁺ φ	∀w∈s: R[w] ⊨⁻ φ
□φ	∀w∈s: R[w] ⊨⁺ φ	∀w∈s: ∃ ne t⊆R[w]: t ⊨⁻ φ
NE	s ≠ ∅	s = ∅

∧/∨ are swapped; ◇/□ are swapped; atoms are dual.

Implementation

Teams are Finset W (with [DecidableEq W] [Fintype W]). Support and anti-support are unified into a single eval function parameterized by a Bool polarity. This makes DNE definitional (eval M true (.neg (.neg φ)) t reduces to eval M true φ t by two applications of the negation clause).

eval returns Prop, with a Decidable instance provided for computational verification via #guard decide (...).

inductive Semantics.BSML.BSMLFormula (Atom : Type u_1) : Type u_1

BSML formula language (Definition 1 from @cite{aloni-2022}).

Parameterized over an atom type Atom : Type*. The base language is: p | ¬φ | φ∧ψ | φ∨ψ | ◇φ | NE. □ is NOT a primitive — it is defined as an abbreviation: □φ := ¬◇¬φ (see BSMLFormula.nec).

• atom {Atom : Type u_1} : Atom → BSMLFormula Atom

  Atomic proposition

• ne {Atom : Type u_1} : BSMLFormula Atom

  Non-emptiness atom: team is non-empty

• neg {Atom : Type u_1} : BSMLFormula Atom → BSMLFormula Atom

  Negation: swap support/anti-support

• conj {Atom : Type u_1} : BSMLFormula Atom → BSMLFormula Atom → BSMLFormula Atom

  Conjunction

• disj {Atom : Type u_1} : BSMLFormula Atom → BSMLFormula Atom → BSMLFormula Atom

  Split disjunction

• poss {Atom : Type u_1} : BSMLFormula Atom → BSMLFormula Atom

  Possibility modal

def Semantics.BSML.instReprBSMLFormula.repr {Atom✝ : Type u_1} [Repr Atom✝] : BSMLFormula Atom✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Semantics.BSML.instReprBSMLFormula {Atom✝ : Type u_1} [Repr Atom✝] : Repr (BSMLFormula Atom✝)

Equations

• Semantics.BSML.instReprBSMLFormula = { reprPrec := Semantics.BSML.instReprBSMLFormula.repr }

def Semantics.BSML.BSMLFormula.nec {Atom : Type u_1} (φ : BSMLFormula Atom) : BSMLFormula Atom

□φ := ¬◇¬φ — necessity as an abbreviation, not a primitive. The derived support/anti-support conditions are:

• s ⊨⁺ □φ iff ∀w∈s, R[w] ⊨⁺ φ
• s ⊨⁻ □φ iff ∀w∈s, ∃ ne t⊆R[w], t ⊨⁻ φ These follow from the definitions of ¬, ◇, and ¬ applied to φ.

Equations

• φ.nec = φ.neg.poss.neg

def Semantics.BSML.BSMLFormula.isNEFree {Atom : Type u_1} : BSMLFormula Atom → Bool

A formula is NE-free if it does not contain the NE atom. For NE-free formulas, BSML reduces to classical modal logic on singleton teams (Fact 15, @cite{aloni-2022}).

Equations

• (Semantics.BSML.BSMLFormula.atom a).isNEFree = true
• Semantics.BSML.BSMLFormula.ne.isNEFree = false
• a.neg.isNEFree = a.isNEFree
• (a.conj a_1).isNEFree = (a.isNEFree && a_1.isNEFree)
• (a.disj a_1).isNEFree = (a.isNEFree && a_1.isNEFree)
• a.poss.isNEFree = a.isNEFree

def Semantics.BSML.BSMLFormula.isPositive {Atom : Type u_1} : BSMLFormula Atom → Bool

A formula is positive if it contains no negation.

Equations

• (Semantics.BSML.BSMLFormula.atom a).isPositive = true
• Semantics.BSML.BSMLFormula.ne.isPositive = true
• a.neg.isPositive = false
• (a.conj a_1).isPositive = (a.isPositive && a_1.isPositive)
• (a.disj a_1).isPositive = (a.isPositive && a_1.isPositive)
• a.poss.isPositive = a.isPositive

def Semantics.BSML.BSMLFormula.isAtom {Atom : Type u_1} : BSMLFormula Atom → Bool

A formula is atomic (a single propositional variable).

Equations

• (Semantics.BSML.BSMLFormula.atom a).isAtom = true
• x✝.isAtom = false

theorem Semantics.BSML.BSMLFormula.isAtom_implies_isNEFree {Atom : Type u_1} (φ : BSMLFormula Atom) (h : φ.isAtom = true) : φ.isNEFree = true

Atoms are NE-free.

structure Semantics.BSML.BSMLModel (W : Type u_2) (Atom : Type u_3) [DecidableEq W] [Fintype W] : Type (max u_2 u_3)

A BSML model: accessibility and valuation over a finite type of worlds (Definition 1, @cite{aloni-2022}). The universe of worlds is given by [Fintype W] — use Finset.univ for the full set.

Parameterized over both W (worlds) and Atom (atomic propositions). The val field maps an atom name to its truth value at each world.

• access : W → Finset W

  Accessibility: R[w] = worlds accessible from w

• val : Atom → W → Bool

  Valuation: which atoms are true at which worlds

def Semantics.BSML.eval {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (M : BSMLModel W Atom) : Bool → BSMLFormula Atom → Finset W → Prop

Bilateral evaluation with polarity parameter (Definition 2, @cite{aloni-2022}).

eval M true φ t is support (⊨⁺), eval M false φ t is anti-support (⊨⁻). Negation flips polarity, making DNE definitional: eval M true (.neg (.neg φ)) t = eval M true φ t by computation.

Split disjunction and split conjunction-anti-support clauses use Core.Logic.Team.splitsAs (= t₁ ∪ t₂ = t); the recursion is the same shape QBSML reuses at the Finset (W × Assignment) carrier.

Equations

• Semantics.BSML.eval M true (Semantics.BSML.BSMLFormula.atom p) x✝ = ∀ w ∈ x✝, M.val p w = true
• Semantics.BSML.eval M false (Semantics.BSML.BSMLFormula.atom p) x✝ = ∀ w ∈ x✝, M.val p w = false
• Semantics.BSML.eval M true Semantics.BSML.BSMLFormula.ne x✝ = x✝.Nonempty
• Semantics.BSML.eval M false Semantics.BSML.BSMLFormula.ne x✝ = (x✝ = ∅)
• Semantics.BSML.eval M true ψ.neg x✝ = Semantics.BSML.eval M false ψ x✝
• Semantics.BSML.eval M false ψ.neg x✝ = Semantics.BSML.eval M true ψ x✝
• Semantics.BSML.eval M true (ψ₁.conj ψ₂) x✝ = (Semantics.BSML.eval M true ψ₁ x✝ ∧ Semantics.BSML.eval M true ψ₂ x✝)
• Semantics.BSML.eval M false (ψ₁.conj ψ₂) x✝ = ∃ (t₁ : Finset W) (t₂ : Finset W), Core.Logic.Team.splitsAs x✝ t₁ t₂ ∧ Semantics.BSML.eval M false ψ₁ t₁ ∧ Semantics.BSML.eval M false ψ₂ t₂
• Semantics.BSML.eval M true (ψ₁.disj ψ₂) x✝ = ∃ (t₁ : Finset W) (t₂ : Finset W), Core.Logic.Team.splitsAs x✝ t₁ t₂ ∧ Semantics.BSML.eval M true ψ₁ t₁ ∧ Semantics.BSML.eval M true ψ₂ t₂
• Semantics.BSML.eval M false (ψ₁.disj ψ₂) x✝ = (Semantics.BSML.eval M false ψ₁ x✝ ∧ Semantics.BSML.eval M false ψ₂ x✝)
• Semantics.BSML.eval M true ψ.poss x✝ = ∀ w ∈ x✝, ∃ s ⊆ M.access w, s.Nonempty ∧ Semantics.BSML.eval M true ψ s
• Semantics.BSML.eval M false ψ.poss x✝ = ∀ w ∈ x✝, Semantics.BSML.eval M false ψ (M.access w)

@[reducible, inline]

abbrev Semantics.BSML.support {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (M : BSMLModel W Atom) (φ : BSMLFormula Atom) (t : Finset W) : Prop

Support: positive evaluation.

Equations

• Semantics.BSML.support M φ t = Semantics.BSML.eval M true φ t

@[reducible, inline]

abbrev Semantics.BSML.antiSupport {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (M : BSMLModel W Atom) (φ : BSMLFormula Atom) (t : Finset W) : Prop

Anti-support: negative evaluation.

Equations

• Semantics.BSML.antiSupport M φ t = Semantics.BSML.eval M false φ t

theorem Semantics.BSML.dne_support {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (M : BSMLModel W Atom) (φ : BSMLFormula Atom) (t : Finset W) : support M φ.neg.neg t ↔ support M φ t

DNE: ¬¬φ has the same support as φ. Definitional with the polarity design.

theorem Semantics.BSML.dne_antiSupport {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (M : BSMLModel W Atom) (φ : BSMLFormula Atom) (t : Finset W) : antiSupport M φ.neg.neg t ↔ antiSupport M φ t

DNE: ¬¬φ has the same anti-support as φ.

@[simp]

theorem Semantics.BSML.support_neg {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (M : BSMLModel W Atom) (φ : BSMLFormula Atom) (t : Finset W) : support M φ.neg t ↔ antiSupport M φ t

@[simp]

theorem Semantics.BSML.antiSupport_neg {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (M : BSMLModel W Atom) (φ : BSMLFormula Atom) (t : Finset W) : antiSupport M φ.neg t ↔ support M φ t

theorem Semantics.BSML.isBilateral {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (M : BSMLModel W Atom) : Core.Logic.Bilateral.IsBilateral (support M) (antiSupport M) BSMLFormula.neg

BSML's support and antiSupport form a paraconsistent bilateral logic (Core.Logic.Bilateral.IsBilateral) under BSMLFormula.neg. Pointwise polarity-flip lemmas (support_neg / antiSupport_neg, both Iff.rfl) lift to function equality via IsBilateral.of_iff.

@[simp]

theorem Semantics.BSML.support_conj {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (M : BSMLModel W Atom) (φ ψ : BSMLFormula Atom) (t : Finset W) : support M (φ.conj ψ) t ↔ support M φ t ∧ support M ψ t

@[simp]

theorem Semantics.BSML.antiSupport_disj {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (M : BSMLModel W Atom) (φ ψ : BSMLFormula Atom) (t : Finset W) : antiSupport M (φ.disj ψ) t ↔ antiSupport M φ t ∧ antiSupport M ψ t

theorem Semantics.BSML.empty_supports_atom {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (M : BSMLModel W Atom) (p : Atom) : support M (BSMLFormula.atom p) ∅

Empty team supports all atoms (vacuous truth).

def Semantics.BSML.BSMLModel.isIndisputable {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (M : BSMLModel W Atom) (t : Finset W) : Prop

Indisputable accessibility: all worlds in team see the same accessible worlds. Required for wide-scope FC (Fact 5, @cite{aloni-2022}).

Defined via Core.Logic.Team.isIndisputable to share substrate with QBSML and any other state-based logic.

Equations

• M.isIndisputable t = Core.Logic.Team.isIndisputable M.access t

def Semantics.BSML.BSMLModel.isStateBased {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (M : BSMLModel W Atom) (t : Finset W) : Prop

State-based accessibility: every world in team has the team itself as accessible worlds. Strictly stronger than indisputability.

Defined via Core.Logic.Team.isStateBased.

Equations

• M.isStateBased t = Core.Logic.Team.isStateBased M.access t

@[implicit_reducible]

instance Semantics.BSML.instDecidableIsIndisputable {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (M : BSMLModel W Atom) (t : Finset W) : Decidable (M.isIndisputable t)

Equations

• Semantics.BSML.instDecidableIsIndisputable M t = id inferInstance

@[implicit_reducible]

instance Semantics.BSML.instDecidableIsStateBased {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (M : BSMLModel W Atom) (t : Finset W) : Decidable (M.isStateBased t)

Equations

• Semantics.BSML.instDecidableIsStateBased M t = id inferInstance

def Semantics.BSML.consequence {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (φ ψ : BSMLFormula Atom) : Prop

Semantic consequence: φ ⊨ ψ if every team supporting φ also supports ψ.

Equations

• Semantics.BSML.consequence φ ψ = ∀ (M : Semantics.BSML.BSMLModel W Atom) (t : Finset W), Semantics.BSML.support M φ t → Semantics.BSML.support M ψ t

def Semantics.BSML.equivalent {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (φ ψ : BSMLFormula Atom) : Prop

Semantic equivalence: same support and anti-support conditions.

Equations

• One or more equations did not get rendered due to their size.

def Semantics.BSML.supportStar {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (M : BSMLModel W Atom) : BSMLFormula Atom → Finset W → Prop

BSML* support: like standard BSML support but ∅ is excluded from all intermediate states. The only difference from eval M true is in disjunction, where both parts of the split must be non-empty. (@cite{aloni-2022} §6.3.1).

NOTE: the negation case | .neg _, _ => True is a placeholder. Aloni's actual BSML* uses bilateral polarity mirror BSML's; completing this requires a proper polarity-flipped supportStar definition. Tracked as out-of-scope per Phenomena/FreeChoice/Divergences.lean §3.

Equations

• Semantics.BSML.supportStar M (Semantics.BSML.BSMLFormula.atom p) x✝ = ∀ w ∈ x✝, M.val p w = true
• Semantics.BSML.supportStar M Semantics.BSML.BSMLFormula.ne x✝ = x✝.Nonempty
• Semantics.BSML.supportStar M a.neg x✝ = True
• Semantics.BSML.supportStar M (φ.conj ψ) x✝ = (Semantics.BSML.supportStar M φ x✝ ∧ Semantics.BSML.supportStar M ψ x✝)
• Semantics.BSML.supportStar M (φ.disj ψ) x✝ = ∃ (t₁ : Finset W) (t₂ : Finset W), Core.Logic.Team.splitsAsNE x✝ t₁ t₂ ∧ Semantics.BSML.supportStar M φ t₁ ∧ Semantics.BSML.supportStar M ψ t₂
• Semantics.BSML.supportStar M φ.poss x✝ = ∀ w ∈ x✝, ∃ s ⊆ M.access w, s.Nonempty ∧ Semantics.BSML.supportStar M φ s

def Semantics.BSML.consequenceStar {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (φ ψ : BSMLFormula Atom) : Prop

BSML* consequence: consequence using BSML* support (non-empty intermediate states) on non-empty teams. In BSML*, the empty set ∅ is not among the possible states (@cite{aloni-2022} §6.3.1).

Equations

• Semantics.BSML.consequenceStar φ ψ = ∀ (M : Semantics.BSML.BSMLModel W Atom) (t : Finset W), t.Nonempty → Semantics.BSML.supportStar M φ t → Semantics.BSML.supportStar M ψ t

def Semantics.BSML.decidableEval {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (M : BSMLModel W Atom) (pol : Bool) (φ : BSMLFormula Atom) (t : Finset W) : Decidable (eval M pol φ t)

Decidability of eval by structural recursion on the formula.

Equations

• Semantics.BSML.decidableEval M true (Semantics.BSML.BSMLFormula.atom p) x✝ = ⋯.mpr inferInstance
• Semantics.BSML.decidableEval M false (Semantics.BSML.BSMLFormula.atom p) x✝ = ⋯.mpr inferInstance
• Semantics.BSML.decidableEval M true Semantics.BSML.BSMLFormula.ne x✝ = ⋯.mpr inferInstance
• Semantics.BSML.decidableEval M false Semantics.BSML.BSMLFormula.ne x✝ = ⋯.mpr inferInstance
• Semantics.BSML.decidableEval M true ψ.neg x✝ = ⋯.mpr (Semantics.BSML.decidableEval M false ψ x✝)
• Semantics.BSML.decidableEval M false ψ.neg x✝ = ⋯.mpr (Semantics.BSML.decidableEval M true ψ x✝)
• Semantics.BSML.decidableEval M true (ψ₁.conj ψ₂) x✝ = ⋯.mpr instDecidableAnd
• Semantics.BSML.decidableEval M false (ψ₁.conj ψ₂) x✝ = ⋯.mpr Fintype.decidableExistsFintype
• Semantics.BSML.decidableEval M true (ψ₁.disj ψ₂) x✝ = ⋯.mpr Fintype.decidableExistsFintype
• Semantics.BSML.decidableEval M false (ψ₁.disj ψ₂) x✝ = ⋯.mpr instDecidableAnd
• Semantics.BSML.decidableEval M true ψ.poss x✝ = ⋯.mpr Finset.decidableDforallFinset
• Semantics.BSML.decidableEval M false ψ.poss x✝ = ⋯.mpr Finset.decidableDforallFinset

@[implicit_reducible]

instance Semantics.BSML.instDecidableEval {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (M : BSMLModel W Atom) (pol : Bool) (φ : BSMLFormula Atom) (t : Finset W) : Decidable (eval M pol φ t)

Equations

• Semantics.BSML.instDecidableEval M pol φ t = Semantics.BSML.decidableEval M pol φ t