Natural deduction for BSML, and its soundness

[AAY24] [Ant25] [Alo22]

The natural deduction system for BSML of [AAY24] (Definition 4.1 boxes (a)–(f), shared by all three systems of the paper; the same system is [Ant25] Definition 2.4.1), encoded as an inductive derivability relation Derives, with soundness (soundness, the paper's Theorem 4.3 restricted to the shared rules): derivable consequence is team-semantic consequence over every model.

The rules for ∨ are constrained because NE breaks downward and union closure: ∨I requires the introduced disjunct NE-free, and the subderivation contexts of ∨E/∨Mon/¬I must be NE-free. The classical-fragment metavariables of ¬I/¬E are NE-freeness side conditions here, since ML is exactly the NE-free fragment.

Main declarations

• BSMLFormula.bot, BSMLFormula.botbot — the weak contradiction p ∧ ¬p ([Alo22]'s definition; the paper takes ⊥ as primitive only to simplify exposition) and the strong contradiction ⊥ ∧ NE.
• support_bot_iff — ⊥ is supported exactly by the empty team.
• eq_empty_of_support_antiSupport — NE-free formulas are bilaterally consistent off the empty team.
• support_singleton_or_antiSupport_singleton — bilateral determinacy of NE-free formulas on singletons.
• Derives — the shared-core natural deduction system; Derives Γ φ is the paper's Γ ⊢ φ (contexts are upper bounds on undischarged assumptions, with explicit weaken).
• soundness — Derives Γ φ implies Γ ⊨ φ on every model.

Implementation notes

• BSMLFormula has no ⊥ primitive (and eval's shape is load-bearing downstream), so rules mentioning ⊥ are parameterized by a witness atom p; support_bot_iff shows support is p-independent.
• The three ⊥NETrs substitution rules completing the full BSML system ([AAY24] Definition 4.33) simulate the global disjunction of BSML⫶ and need an occurrence-substitution apparatus; they matter for completeness, not soundness, and are not yet encoded.
• □Mon is finitary via a List of discharged premises, matching the paper's n-ary rule without needing DecidableEq on formulas.

Contradictions

def Core.Logic.Modal.BSML.BSMLFormula.bot {Atom : Type u_1} (p : Atom) : BSMLFormula Atom

The weak contradiction ⊥ := p ∧ ¬p ([Alo22]; supported exactly by the empty team, for every choice of p — support_bot_iff).

Equations

• Core.Logic.Modal.BSML.BSMLFormula.bot p = (Core.Logic.Modal.BSML.BSMLFormula.atom p).conj (Core.Logic.Modal.BSML.BSMLFormula.atom p).neg

def Core.Logic.Modal.BSML.BSMLFormula.botbot {Atom : Type u_1} (p : Atom) : BSMLFormula Atom

The strong contradiction ⊥⊥ := ⊥ ∧ NE (supported by no team).

Equations

• Core.Logic.Modal.BSML.BSMLFormula.botbot p = (Core.Logic.Modal.BSML.BSMLFormula.bot p).conj Core.Logic.Modal.BSML.BSMLFormula.ne

theorem Core.Logic.Modal.BSML.support_bot_iff {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (M : BSMLModel W Atom) (p : Atom) (s : Finset W) : support M (BSMLFormula.bot p) s ↔ s = ∅

theorem Core.Logic.Modal.BSML.not_support_botbot {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] (M : BSMLModel W Atom) (p : Atom) (s : Finset W) : ¬support M (BSMLFormula.botbot p) s

Classical-fragment lemmas

NE-free formulas behave classically: bilaterally consistent off the empty team, and bilaterally determined on singletons ([Alo22] Fact 15; [AAY24]'s α, β ∈ ML metavariable convention rests on these). Anti-support facts come free from support facts at .neg φ, which is NE-free exactly when φ is.

theorem Core.Logic.Modal.BSML.eq_empty_of_support_antiSupport {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] {φ : BSMLFormula Atom} (hNE : φ.isNEFree = true) (M : BSMLModel W Atom) (s : Finset W) : support M φ s → antiSupport M φ s → s = ∅

NE-free formulas cannot be both supported and anti-supported on a nonempty team.

theorem Core.Logic.Modal.BSML.support_singleton_or_antiSupport_singleton {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] {φ : BSMLFormula Atom} (hNE : φ.isNEFree = true) (M : BSMLModel W Atom) (w : W) : support M φ {w} ∨ antiSupport M φ {w}

Bilateral determinacy on singletons for NE-free formulas: every singleton team supports or anti-supports.

The natural deduction system

inductive Core.Logic.Modal.BSML.Derives {Atom : Type u_1} : Set (BSMLFormula Atom) → BSMLFormula Atom → Prop

The shared-core natural deduction system for BSML ([AAY24] Definition 4.1 boxes (a)–(f) = [Ant25] Definition 2.4.1; these are the ⫶-free rules of every system in the paper, and all of Definition 4.33's BSML system except the three ⊥NETrs substitution rules). Derives Γ φ is the paper's Γ ⊢ φ: contexts are upper bounds on undischarged assumptions (weaken is the formal counterpart of the paper's "derivable from formulas in Φ"), so NE-freeness side conditions on subderivation contexts match the paper's conditions on undischarged assumptions. Rules mentioning ⊥ carry a witness atom p (BSMLFormula.bot).

• hyp {Atom : Type u_1} (φ : BSMLFormula Atom) : Derives {φ} φ

  Assumption.

• weaken {Atom : Type u_1} {Γ Δ : Set (BSMLFormula Atom)} {φ : BSMLFormula Atom} : Derives Γ φ → Derives (Γ ∪ Δ) φ

  Weakening (the paper's subset-closure of Φ ⊢ ψ).

• conjI {Atom : Type u_1} {Γ₁ Γ₂ : Set (BSMLFormula Atom)} {φ ψ : BSMLFormula Atom} : Derives Γ₁ φ → Derives Γ₂ ψ → Derives (Γ₁ ∪ Γ₂) (φ.conj ψ)

  ∧I.

• conjE₁ {Atom : Type u_1} {Γ : Set (BSMLFormula Atom)} {φ ψ : BSMLFormula Atom} : Derives Γ (φ.conj ψ) → Derives Γ φ

  ∧E (left).

• conjE₂ {Atom : Type u_1} {Γ : Set (BSMLFormula Atom)} {φ ψ : BSMLFormula Atom} : Derives Γ (φ.conj ψ) → Derives Γ ψ

  ∧E (right).

• negI {Atom : Type u_1} {Γ : Set (BSMLFormula Atom)} {α : BSMLFormula Atom} (p : Atom) : α.isNEFree = true → (∀ γ ∈ Γ, γ.isNEFree = true) → Derives (insert α Γ) (BSMLFormula.bot p) → Derives Γ α.neg

  ¬I: classical α, NE-free undischarged assumptions.

• negE {Atom : Type u_1} {Γ₁ Γ₂ : Set (BSMLFormula Atom)} {α β : BSMLFormula Atom} : α.isNEFree = true → β.isNEFree = true → Derives Γ₁ α → Derives Γ₂ α.neg → Derives (Γ₁ ∪ Γ₂) β

  ¬E: ex falso for the classical fragment.

• dneE {Atom : Type u_1} {Γ : Set (BSMLFormula Atom)} {φ : BSMLFormula Atom} : Derives Γ φ.neg.neg → Derives Γ φ

  ¬¬E (downward half of the invertible rule).

• dneI {Atom : Type u_1} {Γ : Set (BSMLFormula Atom)} {φ : BSMLFormula Atom} : Derives Γ φ → Derives Γ φ.neg.neg

  ¬¬E (upward half).

• dmConjE {Atom : Type u_1} {Γ : Set (BSMLFormula Atom)} {φ ψ : BSMLFormula Atom} : Derives Γ (φ.conj ψ).neg → Derives Γ (φ.neg.disj ψ.neg)

  DM∧ (downward half).

• dmConjI {Atom : Type u_1} {Γ : Set (BSMLFormula Atom)} {φ ψ : BSMLFormula Atom} : Derives Γ (φ.neg.disj ψ.neg) → Derives Γ (φ.conj ψ).neg

  DM∧ (upward half).

• dmDisjE {Atom : Type u_1} {Γ : Set (BSMLFormula Atom)} {φ ψ : BSMLFormula Atom} : Derives Γ (φ.disj ψ).neg → Derives Γ (φ.neg.conj ψ.neg)

  DM∨ (downward half).

• dmDisjI {Atom : Type u_1} {Γ : Set (BSMLFormula Atom)} {φ ψ : BSMLFormula Atom} : Derives Γ (φ.neg.conj ψ.neg) → Derives Γ (φ.disj ψ).neg

  DM∨ (upward half).

• negNeE {Atom : Type u_1} {Γ : Set (BSMLFormula Atom)} (p : Atom) : Derives Γ BSMLFormula.ne.neg → Derives Γ (BSMLFormula.bot p)

  ¬NEE (downward half).

• negNeI {Atom : Type u_1} {Γ : Set (BSMLFormula Atom)} {p : Atom} : Derives Γ (BSMLFormula.bot p) → Derives Γ BSMLFormula.ne.neg

  ¬NEE (upward half).

• disjI {Atom : Type u_1} {Γ : Set (BSMLFormula Atom)} {φ ψ : BSMLFormula Atom} : ψ.isNEFree = true → Derives Γ φ → Derives Γ (φ.disj ψ)

  ∨I: the introduced disjunct must be NE-free.

• disjW {Atom : Type u_1} {Γ : Set (BSMLFormula Atom)} {φ : BSMLFormula Atom} : Derives Γ φ → Derives Γ (φ.disj φ)

  ∨W: unconstrained introduction of the premise itself.

• disjCom {Atom : Type u_1} {Γ : Set (BSMLFormula Atom)} {φ ψ : BSMLFormula Atom} : Derives Γ (φ.disj ψ) → Derives Γ (ψ.disj φ)

  Com∨.

• disjAss {Atom : Type u_1} {Γ : Set (BSMLFormula Atom)} {φ ψ χ : BSMLFormula Atom} : Derives Γ (φ.disj (ψ.disj χ)) → Derives Γ ((φ.disj ψ).disj χ)

  Ass∨.

• disjE {Atom : Type u_1} {Γ Δ₁ Δ₂ : Set (BSMLFormula Atom)} {φ ψ χ : BSMLFormula Atom} : (∀ γ ∈ Δ₁, γ.isNEFree = true) → (∀ γ ∈ Δ₂, γ.isNEFree = true) → Derives Γ (φ.disj ψ) → Derives (insert φ Δ₁) χ → Derives (insert ψ Δ₂) χ → Derives (Γ ∪ Δ₁ ∪ Δ₂) χ

  ∨E: NE-free subderivation contexts (the ⫶-freeness condition on χ is vacuous in the ⫶-free language).

• disjMon {Atom : Type u_1} {Γ Δ : Set (BSMLFormula Atom)} {φ ψ χ : BSMLFormula Atom} : (∀ γ ∈ Δ, γ.isNEFree = true) → Derives Γ (φ.disj ψ) → Derives (insert ψ Δ) χ → Derives (Γ ∪ Δ) (φ.disj χ)

  ∨Mon: NE-free subderivation context.

• botE {Atom : Type u_1} {Γ : Set (BSMLFormula Atom)} {p : Atom} {φ : BSMLFormula Atom} : Derives Γ ((BSMLFormula.bot p).disj φ) → Derives Γ φ

  ⊥E.

• botbotCtr {Atom : Type u_1} {Γ : Set (BSMLFormula Atom)} {p : Atom} {φ : BSMLFormula Atom} (ψ : BSMLFormula Atom) : Derives Γ ((BSMLFormula.botbot p).disj φ) → Derives Γ ψ

  ⊥⊥Ctr.

• possMon {Atom : Type u_1} {Γ : Set (BSMLFormula Atom)} {φ ψ : BSMLFormula Atom} : Derives {φ} ψ → Derives Γ φ.poss → Derives Γ ψ.poss

  ◇Mon: the subderivation has φ as its only undischarged assumption.

• necMon {Atom : Type u_1} {Γ : Set (BSMLFormula Atom)} {ψ : BSMLFormula Atom} (φs : List (BSMLFormula Atom)) : Derives {δ : BSMLFormula Atom | δ ∈ φs} ψ → (∀ δ ∈ φs, Derives Γ δ.nec) → Derives Γ ψ.nec

  □Mon (finitary): the subderivation's undischarged assumptions are among the boxed premises.

• interE {Atom : Type u_1} {Γ : Set (BSMLFormula Atom)} {φ : BSMLFormula Atom} : Derives Γ φ.poss.neg → Derives Γ φ.neg.nec

  Inter◇□ (downward half).

• interI {Atom : Type u_1} {Γ : Set (BSMLFormula Atom)} {φ : BSMLFormula Atom} : Derives Γ φ.neg.nec → Derives Γ φ.poss.neg

  Inter◇□ (upward half).

• possSep {Atom : Type u_1} {Γ : Set (BSMLFormula Atom)} {φ ψ : BSMLFormula Atom} : Derives Γ (φ.disj (ψ.conj BSMLFormula.ne)).poss → Derives Γ ψ.poss

  ◇Sep (FC-entailment for pragmatically enriched formulas).

• possJoin {Atom : Type u_1} {Γ₁ Γ₂ : Set (BSMLFormula Atom)} {φ ψ : BSMLFormula Atom} : Derives Γ₁ φ.poss → Derives Γ₂ ψ.poss → Derives (Γ₁ ∪ Γ₂) (φ.disj ψ).poss

  ◇Join.

• necInst {Atom : Type u_1} {Γ : Set (BSMLFormula Atom)} {φ : BSMLFormula Atom} : Derives Γ (φ.conj BSMLFormula.ne).nec → Derives Γ φ.poss

  □Inst: □ implies ◇ when accessible worlds exist.

• necPossJoin {Atom : Type u_1} {Γ₁ Γ₂ : Set (BSMLFormula Atom)} {φ ψ : BSMLFormula Atom} : Derives Γ₁ φ.nec → Derives Γ₂ ψ.poss → Derives (Γ₁ ∪ Γ₂) (φ.disj ψ).nec

  □◇Join.

Soundness

theorem Core.Logic.Modal.BSML.soundness {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Fintype W] {Γ : Set (BSMLFormula Atom)} {φ : BSMLFormula Atom} (h : Derives Γ φ) (M : BSMLModel W Atom) (s : Finset W) : (∀ γ ∈ Γ, support M γ s) → support M φ s

Soundness ([AAY24] Theorem 4.3, restricted to the shared-core rules): derivable consequence is team-semantic consequence — on every model, every team supporting all of Γ supports φ. The ∨-rule cases run on the closure pillars: NE-free downward closure (isLowerSet_support_of_isNEFree) for discharging side-conditioned contexts on sub-teams, and unrestricted union closure (supClosed_support) for reassembling ∨E's conclusion.