Documentation

Linglib.Logic.Team.BSML.Classical

The classical fragment of BSML #

The NE-free fragment of BSML, Aloni's BSML∅, behaves like classical modal logic. A BSML formula is classically true at a single world, Realize, with the modal clause taken from ModalLogic.Diamond, and on NE-free formulas team support is classical truth at every world of the team, in both polarities. Consequence and equivalence then coincide with their classical definitions, as Aloni and Anttila observe.

Main definitions #

Main results #

Implementation notes #

Realize is total: NE is true at every world, since singletons are non-empty, so the equations of Proposition 2.2.16 are stated for NE-free formulas only, as in the sources. The proposition is one induction over the polarity parameter of eval, with the split clauses discharged by Team.mem_tensor_flat and the ◇-support clause by Team.exists_nonempty_subset_forall_iff. Flatness of the NE-free fragment is also derived from its closure properties in Properties.lean (isFlat_support_of_neFree).

References #

Classical truth #

source
def BSML.Realize {W : Type u_1} {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) :
Formula Atom → W → Prop

Realize M φ w is the classical Kripke truth of φ at the world w. Split disjunction is pointwise, ◇ is ModalLogic.Diamond over M.accessible, and NE is true.

Equations
Instances For
    source
    @[instance_reducible]
    instance BSML.instDecidableRealize {W : Type u_1} {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) [DecidableRel M.val] (φ : Formula Atom) (w : W) :
    Decidable (Realize M φ w)
    Equations
    source
    @[simp]
    theorem BSML.realize_atom {W : Type u_1} {Atom : Type u_2} {M : ModalLogic.KripkeModel W Atom} {w : W} {p : Atom} :
    Realize M (Formula.atom p) w ↔ M.val p w
    source
    @[simp]
    theorem BSML.realize_ne {W : Type u_1} {Atom : Type u_2} {M : ModalLogic.KripkeModel W Atom} {w : W} :
    Realize M Formula.ne w
    source
    @[simp]
    theorem BSML.realize_neg {W : Type u_1} {Atom : Type u_2} {M : ModalLogic.KripkeModel W Atom} {ψ : Formula Atom} {w : W} :
    Realize M ψ.neg w ↔ ¬Realize M ψ w
    source
    @[simp]
    theorem BSML.realize_conj {W : Type u_1} {Atom : Type u_2} {M : ModalLogic.KripkeModel W Atom} {ψ₁ ψ₂ : Formula Atom} {w : W} :
    Realize M (ψ₁.conj ψ₂) w ↔ Realize M ψ₁ w ∧ Realize M ψ₂ w
    source
    @[simp]
    theorem BSML.realize_disj {W : Type u_1} {Atom : Type u_2} {M : ModalLogic.KripkeModel W Atom} {ψ₁ ψ₂ : Formula Atom} {w : W} :
    Realize M (ψ₁.disj ψ₂) w ↔ Realize M ψ₁ w ∨ Realize M ψ₂ w
    source
    theorem BSML.realize_poss {W : Type u_1} {Atom : Type u_2} {M : ModalLogic.KripkeModel W Atom} {ψ : Formula Atom} {w : W} :
    Realize M ψ.poss w ↔ ∃ v ∈ M.access w, Realize M ψ v

    The ◇ clause is ModalLogic.Diamond over M.accessible, definitionally.

    source
    theorem BSML.realize_nec {W : Type u_1} {Atom : Type u_2} {M : ModalLogic.KripkeModel W Atom} {ψ : Formula Atom} {w : W} :
    Realize M ψ.nec w ↔ ModalLogic.Box M.accessible (Realize M ψ) w

    Support is pointwise truth (Proposition 2.2.16) #

    source
    theorem BSML.eval_iff_forall_realize {W : Type u_1} {Atom : Type u_2} {M : ModalLogic.KripkeModel W Atom} {φ : Formula Atom} [DecidableEq W] (hNE : φ.NEFree) (b : Bool) (t : Finset W) :
    eval M b φ t ↔ ∀ w ∈ t, Realize M φ w ↔ b = true

    An NE-free formula is supported by t iff it is true at every world of t, and anti-supported iff it is false at every world of t ([Ant21] Proposition 2.2.16, both polarities at once).

    source
    theorem BSML.support_iff_forall_realize {W : Type u_1} {Atom : Type u_2} {M : ModalLogic.KripkeModel W Atom} {φ : Formula Atom} [DecidableEq W] {t : Finset W} (hNE : φ.NEFree) :
    support M φ t ↔ ∀ w ∈ t, Realize M φ w
    source
    theorem BSML.antiSupport_iff_forall_not_realize {W : Type u_1} {Atom : Type u_2} {M : ModalLogic.KripkeModel W Atom} {φ : Formula Atom} [DecidableEq W] {t : Finset W} (hNE : φ.NEFree) :
    antiSupport M φ t ↔ ∀ w ∈ t, ¬Realize M φ w
    source
    theorem BSML.support_singleton_iff_realize {W : Type u_1} {Atom : Type u_2} {M : ModalLogic.KripkeModel W Atom} {φ : Formula Atom} {w : W} [DecidableEq W] (hNE : φ.NEFree) :
    support M φ {w} ↔ Realize M φ w

    A singleton team supports an NE-free formula iff its world realizes it, {w} ⊨⁺ φ ↔ M, w ⊨ φ.

    source
    theorem BSML.antiSupport_singleton_iff_not_realize {W : Type u_1} {Atom : Type u_2} {M : ModalLogic.KripkeModel W Atom} {φ : Formula Atom} {w : W} [DecidableEq W] (hNE : φ.NEFree) :
    antiSupport M φ {w} ↔ ¬Realize M φ w

    Consequence is classical consequence (Fact 15) #

    source
    def BSML.ClassicalConsequence {W : Type u_1} {Atom : Type u_2} (φ ψ : Formula Atom) :
    Prop

    ψ is a classical modal consequence of φ when every world of every model realizing φ realizes ψ.

    Equations
    Instances For
      source
      theorem BSML.consequence_iff_classicalConsequence {W : Type u_1} {Atom : Type u_2} {φ ψ : Formula Atom} [DecidableEq W] (hφ : φ.NEFree) (hψ : ψ.NEFree) :
      Consequence φ ψ ↔ ClassicalConsequence φ ψ

      On NE-free formulas BSML consequence is classical modal consequence ([Alo22] Fact 15, [Ant21] Fact 2.2.17).

      source
      theorem BSML.equivalent_iff_classicalConsequence {W : Type u_1} {Atom : Type u_2} {φ ψ : Formula Atom} [DecidableEq W] (hφ : φ.NEFree) (hψ : ψ.NEFree) :
      Equivalent φ ψ ↔ ClassicalConsequence φ ψ ∧ ClassicalConsequence ψ φ

      On NE-free formulas equivalence is mutual classical consequence ([Ant21] Fact 2.2.17).