Documentation

Linglib.Logic.Team.BSML.NaturalDeduction

Natural deduction for BSML #

Aloni, Anttila and Yang axiomatize BSML by a natural deduction system: the rules BSML shares with its extensions by the global disjunction ⩔ and the emptiness operator, and three ⊥NE-translation rules that simulate ⩔, which BSML lacks. The system grows out of Anttila's thesis. This file encodes it as Derives and proves it sound.

The ∨ rules are constrained because NE breaks downward closure: ∨I introduces only NE-free disjuncts, and the side derivations of ¬I, ∨E and ∨Mon have NE-free undischarged assumptions. The translation rules act on an occurrence [ψ] in the scope of no ¬ and no ◇, where φ[ψ] is equivalent to φ[ψ ∧ NE/ψ] ⩔ φ[ψ ∧ ⊥/ψ].

Main definitions #

Main results #

Implementation notes #

⊥ is Formula.falsum, p ∧ ¬p for the default atom, as in Aloni's original syntax; the paper takes ⊥ as primitive. Contexts are upper bounds on undischarged assumptions, so the NE-freeness conditions on side derivations are conditions on their contexts. The paper chains derivations freely, but substituting a derivation for an assumption of a side derivation can break that side derivation's condition, so composition is the rule cut; weakening follows from it. Result numbers and pages follow arXiv:2305.11777v3.

References #

Contexts #

source
inductive BSML.Formula.Context (Atom : Type u_3) :
Type u_3

A one-hole context whose hole is in the scope of no ¬, except as part of □ = ¬◇¬. These are the positions at which replacement holds ([AAY24] Lemma 4.4).

Instances For
    source
    def BSML.Formula.Context.fill {Atom : Type u_1} :
    Context Atom → Formula Atom → Formula Atom

    C.fill φ is the formula C with φ in its hole.

    Equations
    Instances For
      source
      def BSML.Formula.Context.Distributive {Atom : Type u_1} :
      Context Atom → Prop

      A context is distributive when its hole is under no modality, so that it is built from ∧ and ∨ alone. These are the ⩔-distributive positions of [AAY24] (p. 28).

      Equations
      Instances For
        source
        theorem BSML.Formula.Context.setOf_support_fill {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) (ψ : Formula Atom) {C : Context Atom} :
        C.Distributive → {s : Finset W | support M (C.fill ψ) s} = {s : Finset W | support M (C.fill (ψ.conj ne)) s} ∪ {s : Finset W | support M (C.fill (ψ.conj falsum)) s}

        At a distributive position, ψ splits into ψ ∧ NE and ψ ∧ ⊥. The teams supporting C.fill ψ are those supporting C.fill (ψ ∧ NE) together with those supporting C.fill (ψ ∧ ⊥) ([AAY24] p. 34).

        The system #

        source
        inductive BSML.Derives {Atom : Type u_1} [Inhabited Atom] :
        Set (Formula Atom) → Formula Atom → Prop

        The natural deduction system for BSML ([AAY24] Definition 4.33) has the rules of Definition 4.1, boxes (a)–(f), and the three ⊥NE-translation rules. Derives Γ φ says that φ is derivable from formulas in Γ, and cut composes derivations.

        Instances For
          source
          def BSML.«term_⊢_» :
          Lean.TrailingParserDescr

          The natural deduction system for BSML ([AAY24] Definition 4.33) has the rules of Definition 4.1, boxes (a)–(f), and the three ⊥NE-translation rules. Derives Γ φ says that φ is derivable from formulas in Γ, and cut composes derivations.

          Equations
          • BSML.«term_⊢_» = Lean.ParserDescr.trailingNode `BSML.«term_⊢_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢ ") (Lean.ParserDescr.cat `term 51))
          Instances For

            Soundness #

            source
            theorem BSML.soundness {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Inhabited Atom] {Γ : Set (Formula Atom)} {φ : Formula Atom} (h : Derives Γ φ) (M : ModalLogic.KripkeModel W Atom) (s : Finset W) :
            (∀ γ ∈ Γ, support M γ s) → support M φ s

            Soundness ([AAY24] Theorem 4.34). Every team supporting the premises supports what they derive.

            source
            theorem BSML.consequence_of_derives {Atom : Type u_1} {W : Type u_2} [DecidableEq W] [Inhabited Atom] {φ ψ : Formula Atom} (h : Derives {φ} ψ) :
            Consequence φ ψ

            A derivation from one premise is a consequence in the sense of Consequence.

            Derived rules #

            source
            theorem BSML.Derives.single {Atom : Type u_1} [Inhabited Atom] (φ : Formula Atom) :
            Derives {φ} φ

            A formula derives itself.

            source
            theorem BSML.Derives.mono {Atom : Type u_1} [Inhabited Atom] {Γ Δ : Set (Formula Atom)} {φ : Formula Atom} (hΓΔ : Γ ⊆ Δ) (h : Derives Γ φ) :
            Derives Δ φ

            A derivation from Γ is a derivation from any larger set.

            source
            theorem BSML.Derives.cut' {Atom : Type u_1} [Inhabited Atom] {Γ : Set (Formula Atom)} {φ ψ : Formula Atom} (h₁ : Derives Γ φ) (h₂ : Derives (insert φ Γ) ψ) :
            Derives Γ ψ

            cut applies within one set of premises.

            source
            theorem BSML.Derives.trans {Atom : Type u_1} [Inhabited Atom] {Γ : Set (Formula Atom)} {φ ψ : Formula Atom} (h₁ : Derives Γ φ) (h₂ : Derives {φ} ψ) :
            Derives Γ ψ

            Derivations compose with a derivation from a single premise.

            source
            theorem BSML.Derives.conj {Atom : Type u_1} [Inhabited Atom] {Γ : Set (Formula Atom)} {φ ψ : Formula Atom} (h₁ : Derives Γ φ) (h₂ : Derives Γ ψ) :
            Derives Γ (φ.conj ψ)

            ∧I applies within one set of premises.

            source
            theorem BSML.Derives.possMon' {Atom : Type u_1} [Inhabited Atom] {Γ : Set (Formula Atom)} {φ ψ : Formula Atom} (h₁ : Derives Γ φ.poss) (h₂ : Derives {φ} ψ) :
            Derives Γ ψ.poss

            ◇Mon applies with the premise first.

            source
            theorem BSML.Derives.disjMon' {Atom : Type u_1} [Inhabited Atom] {Γ : Set (Formula Atom)} {φ ψ χ : Formula Atom} (h₁ : Derives Γ (φ.disj ψ)) (h₂ : Derives {ψ} χ) :
            Derives Γ (φ.disj χ)

            ∨Mon applies with a side derivation from the replaced disjunct alone.

            source
            theorem BSML.Derives.fill {Atom : Type u_1} [Inhabited Atom] {φ ψ : Formula Atom} (h : Derives {φ} ψ) (C : Formula.Context Atom) :
            Derives {C.fill φ} (C.fill ψ)

            Replacement ([AAY24] Lemma 4.4). A derivation of ψ from φ carries over to any context in which the hole is under no ¬ except as part of □.

            Derivations from the papers #

            source
            theorem BSML.strongFalsum_derives {Atom : Type u_1} [Inhabited Atom] (φ : Formula Atom) :
            Derives {Formula.strongFalsum} φ

            The strong contradiction derives everything ([AAY24] Lemma 4.2).

            source
            theorem BSML.derives_neg_falsum {Atom : Type u_1} [Inhabited Atom] :
            Derives ∅ Formula.falsum.neg

            The strong tautology ¬⊥ is derivable from no premises.

            source
            theorem BSML.conj_disj_derives_disj_conj {Atom : Type u_1} [Inhabited Atom] {φ ψ χ : Formula Atom} (hφ : φ.NEFree) :
            Derives {φ.conj (ψ.disj χ)} ((φ.conj ψ).disj (φ.conj χ))

            Conjunction with an NE-free formula distributes over ∨ ([AAY24] Proposition 4.6 (i)). Each disjunct needs φ, which only cut can supply without putting the premise into a side derivation.

            source
            theorem BSML.disj_conj_ne_derives_conj_ne {Atom : Type u_1} [Inhabited Atom] {φ ψ : Formula Atom} :
            Derives {φ.disj (ψ.conj Formula.ne)} ((φ.disj (ψ.conj Formula.ne)).conj Formula.ne)

            A disjunction with an NE-conjunct is nonempty ([AAY24] Lemma 4.17). The paper derives it with ⩔; here ⊥NETrs on the hole splits the premise, and its ⊥-branch closes by ⊥⊥Ctr.

            source
            theorem BSML.poss_derives_poss_conj_ne {Atom : Type u_1} [Inhabited Atom] {φ : Formula Atom} :
            Derives {φ.poss} (φ.conj Formula.ne).poss

            A possibility has a nonempty witness ([AAY24] Lemma 4.21). ◇⊥NETrs splits ◇φ into ◇(φ ∧ NE) ∨ ◇(φ ∧ ⊥), and ◇⊥ refutes itself.

            source
            theorem BSML.poss_disj_conj_ne_derives_conj_poss {Atom : Type u_1} [Inhabited Atom] {φ ψ : Formula Atom} :
            Derives {((φ.conj Formula.ne).disj (ψ.conj Formula.ne)).poss} (φ.poss.conj ψ.poss)

            Free choice ([Ant21] Proposition 4.2.5, p. 71). A possibility of a disjunction of nonempty disjuncts yields both possibilities, by ◇Sep once directly and once after Com∨.

            Non-derivations #

            source
            theorem BSML.not_atom_derives_disj_ne {Atom : Type u_1} [Inhabited Atom] (p : Atom) :
            ¬Derives {Formula.atom p} ((Formula.atom p).disj Formula.ne)

            Unrestricted ∨I would be unsound, since p ⊬ p ∨ NE. The empty team supports p but not p ∨ NE ([AAY24] p. 19).

            source
            theorem BSML.not_poss_disj_derives_conj_poss {Atom : Type u_1} [Inhabited Atom] {p q : Atom} (hpq : p ≠ q) :
            ¬Derives {((Formula.atom p).disj (Formula.atom q)).poss} ((Formula.atom p).poss.conj (Formula.atom q).poss)

            Free choice fails without enrichment, ◇(p ∨ q) ⊬ ◇p ∧ ◇q for distinct atoms. A world that sees only a q-world is a zero-model of ◇(p ∨ q), the empty team witnessing p, but does not support ◇p, as at the world w_∅ of the state s_b in [AAY24] Figure 3(b) (pp. 6–7).