BSML Classical Validities

Aloni's bilateral state-based modal logic ([Alo22]) preserves several classical validities despite its non-classical bilateral semantics, and exhibits one non-classical defect: replacement under negation can fail. This module proves the key equivalences and the replacement-failure counterexample.

Main declarations

• box_diamond_duality_support / box_diamond_duality_antiSupport: □φ and ¬◇¬φ are bilaterally equivalent (definitional — □ is an abbreviation).
• deMorgan_conj_support / deMorgan_disj_support (+ anti-support and full-equivalence counterparts): De Morgan laws hold bilaterally.
• dne_equivalent: double negation elimination as a bilateral equivalence.
• disjoint_support_antiSupport: the engine fact — anti-support of φ and support of φ cannot share any world. Proved by structural induction.
• negation_incompatibility: if s supports ¬φ and t supports φ, then s and t are disjoint as finsets.
• replacement_failure_counterexample: a concrete BSMLModel witnessing φ ≡ ψ ⇏ ¬φ ≡ ¬ψ. The pair is p ∧ ¬p versus ¬NE, both supported only by ∅; their negations diverge there.

Implementation notes

The bilateral validities (De Morgan, DNE, box-diamond) all close by Iff.rfl because the substrate (BSML.Defs.eval) is wired so that, e.g., eval M true (.neg (.conj φ ψ)) and eval M true (.disj (.neg φ) (.neg ψ)) are the same clause up to one polarity flip. The proofs are documentary — the content is in Defs.lean, where the design of eval enforces these.

The negation-incompatibility result is one-directional only: support of ¬φ implies incompatibility with every supporter of φ, but the converse fails in BSML ([Alo22] gives a counterexample using ¬((p ∧ NE) ∨ q)). The framing "negation as incompatibility" should not be read as a definitional identification.

Todo

• Engage with [AAY24], which axiomatizes BSML and proves the soundness/completeness results these validities sit underneath.
• Extract the bilateral validities to a Core.Logic.Bilateral.Validities module — they depend only on the IsBilateral polarity-flip structure (already wired via BSML.isBilateral in Defs.lean).

Box-diamond duality

theorem Core.Logic.Modal.BSML.box_diamond_duality_support {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ : BSMLFormula Atom) (t : Finset W) : support M φ.nec t ↔ support M φ.neg.poss.neg t

Box-diamond duality (support): definitionally equal since □ := ¬◇¬.

theorem Core.Logic.Modal.BSML.box_diamond_duality_antiSupport {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ : BSMLFormula Atom) (t : Finset W) : antiSupport M φ.nec t ↔ antiSupport M φ.neg.poss.neg t

Box-diamond duality (anti-support): definitionally equal.

De Morgan laws

theorem Core.Logic.Modal.BSML.deMorgan_conj_support {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ ψ : BSMLFormula Atom) (t : Finset W) : support M (φ.conj ψ).neg t ↔ support M (φ.neg.disj ψ.neg) t

De Morgan for conjunction (support): ¬(φ ∧ ψ) ≡ ¬φ ∨ ¬ψ. Both sides reduce to the same SPLIT existential.

theorem Core.Logic.Modal.BSML.deMorgan_conj_antiSupport {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ ψ : BSMLFormula Atom) (t : Finset W) : antiSupport M (φ.conj ψ).neg t ↔ antiSupport M (φ.neg.disj ψ.neg) t

De Morgan for conjunction (anti-support).

theorem Core.Logic.Modal.BSML.deMorgan_disj_support {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ ψ : BSMLFormula Atom) (t : Finset W) : support M (φ.disj ψ).neg t ↔ support M (φ.neg.conj ψ.neg) t

De Morgan for disjunction (support): ¬(φ ∨ ψ) ≡ ¬φ ∧ ¬ψ.

theorem Core.Logic.Modal.BSML.deMorgan_disj_antiSupport {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ ψ : BSMLFormula Atom) (t : Finset W) : antiSupport M (φ.disj ψ).neg t ↔ antiSupport M (φ.neg.conj ψ.neg) t

De Morgan for disjunction (anti-support).

Bilateral equivalence statements

theorem Core.Logic.Modal.BSML.dne_equivalent {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (φ : BSMLFormula Atom) : equivalent φ.neg.neg φ

DNE is a full bilateral equivalence.

theorem Core.Logic.Modal.BSML.box_diamond_equivalent {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (φ : BSMLFormula Atom) : equivalent φ.nec φ.neg.poss.neg

Box-diamond duality is a full bilateral equivalence.

theorem Core.Logic.Modal.BSML.deMorgan_conj_equivalent {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (φ ψ : BSMLFormula Atom) : equivalent (φ.conj ψ).neg (φ.neg.disj ψ.neg)

De Morgan for conjunction is a full bilateral equivalence.

theorem Core.Logic.Modal.BSML.deMorgan_disj_equivalent {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (φ ψ : BSMLFormula Atom) : equivalent (φ.disj ψ).neg (φ.neg.conj ψ.neg)

De Morgan for disjunction is a full bilateral equivalence.

Negation and incompatibility

theorem Core.Logic.Modal.BSML.disjoint_support_antiSupport {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ : BSMLFormula Atom) {s t : Finset W} (hs : antiSupport M φ s) (ht : support M φ t) : Disjoint s t

Anti-support and support of the same φ are disjoint teams: if s anti-supports φ and t supports φ, no world lies in both.

theorem Core.Logic.Modal.BSML.negation_incompatibility {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ : BSMLFormula Atom) {s t : Finset W} (hs : support M φ.neg s) (ht : support M φ t) : Disjoint s t

Negation and incompatibility: if s supports ¬φ and t supports φ, then s and t are disjoint as finsets.

One-directional only — the converse fails in BSML; see [Alo22].

Failure of replacement under negation

theorem Core.Logic.Modal.BSML.replacement_failure_counterexample : ∃ (W : Type) (x : DecidableEq W) (x_1 : Fintype W) (M : BSMLModel W String) (t : Finset W), (support M ((BSMLFormula.atom "p").conj (BSMLFormula.atom "p").neg) t ↔ support M BSMLFormula.ne.neg t) ∧ ¬(support M ((BSMLFormula.atom "p").conj (BSMLFormula.atom "p").neg).neg t ↔ support M BSMLFormula.ne.neg.neg t)

Failure of replacement under negation: φ ≡ ψ ⇏ ¬φ ≡ ¬ψ.

Counterexample ([Alo22]): ⊥₁ = p ∧ ¬p and ⊥₂ = ¬NE are bilaterally equivalent (both supported only by ∅), but ¬⊥₁ and ¬⊥₂ diverge: ¬(p ∧ ¬p) is supported by every team (including ∅) via the trivial split ∅ ∪ ∅, while ¬¬NE = NE requires a non-empty team.