Negation in BSML

BSML's negation swaps support and anti-support. It validates double negation elimination, the De Morgan laws and the duality of ◇ and □ as strong equivalences (⊜, same support and same anti-support), and a team supporting a formula is disjoint from every team anti-supporting it. It is not a function of support alone: two formulas with the same support can have negations with different support, so replacement of equivalents fails under ¬. Aloni states these facts for BSML; Aloni, Anttila and Yang distinguish equivalence from strong equivalence.

Main results

• stronglyEquivalent_neg_neg, stronglyEquivalent_neg_conj, stronglyEquivalent_neg_disj, stronglyEquivalent_neg_poss, stronglyEquivalent_neg_nec: the classical laws of negation.
• disjoint_of_support_of_antiSupport: negation is incompatibility.
• exists_equivalent_not_equivalent_neg: replacement of equivalents fails under negation.

Implementation notes

The laws hold by Iff.rfl: the anti-support clause of each connective is the support clause of its De Morgan dual, and □ abbreviates ¬◇¬.

TODO

Aloni, Anttila and Yang's replacement theorem for strong equivalence (Proposition 2.4) needs a substitution operation on formulas.

References

• [Alo22] Aloni, Logic and Conversation: The Case of Free Choice
• [AAY24] Aloni, Anttila and Yang, State-based Modal Logics for Free Choice
• [Ant21] Anttila, The Logic of Free Choice: Axiomatizations of State-based Modal Logics

The classical laws

theorem BSML.stronglyEquivalent_neg_neg {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (φ : Formula Atom) : StronglyEquivalent φ.neg.neg φ

Double negation elimination holds as a strong equivalence, ¬¬φ ⊜ φ ([Alo22] Fact 6, [AAY24] Fact 2.5).

theorem BSML.stronglyEquivalent_neg_conj {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (φ ψ : Formula Atom) : StronglyEquivalent (φ.conj ψ).neg (φ.neg.disj ψ.neg)

The negation of a conjunction is the split disjunction of the negations, ¬(φ ∧ ψ) ⊜ ¬φ ∨ ¬ψ ([Alo22] Fact 6, [AAY24] Fact 2.5).

theorem BSML.stronglyEquivalent_neg_disj {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (φ ψ : Formula Atom) : StronglyEquivalent (φ.disj ψ).neg (φ.neg.conj ψ.neg)

The negation of a split disjunction is the conjunction of the negations, ¬(φ ∨ ψ) ⊜ ¬φ ∧ ¬ψ ([Alo22] Fact 6, [AAY24] Fact 2.5).

theorem BSML.stronglyEquivalent_neg_poss {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (φ : Formula Atom) : StronglyEquivalent φ.poss.neg φ.neg.nec

Negation turns ◇ into □, ¬◇φ ⊜ □¬φ ([Alo22] Fact 6, [AAY24] Fact 2.5).

theorem BSML.stronglyEquivalent_neg_nec {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (φ : Formula Atom) : StronglyEquivalent φ.nec.neg φ.neg.poss

Negation turns □ into ◇, ¬□φ ⊜ ◇¬φ ([Alo22] Fact 6).

Negation and incompatibility

theorem BSML.disjoint_of_support_of_antiSupport {W : Type u_1} [DecidableEq W] {Atom : Type u_2} {M : ModalLogic.KripkeModel W Atom} {φ : Formula Atom} {s t : Finset W} (hs : support M φ s) (ht : antiSupport M φ t) : Disjoint s t

A team supporting φ and a team anti-supporting φ are disjoint ([Alo22] Fact 7, [Ant21] Proposition 3.3.9).

theorem BSML.eq_empty_of_support_of_antiSupport {W : Type u_1} [DecidableEq W] {Atom : Type u_2} {M : ModalLogic.KripkeModel W Atom} {φ : Formula Atom} {s : Finset W} (hs : support M φ s) (hs' : antiSupport M φ s) : s = ∅

A team that supports and anti-supports φ is empty ([Ant21] Proposition 3.3.9).

Failure of replacement under negation

theorem BSML.exists_equivalent_not_equivalent_neg {W : Type u_1} [DecidableEq W] {Atom : Type u_2} [Inhabited Atom] : ∃ (φ : Formula Atom) (ψ : Formula Atom), Equivalent φ ψ ∧ ¬Equivalent φ.neg ψ.neg

Replacement of equivalents fails under negation ([Alo22] Fact 8, [Ant21] Fact 2.2.3). The weak contradictions p ∧ ¬p and ¬NE are both supported by ∅ alone, but the empty team supports ¬(p ∧ ¬p) and not ¬¬NE.