Documentation

Studies.AloniAnttilaYang2024

Aloni, Anttila and Yang (2024): state-based modal logics for free choice #

Aloni, Anttila and Yang extend bilateral state-based modal logic (BSML) in two ways. BSML⨼ adds the global disjunction ⨼, supported when either disjunct is, and BSML⊘ adds the emptiness operator ⊘, supported when its argument is or the state is empty. NE is the only obstruction to downward closure and to the empty-state property, and ⨼ the only obstruction to union closure. All three logics are invariant under bounded bisimulation, and BSML, though union closed, cannot express every union-closed bisimulation-invariant property.

Main results #

Implementation notes #

The three logics are fragments of one syntax: Formula carries ⊥, NE, ⨼ and ⊘ together, and NEFree, GDFree and EmptFree cut out the languages, so each closure property is one theorem under its fragment hypothesis. Expressive completeness (Theorems 3.15 and 3.17) and the natural-deduction systems of §4 are not formalized here; the BSML system lives in Logic/Team/BSML/NaturalDeduction.lean.

References #

Syntax and semantics #

source
inductive AloniAnttilaYang2024.Formula (Atom : Type u_4) :
Type u_4

The formulas of the joint syntax of BSML, BSML⨼ and BSML⊘ (Definition 2.1) are those of BSML together with the weak contradiction ⊥, the global disjunction ⨼ and the emptiness operator ⊘.

Instances For
    source
    def AloniAnttilaYang2024.instReprFormula.repr {Atom✝ : Type u_4} [Repr Atom✝] :
    Formula Atom✝ → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance AloniAnttilaYang2024.instReprFormula {Atom✝ : Type u_4} [Repr Atom✝] :
      Repr (Formula Atom✝)
      Equations
      source
      @[instance_reducible]
      instance AloniAnttilaYang2024.instDecidableEqFormula {Atom✝ : Type u_4} [DecidableEq Atom✝] :
      DecidableEq (Formula Atom✝)
      Equations
      source
      def AloniAnttilaYang2024.instDecidableEqFormula.decEq {Atom✝ : Type u_4} [DecidableEq Atom✝] (x✝ x✝¹ : Formula Atom✝) :
      Decidable (x✝ = x✝¹)
      Equations
      Instances For
        source
        def AloniAnttilaYang2024.Formula.nec {Atom : Type u_3} (φ : Formula Atom) :
        Formula Atom

        □φ := ¬◇¬φ.

        Equations
        Instances For
          source
          def AloniAnttilaYang2024.Formula.NEFree {Atom : Type u_3} :
          Formula Atom → Prop

          φ.NEFree holds when φ contains no NE.

          Equations
          Instances For
            source
            def AloniAnttilaYang2024.Formula.GDFree {Atom : Type u_3} :
            Formula Atom → Prop

            φ.GDFree holds when φ contains no ⨼, that is, when φ is a BSML⊘ formula.

            Equations
            Instances For
              source
              def AloniAnttilaYang2024.Formula.EmptFree {Atom : Type u_3} :
              Formula Atom → Prop

              φ.EmptFree holds when φ contains no ⊘, that is, when φ is a BSML⨼ formula.

              Equations
              Instances For
                source
                @[instance_reducible]
                instance AloniAnttilaYang2024.Formula.instDecidableNEFree {Atom : Type u_3} (φ : Formula Atom) :
                Decidable φ.NEFree
                Equations
                source
                @[instance_reducible]
                instance AloniAnttilaYang2024.Formula.instDecidableGDFree {Atom : Type u_3} (φ : Formula Atom) :
                Decidable φ.GDFree
                Equations
                source
                @[instance_reducible]
                instance AloniAnttilaYang2024.Formula.instDecidableEmptFree {Atom : Type u_3} (φ : Formula Atom) :
                Decidable φ.EmptFree
                Equations
                source
                def AloniAnttilaYang2024.eval {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) :
                Bool → Formula Atom → Finset W → Prop

                Bilateral evaluation eval M b φ t (Definition 2.3) is support when b is true and anti-support when it is false.

                Equations
                Instances For
                  source
                  @[reducible, inline]
                  abbrev AloniAnttilaYang2024.support {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) :
                  Prop
                  Equations
                  Instances For
                    source
                    @[reducible, inline]
                    abbrev AloniAnttilaYang2024.antiSupport {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) :
                    Prop
                    Equations
                    Instances For
                      source
                      @[simp]
                      theorem AloniAnttilaYang2024.support_neg {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) :
                      support M φ.neg t ↔ antiSupport M φ t
                      source
                      @[simp]
                      theorem AloniAnttilaYang2024.antiSupport_neg {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) :
                      antiSupport M φ.neg t ↔ support M φ t
                      source
                      @[simp]
                      theorem AloniAnttilaYang2024.support_bot {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (t : Finset W) :
                      support M Formula.bot t ↔ t = ∅
                      source
                      @[simp]
                      theorem AloniAnttilaYang2024.antiSupport_bot {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (t : Finset W) :
                      antiSupport M Formula.bot t
                      source
                      @[simp]
                      theorem AloniAnttilaYang2024.support_ne {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (t : Finset W) :
                      support M Formula.ne t ↔ t.Nonempty
                      source
                      @[simp]
                      theorem AloniAnttilaYang2024.antiSupport_ne {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (t : Finset W) :
                      antiSupport M Formula.ne t ↔ t = ∅
                      source
                      @[simp]
                      theorem AloniAnttilaYang2024.support_conj {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (φ ψ : Formula Atom) (t : Finset W) :
                      support M (φ.conj ψ) t ↔ support M φ t ∧ support M ψ t
                      source
                      @[simp]
                      theorem AloniAnttilaYang2024.antiSupport_disj {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (φ ψ : Formula Atom) (t : Finset W) :
                      antiSupport M (φ.disj ψ) t ↔ antiSupport M φ t ∧ antiSupport M ψ t
                      source
                      @[simp]
                      theorem AloniAnttilaYang2024.support_gdisj {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (φ ψ : Formula Atom) (t : Finset W) :
                      support M (φ.gdisj ψ) t ↔ support M φ t ∨ support M ψ t
                      source
                      @[simp]
                      theorem AloniAnttilaYang2024.antiSupport_gdisj {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (φ ψ : Formula Atom) (t : Finset W) :
                      antiSupport M (φ.gdisj ψ) t ↔ antiSupport M φ t ∧ antiSupport M ψ t
                      source
                      @[simp]
                      theorem AloniAnttilaYang2024.support_empt {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) :
                      support M φ.empt t ↔ support M φ t ∨ t = ∅
                      source
                      @[simp]
                      theorem AloniAnttilaYang2024.antiSupport_empt {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) :
                      antiSupport M φ.empt t ↔ antiSupport M φ t

                      The §2 equivalences #

                      source
                      theorem AloniAnttilaYang2024.support_empt_iff_gdisj_bot {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) :
                      support M φ.empt t ↔ support M (φ.gdisj Formula.bot) t

                      ⊘φ ≡ φ ⨼ ⊥.

                      source
                      theorem AloniAnttilaYang2024.support_conj_gdisj {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (φ ψ χ : Formula Atom) (t : Finset W) :
                      support M (φ.conj (ψ.gdisj χ)) t ↔ support M ((φ.conj ψ).gdisj (φ.conj χ)) t

                      φ ∧ (ψ ⨼ χ) ≡ (φ ∧ ψ) ⨼ (φ ∧ χ).

                      source
                      theorem AloniAnttilaYang2024.support_disj_gdisj {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (φ ψ χ : Formula Atom) (t : Finset W) :
                      support M (φ.disj (ψ.gdisj χ)) t ↔ support M ((φ.disj ψ).gdisj (φ.disj χ)) t

                      φ ∨ (ψ ⨼ χ) ≡ (φ ∨ ψ) ⨼ (φ ∨ χ).

                      source
                      theorem AloniAnttilaYang2024.support_poss_gdisj {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (φ ψ : Formula Atom) (t : Finset W) :
                      support M (φ.gdisj ψ).poss t ↔ support M (φ.poss.disj ψ.poss) t

                      The diamond converts the global disjunction into the tensor one, ◇(φ ⨼ ψ) ≡ ◇φ ∨ ◇ψ, which makes the rule Conv◇⨼∨ of Theorem 4.3 sound.

                      Closure properties (Fact 2.7) #

                      source
                      theorem AloniAnttilaYang2024.support_empty_of_neFree {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (hNE : φ.NEFree) :
                      support M φ ∅

                      NE-free formulas have the empty-state property.

                      source
                      theorem AloniAnttilaYang2024.isLowerSet_support_of_neFree {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (hNE : φ.NEFree) :
                      IsLowerSet {t : Finset W | support M φ t}

                      NE-free formulas are downward closed.

                      source
                      theorem AloniAnttilaYang2024.supClosed_support_of_gdFree {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (hGD : φ.GDFree) :
                      SupClosed {t : Finset W | support M φ t}

                      ⨼-free formulas are union closed; in particular every BSML⊘ formula is.

                      source
                      theorem AloniAnttilaYang2024.isFlat_support_of_neFree_gdFree {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (hNE : φ.NEFree) (hGD : φ.GDFree) :
                      Team.IsFlat {t : Finset W | support M φ t}

                      Classical formulas — NE-free and ⨼-free — are flat.

                      BSML is not complete for union-closed properties #

                      source
                      theorem AloniAnttilaYang2024.isLowerSet_of_support_empty {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (hGD : φ.GDFree) (hE : φ.EmptFree) :
                      (support M φ ∅ → ∀ (s t : Finset W), t ⊆ s → support M φ s → support M φ t) ∧ (antiSupport M φ ∅ → ∀ (s t : Finset W), t ⊆ s → antiSupport M φ s → antiSupport M φ t)

                      A BSML formula with the empty-state property is downward closed (Lemma 3.18).

                      source
                      def AloniAnttilaYang2024.twoWorlds :
                      ModalLogic.KripkeModel Bool Unit

                      The two-world model of Fact 3.19 makes p true at true only and has no accessible worlds.

                      Equations
                      Instances For
                        source
                        def AloniAnttilaYang2024.splitProperty (s : Finset Bool) :
                        Prop

                        The property ‖(p ∧ NE) ∨ (¬p ∧ NE)‖ ∪ ‖⊥‖ of Fact 3.19 is union closed and bisimulation invariant, yet not expressible in BSML.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          theorem AloniAnttilaYang2024.bsml_not_complete_for_unionClosed :
                          ¬∃ (φ : Formula Unit), φ.GDFree ∧ φ.EmptFree ∧ ∀ (s : Finset Bool), support twoWorlds φ s ↔ splitProperty s

                          No BSML formula expresses splitProperty (Fact 3.19). The property holds on ∅ and on {true, false}, so a BSML formula expressing it would be downward closed (Lemma 3.18) and hold on {true}, where the property fails.

                          The emptiness operator cancels enrichment #

                          source
                          theorem AloniAnttilaYang2024.support_empt_conj_ne {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) (hα : φ.NEFree) :
                          support M (φ.conj Formula.ne).empt t ↔ support M φ t

                          For classical α, ⊘(α ∧ NE) ≡ α (§5), so the emptiness operator undoes the non-emptiness that pragmatic enrichment adds.

                          The embedding of BSML #

                          source
                          def AloniAnttilaYang2024.ofBSML {Atom : Type u_3} :
                          BSML.Formula Atom → Formula Atom

                          BSML formulas as formulas of the joint language.

                          Equations
                          Instances For
                            source
                            theorem AloniAnttilaYang2024.gdFree_ofBSML {Atom : Type u_3} (φ : BSML.Formula Atom) :
                            (ofBSML φ).GDFree
                            source
                            theorem AloniAnttilaYang2024.emptFree_ofBSML {Atom : Type u_3} (φ : BSML.Formula Atom) :
                            (ofBSML φ).EmptFree
                            source
                            theorem AloniAnttilaYang2024.eval_ofBSML {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (t : Finset W) (b : Bool) (φ : BSML.Formula Atom) :
                            eval M b (ofBSML φ) t ↔ BSML.eval M b φ t

                            The embedding preserves bilateral evaluation, so the joint language is a conservative extension of BSML.

                            source
                            theorem AloniAnttilaYang2024.narrowScopeFC {W : Type u_1} [DecidableEq W] {Atom : Type u_3} (M : ModalLogic.KripkeModel W Atom) (t : Finset W) {α β : BSML.Formula Atom} (hα : α.NEFree) (hβ : β.NEFree) (h : support M (ofBSML (BSML.enrich (α.disj β).poss)) t) :
                            support M (ofBSML (α.poss.conj β.poss)) t

                            Narrow-scope free choice, [◇(α ∨ β)]⁺ ⊨ ◇α ∧ ◇β, transported from [Alo22] along the embedding.

                            Bisimulation invariance (Theorem 3.8) #

                            source
                            def AloniAnttilaYang2024.Formula.modalDepth {Atom : Type u_3} :
                            Formula Atom → ℕ

                            The modal depth of a formula is the greatest number of nested ◇s in it.

                            Equations
                            Instances For
                              source
                              theorem AloniAnttilaYang2024.invariant_eval {W : Type u_1} {W' : Type u_2} [DecidableEq W] [DecidableEq W'] {Atom : Type u_3} {M : ModalLogic.KripkeModel W Atom} {M' : ModalLogic.KripkeModel W' Atom} {k : ℕ} (φ : Formula Atom) (hd : φ.modalDepth ≤ k) (b : Bool) :
                              Team.Invariant (fun (x1 : W) (x2 : W') => ModalLogic.WorldBisim k M x1 M' x2) {t : Finset W | eval M b φ t} {t : Finset W' | eval M' b φ t}

                              Teams that are k-bisimilar agree on every formula of modal depth at most k, in both polarities (Theorem 3.8).