Bilateral State-based Modal Logic (BSML) — Core

@cite{aloni-yang-2024} @cite{aloni-2022}

Core definitions for BSML: formulas, models, bilateral support/anti-support, and double negation elimination.

BSML evaluates formulas bilaterally 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₂ ⊨ ψ
• Non-emptiness atom (NE): t ⊨ NE iff t ≠ ∅

inductive Semantics.Dynamic.BSML.BSMLFormula : Type

BSML formulas with bilateral support conditions.

The key innovation is SPLIT DISJUNCTION: a team supports φ ∨ ψ iff the team can be partitioned into parts supporting each disjunct.

• atom : String → BSMLFormula

  Atomic proposition

• ne : BSMLFormula

  Non-emptiness atom: team is non-empty

• neg : BSMLFormula → BSMLFormula

  Negation: swap support/anti-support

• conj : BSMLFormula → BSMLFormula → BSMLFormula

  Conjunction

• disj : BSMLFormula → BSMLFormula → BSMLFormula

  Split disjunction (Aloni's key innovation)

• poss : BSMLFormula → BSMLFormula

  Possibility modal

• nec : BSMLFormula → BSMLFormula

  Necessity modal

def Semantics.Dynamic.BSML.instReprBSMLFormula.repr : BSMLFormula → ℕ → Std.Format

Equations

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

instance Semantics.Dynamic.BSML.instReprBSMLFormula : Repr BSMLFormula

Equations

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

structure Semantics.Dynamic.BSML.BSMLModel (W : Type u_1) : Type u_1

A BSML model bundles:

• A finite list of worlds
• An accessibility relation R (for modals), given as R[w] = accessible team
• A valuation V (atomic propositions)

• worlds : List W

  The finite universe of worlds

• access : W → TeamSemantics.Team W

  Accessibility: R[w] = worlds accessible from w

• valuation : String → W → Bool

  Valuation: which atoms are true at which worlds

def Semantics.Dynamic.BSML.BSMLModel.universal {W : Type u_1} (worlds : List W) : BSMLModel W

Universal accessibility (S5-like): all worlds accessible from all

Equations

• Semantics.Dynamic.BSML.BSMLModel.universal worlds = { worlds := worlds, access := fun (x : W) => Semantics.Dynamic.TeamSemantics.Team.full, valuation := fun (x : String) (x_1 : W) => false }

def Semantics.Dynamic.BSML.BSMLModel.isIndisputable {W : Type u_1} (M : BSMLModel W) (t : TeamSemantics.Team W) : Bool

Indisputable accessibility: all worlds in team have same accessible worlds

Equations

• M.isIndisputable t = match t.toList M.worlds with | [] => true | w :: rest => rest.all fun (v : W) => (M.access w).beq (M.access v) M.worlds

def Semantics.Dynamic.BSML.allSubsets {α : Type u_1} : List α → List (List α)

Generate all subsets of a list

Equations

• Semantics.Dynamic.BSML.allSubsets [] = [[]]
• Semantics.Dynamic.BSML.allSubsets (w :: rest) = Semantics.Dynamic.BSML.allSubsets rest ++ List.map (fun (x : List α) => w :: x) (Semantics.Dynamic.BSML.allSubsets rest)

def Semantics.Dynamic.BSML.generateSplits {W : Type u_1} [DecidableEq W] (t : TeamSemantics.Team W) (worlds : List W) : List (TeamSemantics.Team W × TeamSemantics.Team W)

Generate all possible splits of a team into two parts

Equations

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

def Semantics.Dynamic.BSML.generateSubteams {W : Type u_1} [DecidableEq W] (t : TeamSemantics.Team W) (worlds : List W) : List (TeamSemantics.Team W)

Generate all subteams of a team

Equations

• Semantics.Dynamic.BSML.generateSubteams t worlds = List.map Semantics.Dynamic.TeamSemantics.Team.ofList (Semantics.Dynamic.BSML.allSubsets (t.toList worlds))

def Semantics.Dynamic.BSML.support {W : Type u_1} [DecidableEq W] (M : BSMLModel W) (φ : BSMLFormula) (t : TeamSemantics.Team W) : Bool

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Dynamic.BSML.support M (Semantics.Dynamic.BSML.BSMLFormula.atom a) t = t.all (M.valuation a) M.worlds
• Semantics.Dynamic.BSML.support M Semantics.Dynamic.BSML.BSMLFormula.ne t = t.isNonEmpty M.worlds
• Semantics.Dynamic.BSML.support M a.neg t = Semantics.Dynamic.BSML.antiSupport M a t
• Semantics.Dynamic.BSML.support M (a.conj a_1) t = (Semantics.Dynamic.BSML.support M a t && Semantics.Dynamic.BSML.support M a_1 t)
• Semantics.Dynamic.BSML.support M a.nec t = t.all (fun (w : W) => Semantics.Dynamic.BSML.support M a (M.access w)) M.worlds

def Semantics.Dynamic.BSML.antiSupport {W : Type u_1} [DecidableEq W] (M : BSMLModel W) (φ : BSMLFormula) (t : TeamSemantics.Team W) : Bool

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Dynamic.BSML.antiSupport M (Semantics.Dynamic.BSML.BSMLFormula.atom a) t = t.all (fun (w : W) => !M.valuation a w) M.worlds
• Semantics.Dynamic.BSML.antiSupport M Semantics.Dynamic.BSML.BSMLFormula.ne t = t.isEmpty M.worlds
• Semantics.Dynamic.BSML.antiSupport M a.neg t = Semantics.Dynamic.BSML.support M a t
• Semantics.Dynamic.BSML.antiSupport M (a.conj a_1) t = (Semantics.Dynamic.BSML.antiSupport M a t || Semantics.Dynamic.BSML.antiSupport M a_1 t)
• Semantics.Dynamic.BSML.antiSupport M (a.disj a_1) t = (Semantics.Dynamic.BSML.antiSupport M a t && Semantics.Dynamic.BSML.antiSupport M a_1 t)
• Semantics.Dynamic.BSML.antiSupport M a.nec t = t.any (fun (w : W) => Semantics.Dynamic.BSML.antiSupport M a (M.access w)) M.worlds

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

DNE holds definitionally: ¬¬φ has the same support conditions as φ.

This follows from negation swapping support and anti-support.

theorem Semantics.Dynamic.BSML.dne_antiSupport {W : Type u_1} [DecidableEq W] (M : BSMLModel W) (φ : BSMLFormula) (t : TeamSemantics.Team W) : antiSupport M φ.neg.neg t = antiSupport M φ t