Bilateral state-based modal logic

Aloni's bilateral state-based modal logic (BSML) evaluates formulas against teams, finite sets of worlds of a Kripke model, in two polarities: support (⊨⁺) and anti-support (⊨⁻). Negation swaps the polarities, and the non-emptiness atom NE, supported exactly by the non-empty teams, is the source of the free-choice effects. BSML is static: formulas are evaluated against teams, not updated by them. QBSML runs the same recursion over quantified atoms.

Main definitions

• Formula: atoms, NE, ¬, ∧, split ∨ and ◇; □ is the abbreviation Formula.nec.
• eval: bilateral evaluation, with the polarity a Bool; support and antiSupport fix it.
• Formula.NEFree, Formula.Positive: the NE-free and the negation-free fragments.
• Formula.modalDepth: the nesting depth of ◇.
• Formula.falsum, Formula.strongFalsum: the weak contradiction p ∧ ¬p and the strong contradiction ⊥ ∧ NE.
• Consequence, Equivalent: support consequence and its symmetric closure, the ≡ of the sources; StronglyEquivalent: equivalence of the formulas and of their negations.
• evalStar, ConsequenceStar: BSML*, which excludes ∅ from the possible states.

Implementation notes

The support and anti-support clauses are dual: ∧ and ∨ swap, ◇ and □ swap, and atoms flip their 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 = ∅

Each clause applies an operation of Team/Operations.lean to the support sets of the subformulas, so the closure properties of Properties.lean are folds over the per-connective lemmas there. One eval for both polarities makes double-negation elimination rfl. eval is Prop-valued with a Decidable instance, so concrete claims close by decide.

References

• [Alo22] Aloni, Logic and Conversation: The Case of Free Choice
• [AAY24] Aloni, Anttila and Yang, State-based Modal Logics for Free Choice
• [AvO23] Aloni and van Ormondt, Modified Numerals and Split Disjunction: The First-Order Case
• [Ant21] Anttila, The Logic of Free Choice: Axiomatizations of State-based Modal Logics

Formulas

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

The formulas of BSML over an atom type are built from atoms and NE by ¬, ∧, split ∨ and ◇; □ is the abbreviation Formula.nec.

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

  An atomic proposition.

• ne {Atom : Type u_1} : Formula Atom

  The non-emptiness atom, supported by the non-empty teams.

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

  Negation, which swaps support and 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

  The possibility modality.

@[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 □φ abbreviates ¬◇¬φ. A team supports it when the successors of each of its worlds support φ, and anti-supports it when each world has a non-empty set of successors anti-supporting φ.

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/Classical.lean).

Equations

• (BSML.Formula.atom a).NEFree = True
• BSML.Formula.ne.NEFree = False
• φ.neg.NEFree = φ.NEFree
• (φ.conj ψ).NEFree = (φ.NEFree ∧ ψ.NEFree)
• (φ.disj ψ).NEFree = (φ.NEFree ∧ ψ.NEFree)
• φ.poss.NEFree = φ.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 φ.neg = BSML.instDecidableNEFree φ
• BSML.instDecidableNEFree (φ.conj ψ) = instDecidableAnd
• BSML.instDecidableNEFree (φ.disj ψ) = instDecidableAnd
• BSML.instDecidableNEFree φ.poss = BSML.instDecidableNEFree φ

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
• φ.neg.Positive = False
• (φ.conj ψ).Positive = (φ.Positive ∧ ψ.Positive)
• (φ.disj ψ).Positive = (φ.Positive ∧ ψ.Positive)
• φ.poss.Positive = φ.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 φ.neg = isFalse ⋯
• BSML.instDecidablePositive (φ.conj ψ) = instDecidableAnd
• BSML.instDecidablePositive (φ.disj ψ) = instDecidableAnd
• BSML.instDecidablePositive φ.poss = BSML.instDecidablePositive φ

def BSML.Formula.modalDepth {Atom : Type u_1} : Formula Atom → ℕ

The modal depth of a formula is the greatest number of nested ◇s in it ([AAY24]).

Equations

• (BSML.Formula.atom a).modalDepth = 0
• BSML.Formula.ne.modalDepth = 0
• φ.neg.modalDepth = φ.modalDepth
• (φ.conj ψ).modalDepth = max φ.modalDepth ψ.modalDepth
• (φ.disj ψ).modalDepth = max φ.modalDepth ψ.modalDepth
• φ.poss.modalDepth = φ.modalDepth + 1

Contradictions

def BSML.Formula.falsum {Atom : Type u_1} [Inhabited Atom] : Formula Atom

The weak contradiction ⊥ := p ∧ ¬p for a fixed atom p, the default one ([Alo22]; [AAY24] take ⊥ as primitive instead).

Equations

• BSML.Formula.falsum = (BSML.Formula.atom default).conj (BSML.Formula.atom default).neg

def BSML.Formula.strongFalsum {Atom : Type u_1} [Inhabited Atom] : Formula Atom

The strong contradiction ⊥⊥ := ⊥ ∧ NE ([AAY24]).

Equations

• BSML.Formula.strongFalsum = BSML.Formula.falsum.conj BSML.Formula.ne

@[simp]

theorem BSML.Formula.neFree_falsum {Atom : Type u_1} [Inhabited Atom] : falsum.NEFree

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 eval M b φ t is support (⊨⁺) when b is true and anti-support (⊨⁻) when b is false. Negation flips the polarity, and the split clauses, support of ∨ and anti-support of ∧, are Team.tensor.

Equations

• BSML.eval M true (BSML.Formula.atom p) x✝ = (x✝ ∈ Team.flat (M.val p))
• BSML.eval M false (BSML.Formula.atom p) x✝ = (x✝ ∈ Team.flat fun (w : W) => ¬M.val p w)
• BSML.eval M true BSML.Formula.ne x✝ = (x✝ ∈ Team.ne)
• 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✝ = (x✝ ∈ Team.tensor {s : Finset W | BSML.eval M false ψ₁ s} {s : Finset W | BSML.eval M false ψ₂ s})
• BSML.eval M true (ψ₁.disj ψ₂) x✝ = (x✝ ∈ Team.tensor {s : Finset W | BSML.eval M true ψ₁ s} {s : Finset W | BSML.eval M true ψ₂ s})
• BSML.eval M false (ψ₁.disj ψ₂) x✝ = (BSML.eval M false ψ₁ x✝ ∧ BSML.eval M false ψ₂ x✝)
• BSML.eval M true ψ.poss x✝ = (x✝ ∈ Team.poss M.access {s : Finset W | BSML.eval M true ψ s})
• BSML.eval M false ψ.poss x✝ = (x✝ ∈ Team.nec M.access {s : Finset W | BSML.eval M false ψ s})

@[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 is evaluation in the positive polarity.

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 is evaluation in the negative polarity.

Equations

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

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

@[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.

@[simp]

theorem BSML.support_falsum {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) (t : Finset W) : support M Formula.falsum t ↔ t = ∅

The weak contradiction is supported by the empty team only.

theorem BSML.not_support_strongFalsum {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) (t : Finset W) : ¬support M Formula.strongFalsum t

The strong contradiction is supported by no team.

Consequence and equivalence

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

ψ is a consequence of φ when 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

Two formulas are equivalent, φ ≡ ψ, when they have the same support in every model ([Alo22] p. 5:30, [Ant21] Definition 2.1.6, [AAY24] p. 5).

Equations

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

theorem BSML.equivalent_iff {Atom : Type u_1} {W : Type u_2} [DecidableEq W] {φ ψ : Formula Atom} : Equivalent φ ψ ↔ Consequence φ ψ ∧ Consequence ψ φ

Equivalence is mutual consequence.

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

Two formulas are strongly equivalent when they and their negations are equivalent ([AAY24] p. 5), that is, when they have the same support and the same anti-support.

Equations

• BSML.StronglyEquivalent φ ψ = (BSML.Equivalent φ ψ ∧ BSML.Equivalent φ.neg ψ.neg)

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) differs from eval in that ∅ is not among the possible states, so each part of a split is intersected with Team.ne. The exclusion applies wherever states are quantified, in the splits here and on the outer team in ConsequenceStar; the atom, ne and modal clauses keep their BSML form.

Equations

• BSML.evalStar M true (BSML.Formula.atom p) x✝ = (x✝ ∈ Team.flat (M.val p))
• BSML.evalStar M false (BSML.Formula.atom p) x✝ = (x✝ ∈ Team.flat fun (w : W) => ¬M.val p w)
• BSML.evalStar M true BSML.Formula.ne x✝ = (x✝ ∈ Team.ne)
• 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✝ = (x✝ ∈ Team.tensor ({s : Finset W | BSML.evalStar M false ψ₁ s} ∩ Team.ne) ({s : Finset W | BSML.evalStar M false ψ₂ s} ∩ Team.ne))
• BSML.evalStar M true (ψ₁.disj ψ₂) x✝ = (x✝ ∈ Team.tensor ({s : Finset W | BSML.evalStar M true ψ₁ s} ∩ Team.ne) ({s : Finset W | BSML.evalStar M true ψ₂ s} ∩ Team.ne))
• BSML.evalStar M false (ψ₁.disj ψ₂) x✝ = (BSML.evalStar M false ψ₁ x✝ ∧ BSML.evalStar M false ψ₂ x✝)
• BSML.evalStar M true ψ.poss x✝ = (x✝ ∈ Team.poss M.access {s : Finset W | BSML.evalStar M true ψ s})
• BSML.evalStar M false ψ.poss x✝ = (x✝ ∈ Team.nec M.access {s : Finset W | BSML.evalStar M false ψ s})

@[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 is evalStar in the positive polarity.

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 is evalStar in the negative polarity.

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

In BSML*, ψ is a consequence of φ when every non-empty team supporting φ supports ψ.

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) [DecidableRel M.val] (pol : Bool) (φ : Formula Atom) (t : Finset W) : Decidable (eval M pol φ t)

Decidability of eval by structural recursion on the formula, through the operators' instances.

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 (Team.tensor.instDecidableMem (BSML.eval M false ψ₁) (BSML.eval M false ψ₂) x✝)
• BSML.decidableEval M true (ψ₁.disj ψ₂) x✝ = ⋯.mpr (Team.tensor.instDecidableMem (BSML.eval M true ψ₁) (BSML.eval M true ψ₂) x✝)
• BSML.decidableEval M false (ψ₁.disj ψ₂) x✝ = ⋯.mpr instDecidableAnd
• BSML.decidableEval M true ψ.poss x✝ = ⋯.mpr (Team.poss.instDecidableMem M.access (BSML.eval M true ψ) x✝)
• BSML.decidableEval M false ψ.poss x✝ = ⋯.mpr (Team.nec.instDecidableMem M.access (BSML.eval M false ψ) x✝)

@[instance_reducible]

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

Equations

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