Bilateral state-based modal logic: core definitions

Bilateral state-based modal logic (BSML, [Alo22]) evaluates formulas against teams — finite sets of worlds of a Kripke model — with two polarities: support (⊨⁺) and anti-support (⊨⁻). Negation swaps the polarities, so double-negation elimination holds definitionally, and the non-emptiness atom NE (supported exactly by non-empty teams) is the ingredient from which the free-choice effects derive. Despite being state-based, BSML is a static logic: formulas are evaluated against teams, not updated by them ([Alo22] p. 22). QBSML ([AvO23]) runs the same recursion over quantified atoms.

Main declarations

• Formula — atoms, NE, ¬, ∧, split ∨, and ◇; □ is the abbreviation Formula.nec (□φ := ¬◇¬φ).
• eval — bilateral evaluation, the two polarities unified by a Bool parameter; support/antiSupport fix the polarity.
• Formula.NEFree, Formula.Positive — the NE-free and negation-free syntactic fragments.
• ModalLogic.KripkeModel.IsIndisputable, ModalLogic.KripkeModel.IsStateBased — the frame conditions governing wide-scope free choice.
• consequence, equivalent — support consequence and bilateral equivalence.
• evalStar, consequenceStar — BSML*, the variant excluding ∅ from the possible states; supportStar/antiSupportStar fix the polarity.

Implementation notes

The support and anti-support clauses are dual — ∧/∨ swap, ◇/□ swap, atoms flip truth value:

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 = ∅

Encoding both polarities in one eval makes the duality a single recursion and double-negation elimination a rfl: eval M true (.neg (.neg φ)) t reduces to eval M true φ t by two negation clauses. Models are the shared ModalLogic.KripkeModel carrier; teams are Finset W; eval is Prop-valued with a Decidable instance, so concrete claims close by decide.

Formulas

inductive BSML.Formula (Atom : Type u_1) : Type u_1

BSML formulas over an atom type: p | NE | ¬φ | φ∧ψ | φ∨ψ | ◇φ. □ is not primitive — see Formula.nec.

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

  Atomic proposition

• ne {Atom : Type u_1} : Formula Atom

  Non-emptiness atom: team is non-empty

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

  Negation: swap support/anti-support

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

  Conjunction

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

  Split disjunction

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

  Possibility modal

@[instance_reducible]

instance BSML.instReprFormula {Atom✝ : Type u_1} [Repr Atom✝] : Repr (Formula Atom✝)

Equations

• BSML.instReprFormula = { reprPrec := BSML.instReprFormula.repr }

def BSML.instReprFormula.repr {Atom✝ : Type u_1} [Repr Atom✝] : Formula Atom✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• BSML.instReprFormula.repr BSML.Formula.ne prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BSML.Formula.ne")).group prec✝

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

Necessity as an abbreviation: Formula.nec φ = ¬◇¬φ, giving the derived clauses s ⊨⁺ □φ ↔ ∀ w ∈ s, R[w] ⊨⁺ φ and s ⊨⁻ □φ ↔ ∀ w ∈ s, ∃ nonempty t ⊆ R[w], t ⊨⁻ φ.

Equations

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

Syntactic fragments

def BSML.Formula.NEFree {Atom : Type u_1} : Formula Atom → Prop

Formula.NEFree φ holds when φ contains no NE atom — the fragment on which BSML collapses to classical modal logic on singleton teams (BSML/Bridge.lean).

Equations

• (BSML.Formula.atom a).NEFree = True
• BSML.Formula.ne.NEFree = False
• a.neg.NEFree = a.NEFree
• (a.conj a_1).NEFree = (a.NEFree ∧ a_1.NEFree)
• (a.disj a_1).NEFree = (a.NEFree ∧ a_1.NEFree)
• a.poss.NEFree = a.NEFree

@[instance_reducible]

instance BSML.instDecidableNEFree {Atom : Type u_1} (φ : Formula Atom) : Decidable φ.NEFree

Equations

• BSML.instDecidableNEFree (BSML.Formula.atom a) = isTrue trivial
• BSML.instDecidableNEFree BSML.Formula.ne = isFalse ⋯
• BSML.instDecidableNEFree a.neg = BSML.instDecidableNEFree a
• BSML.instDecidableNEFree (a.conj a_1) = instDecidableAnd
• BSML.instDecidableNEFree (a.disj a_1) = instDecidableAnd
• BSML.instDecidableNEFree a.poss = BSML.instDecidableNEFree a

def BSML.Formula.Positive {Atom : Type u_1} : Formula Atom → Prop

Formula.Positive φ holds when φ contains no negation.

Equations

• (BSML.Formula.atom a).Positive = True
• BSML.Formula.ne.Positive = True
• a.neg.Positive = False
• (a.conj a_1).Positive = (a.Positive ∧ a_1.Positive)
• (a.disj a_1).Positive = (a.Positive ∧ a_1.Positive)
• a.poss.Positive = a.Positive

@[instance_reducible]

instance BSML.instDecidablePositive {Atom : Type u_1} (φ : Formula Atom) : Decidable φ.Positive

Equations

• BSML.instDecidablePositive (BSML.Formula.atom a) = isTrue trivial
• BSML.instDecidablePositive BSML.Formula.ne = isTrue trivial
• BSML.instDecidablePositive a.neg = isFalse ⋯
• BSML.instDecidablePositive (a.conj a_1) = instDecidableAnd
• BSML.instDecidablePositive (a.disj a_1) = instDecidableAnd
• BSML.instDecidablePositive a.poss = BSML.instDecidablePositive a

Bilateral evaluation

def BSML.eval {Atom : Type u_1} {W : Type u_2} [DecidableEq W] (M : ModalLogic.KripkeModel W Atom) : Bool → Formula Atom → Finset W → Prop

Bilateral evaluation with polarity parameter: eval M true φ t is support (⊨⁺), eval M false φ t is anti-support (⊨⁻), and negation flips the polarity. The split clauses (disjunction-support, conjunction-anti-support) quantify over Team.splitsAs decompositions t₁ ∪ t₂ = t.

Equations

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

@[reducible, inline]

abbrev BSML.support {Atom : Type u_1} {W : Type u_2} [DecidableEq W] (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) : Prop

Support: positive evaluation.

Equations

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

@[reducible, inline]

abbrev BSML.antiSupport {Atom : Type u_1} {W : Type u_2} [DecidableEq W] (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) : Prop

Anti-support: negative evaluation.

Equations

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

Double-negation elimination

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

¬¬φ has the same support as φ, definitionally.

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

¬¬φ has the same anti-support as φ, definitionally.

Unfolding lemmas

@[simp]

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

@[simp]

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

theorem BSML.isBilateral {Atom : Type u_1} {W : Type u_2} [DecidableEq W] (M : ModalLogic.KripkeModel W Atom) : Bilateral.IsBilateral (support M) (antiSupport M) Formula.neg

BSML's support and antiSupport form a paraconsistent bilateral logic (Bilateral.IsBilateral) under Formula.neg.

@[simp]

theorem BSML.support_conj {Atom : Type u_1} {W : Type u_2} [DecidableEq W] (M : ModalLogic.KripkeModel W Atom) (φ ψ : Formula Atom) (t : Finset W) : support M (φ.conj ψ) t ↔ support M φ t ∧ support M ψ t

@[simp]

theorem BSML.antiSupport_disj {Atom : Type u_1} {W : Type u_2} [DecidableEq W] (M : ModalLogic.KripkeModel W Atom) (φ ψ : Formula Atom) (t : Finset W) : antiSupport M (φ.disj ψ) t ↔ antiSupport M φ t ∧ antiSupport M ψ t

theorem BSML.empty_supports_atom {Atom : Type u_1} {W : Type u_2} [DecidableEq W] (M : ModalLogic.KripkeModel W Atom) (p : Atom) : support M (Formula.atom p) ∅

The empty team supports every atom, vacuously.

Frame conditions

def ModalLogic.KripkeModel.IsIndisputable {Atom : Type u_1} {W : Type u_2} (M : KripkeModel W Atom) (t : Finset W) : Prop

Indisputable accessibility: all worlds in the team see the same accessible worlds — the frame condition for wide-scope free choice. Defined via Team.IsIndisputable, sharing substrate with QBSML.

Equations

• M.IsIndisputable t = Team.IsIndisputable M.access t

def ModalLogic.KripkeModel.IsStateBased {Atom : Type u_1} {W : Type u_2} (M : KripkeModel W Atom) (t : Finset W) : Prop

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

Equations

• M.IsStateBased t = Team.IsStateBased M.access t

@[instance_reducible]

instance BSML.instDecidableIsIndisputableOfFintype {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (M : ModalLogic.KripkeModel W Atom) (t : Finset W) : Decidable (M.IsIndisputable t)

Equations

• BSML.instDecidableIsIndisputableOfFintype M t = BSML.instDecidableIsIndisputableOfFintype._aux_1 M t

@[instance_reducible]

instance BSML.instDecidableIsStateBasedOfFintype {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (M : ModalLogic.KripkeModel W Atom) (t : Finset W) : Decidable (M.IsStateBased t)

Equations

• BSML.instDecidableIsStateBasedOfFintype M t = BSML.instDecidableIsStateBasedOfFintype._aux_1 M t

Consequence and equivalence

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

Semantic consequence: every team supporting φ supports ψ.

Equations

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

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

Semantic equivalence: same support and anti-support conditions.

Equations

• BSML.equivalent φ ψ = ∀ (M : ModalLogic.KripkeModel W Atom) (t : Finset W), (BSML.support M φ t ↔ BSML.support M ψ t) ∧ (BSML.antiSupport M φ t ↔ BSML.antiSupport M ψ t)

BSML*

def BSML.evalStar {Atom : Type u_1} {W : Type u_2} [DecidableEq W] (M : ModalLogic.KripkeModel W Atom) : Bool → Formula Atom → Finset W → Prop

Bilateral evaluation for BSML* ([Alo22] §6.3.1): like eval, but ∅ is not among the possible states, so the split clauses (disjunction-support, conjunction-anti-support) quantify over Team.splitsAsNE decompositions into non-empty parts. The exclusion is imposed wherever states are quantified — the splits here and the outer team in consequenceStar — while the atom, ne, and modal clauses keep their BSML form.

Equations

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

@[reducible, inline]

abbrev BSML.supportStar {Atom : Type u_1} {W : Type u_2} [DecidableEq W] (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) : Prop

BSML* support: positive evaluation with non-empty intermediate states.

Equations

• BSML.supportStar M φ t = BSML.evalStar M true φ t

@[reducible, inline]

abbrev BSML.antiSupportStar {Atom : Type u_1} {W : Type u_2} [DecidableEq W] (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) : Prop

BSML* anti-support.

Equations

• BSML.antiSupportStar M φ t = BSML.evalStar M false φ t

@[simp]

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

@[simp]

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

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

BSML* consequence: supportStar consequence on non-empty teams — in BSML*, ∅ is not among the possible states.

Equations

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

Decidability of evaluation

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

Decidability of eval by structural recursion on the formula.

Equations

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

@[instance_reducible]

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

Equations

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