BSML Classical Validities

@cite{aloni-2022}

BSML preserves several classical validities despite its non-classical bilateral semantics. This module proves the key equivalences from @cite{aloni-2022} and formalizes the non-classical properties of bilateral negation.

Key Results

Result	Statement
DNE (Fact 6)	¬¬φ ≡ φ (already in Defs.lean)
Box-Diamond (Fact 6)	□φ ≡ ¬◇¬φ (definitional: □ is an abbreviation)
De Morgan (Fact 6)	¬(φ ∧ ψ) ≡ ¬φ ∨ ¬ψ; ¬(φ ∨ ψ) ≡ ¬φ ∧ ¬ψ
Incompatibility (Fact 7)	s ⊨ ¬φ ⇒ s∩t=∅ for all t ⊨ φ
Replacement failure (Fact 8)	φ ≡ ψ ⇏ ¬φ ≡ ¬ψ (counterexample)

Facts 6 proofs are definitional. Fact 7 connects to the philosophy of negation as incompatibility. Fact 8 demonstrates NE's non-classical behavior.

theorem Semantics.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 Semantics.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.

theorem Semantics.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 Semantics.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 Semantics.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 Semantics.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).

theorem Semantics.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 Semantics.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 Semantics.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 Semantics.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.

theorem Semantics.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 (Fact 7 from @cite{aloni-2022}).

If s supports ¬φ, then s and any t supporting φ are disjoint.

theorem Semantics.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 (Fact 8 from @cite{aloni-2022}).

In BSML, φ ≡ ψ does NOT imply ¬φ ≡ ¬ψ. Counterexample: ⊥₁ = p ∧ ¬p and ⊥₂ = ¬NE are equivalent, but ¬⊥₁ ≠ ¬⊥₂.