Documentation

Linglib.Logic.Team.ModalInclusion

Modal inclusion logic #

Modal inclusion logic ML(⊆) extends classical modal logic with inclusion atoms a ⊆ b, supported by a team when every tuple of truth values that a takes at a world of the team is taken by b at some world of the team. It has support only, no anti-support. Its ◇ is lax: a team supports ◇φ when some team of successors supporting φ reaches every world of the team. ML(⊆) formulas are union closed and supported by the empty team, but the inclusion atom breaks downward closure. Anttila, Häggblom and Yang axiomatize the logic and characterize its expressive power.

Main definitions #

Main results #

Implementation notes #

eval is a fold over the operations of Team/Operations.lean and the inclusion atom Team.incl. It departs from the source in two ways. Inclusion atoms relate lists of atoms, where the source allows classical formulas. Negation applies to any formula, with the source's pointwise clause, where the source restricts it to classical formulas.

TODO #

References #

Syntax #

source
inductive ModalLogic.Inclusion.Formula (Atom : Type u_3) :
Type u_3

The formulas of ML(⊆) ([AHY25] Definition 2.1), with ◇ and □ both primitive. An inclusion atom α₁...αₙ ⊆ β₁...βₙ is the list of pairs [(α₁, β₁), ..., (αₙ, βₙ)].

  • atom {Atom : Type u_3} (p : Atom) : Formula Atom

    Atomic proposition.

  • bot {Atom : Type u_3} : Formula Atom

    Weak contradiction ⊥.

  • incl {Atom : Type u_3} (xys : List (Atom × Atom)) : Formula Atom

    Inclusion atom x⃗ ⊆ y⃗.

  • neg {Atom : Type u_3} (φ : Formula Atom) : Formula Atom

    Classical negation (restricted to classical formulas in the paper; we allow on any formula for uniform recursion).

  • conj {Atom : Type u_3} (φ ψ : Formula Atom) : Formula Atom

    Conjunction.

  • disj {Atom : Type u_3} (φ ψ : Formula Atom) : Formula Atom

    Tensor disjunction.

  • poss {Atom : Type u_3} (φ : Formula Atom) : Formula Atom

    Possibility modal ◇ (lax semantics).

  • nec {Atom : Type u_3} (φ : Formula Atom) : Formula Atom

    Necessity modal □.

Instances For
    source
    @[instance_reducible]
    instance ModalLogic.Inclusion.instReprFormula {Atom✝ : Type u_3} [Repr Atom✝] :
    Repr (Formula Atom✝)
    Equations
    source
    def ModalLogic.Inclusion.instReprFormula.repr {Atom✝ : Type u_3} [Repr Atom✝] :
    Formula Atom✝ → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Classical truth #

      Without inclusion atoms MIL is classical modal logic ([Ant21]'s Proposition 2.2.16 for the lax and image modalities, support_iff_forall_realize below).

      source
      def ModalLogic.Inclusion.Formula.InclFree {Atom : Type u_2} :
      Formula Atom → Prop

      Formula.InclFree φ holds when φ contains no inclusion atom.

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

        Classical Kripke truth of a MIL formula at a world, with ◇ and □ the shared ModalLogic.Diamond and ModalLogic.Box; an inclusion atom is true at every world.

        Equations
        Instances For
          source
          theorem ModalLogic.Inclusion.realize_poss {W : Type u_1} {Atom : Type u_2} {M : KripkeModel W Atom} {ψ : Formula Atom} {w : W} :
          Realize M ψ.poss w ↔ ∃ v ∈ M.access w, Realize M ψ v
          source
          theorem ModalLogic.Inclusion.realize_nec {W : Type u_1} {Atom : Type u_2} {M : KripkeModel W Atom} {ψ : Formula Atom} {w : W} :
          Realize M ψ.nec w ↔ ∀ v ∈ M.access w, Realize M ψ v

          Semantics #

          source
          def ModalLogic.Inclusion.eval {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) :
          Formula Atom → Finset W → Prop

          A team supports a formula ([AHY25] Definition 2.2).

          Equations
          Instances For
            source
            @[reducible, inline]
            abbrev ModalLogic.Inclusion.support {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) :
            Prop

            Support is eval, under its conventional name; ML(⊆) has no anti-support.

            Equations
            Instances For
              source
              @[simp]
              theorem ModalLogic.Inclusion.support_atom {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (p : Atom) (t : Finset W) :
              support M (Formula.atom p) t ↔ ∀ w ∈ t, M.val p w
              source
              @[simp]
              theorem ModalLogic.Inclusion.support_bot {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (t : Finset W) :
              support M Formula.bot t ↔ t = ∅
              source
              @[simp]
              theorem ModalLogic.Inclusion.support_incl {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (xys : List (Atom × Atom)) (t : Finset W) :
              support M (Formula.incl xys) t ↔ ∀ w₁ ∈ t, ∃ w₂ ∈ t, ∀ xy ∈ xys, M.val xy.1 w₁ ↔ M.val xy.2 w₂
              source
              @[simp]
              theorem ModalLogic.Inclusion.support_neg {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) :
              support M φ.neg t ↔ ∀ w ∈ t, ¬support M φ {w}
              source
              @[simp]
              theorem ModalLogic.Inclusion.support_conj {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (φ ψ : Formula Atom) (t : Finset W) :
              support M (φ.conj ψ) t ↔ support M φ t ∧ support M ψ t
              source
              @[simp]
              theorem ModalLogic.Inclusion.support_disj {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (φ ψ : Formula Atom) (t : Finset W) :
              support M (φ.disj ψ) t ↔ ∃ (t₁ : Finset W), support M φ t₁ ∧ ∃ (t₂ : Finset W), support M ψ t₂ ∧ t₁ ∪ t₂ = t
              source
              @[simp]
              theorem ModalLogic.Inclusion.support_poss {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) :
              support M φ.poss t ↔ ∃ S ⊆ t.biUnion M.access, (∀ w ∈ t, ∃ s ∈ S, s ∈ M.access w) ∧ support M φ S
              source
              @[simp]
              theorem ModalLogic.Inclusion.support_nec {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) :
              support M φ.nec t ↔ support M φ (t.biUnion M.access)
              source
              def ModalLogic.Inclusion.Formula.modalDepth {Atom : Type u_2} :
              Formula Atom → ℕ

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

              Equations
              Instances For

                Union closure #

                source
                theorem ModalLogic.Inclusion.supClosed_support {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (φ : Formula Atom) :
                SupClosed {t : Finset W | support M φ t}

                Every MIL formula has union-closed support. Each case is the closure lemma of its connective in Team/Operations.lean, and an inclusion witness in either team is one in the union.

                Empty team property #

                source
                theorem ModalLogic.Inclusion.support_empty {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (φ : Formula Atom) :
                support M φ ∅

                Inclusion breaks downward closure (the defining feature) #

                source
                theorem ModalLogic.Inclusion.not_isLowerSet_incl_of_witness {W : Type u_1} {Atom : Type u_2} [DecidableEq W] {a b : Atom} {w₁ w₂ : W} {M : KripkeModel W Atom} (hpair : M.val a w₁ ↔ M.val b w₂) (hself : M.val a w₂ ↔ M.val b w₂) (hwit : ¬(M.val a w₁ ↔ M.val b w₁)) :
                ¬IsLowerSet {t : Finset W | support M (Formula.incl [(a, b)]) t}

                The inclusion atom is not downward closed. If w₂ supplies the b-value matching both its own and w₁'s a-value but w₁ does not match itself, then {w₁, w₂} supports a ⊆ b and {w₁} does not.

                Bisimulation invariance #

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

                Teams that are k-bisimilar agree on every formula of modal depth at most k ([AHY25] Theorem 3.6).

                source
                theorem ModalLogic.Inclusion.bisimClosed_support {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (φ : Formula Atom) :
                BisimClosed M {t : Finset W | support M φ t}

                The support of a formula is closed under bisimulation at its modal depth.

                Soundness for the closure cell (Definability bridge) #

                source
                theorem ModalLogic.Inclusion.definableClass_support_subset {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) :
                Team.definableClass (support M) ⊆ {P : Team.TeamProperty W | SupClosed P ∧ ∅ ∈ P ∧ BisimClosed M P}

                Every MIL-definable team property is union closed, contains the empty team and is closed under bounded bisimulation. This is the easy inclusion of the expressive completeness of ML(⊆) ([AHY25] §3).

                The classical fragment #

                On incl-free formulas support is pointwise classical truth: the lax and image modalities agree with the flat ones on flat properties (Team.possLax_flat, Team.necImage_flat).

                source
                theorem ModalLogic.Inclusion.support_iff_forall_realize {W : Type u_1} {Atom : Type u_2} [DecidableEq W] {M : KripkeModel W Atom} {φ : Formula Atom} (hI : φ.InclFree) (t : Finset W) :
                support M φ t ↔ ∀ w ∈ t, Realize M φ w

                On incl-free formulas, support is pointwise classical truth.

                source
                theorem ModalLogic.Inclusion.support_singleton_iff_realize {W : Type u_1} {Atom : Type u_2} [DecidableEq W] {M : KripkeModel W Atom} {φ : Formula Atom} {w : W} (hI : φ.InclFree) :
                support M φ {w} ↔ Realize M φ w