Documentation

Linglib.Logic.Temporal.Defs

T × W tense-modal logic: frames, language and satisfaction #

A T × W frame has worlds sharing one time order and, at each time, historical equivalence, an equivalence relation on worlds, agreement up to that time, that gets finer as time advances. Its object language has the linear tenses G and H, historical necessity N along historical equivalence and box over all worlds. Each of the four is necessity along a relation, so the logic is a multimodal Kripke logic by construction.

Main definitions #

References #

source
structure Temporal.TWFrame (World : Type v) (T : Type u) [Preorder T] :
Type (max u v)

A T × W frame ([Tho84], [vK97]) has, at each time, historical equivalence on worlds, which gets finer as time advances.

  • sim : T → Setoid World

    Historical equivalence ∼ₜ, relating worlds that share their history up to t.

  • antitone_sim : Antitone self.sim

    Worlds that share their history up to a time share it up to every earlier time.

Instances For
    source
    def Temporal.TWFrame.alt {T : Type u} {World : Type v} [Preorder T] (F : TWFrame World T) (t : T) :
    SetRel World World

    Historical equivalence at t as an accessibility relation.

    Equations
    • F.alt t = {p : World × World | (F.sim t) p.1 p.2}
    Instances For
      source
      def Temporal.TWFrame.ofDatedFacts {T : Type u} {World : Type v} [Preorder T] {Fact : Type u_1} (time : Fact → T) (holds : World → Fact → Prop) :
      TWFrame World T

      Over a stock of dated facts, worlds are historically equivalent up to a time when they agree on every fact dated at or before it, the world–time model of [Tho84].

      Equations
      • Temporal.TWFrame.ofDatedFacts time holds = { sim := fun (t : T) => { r := fun (w w' : World) => ∀ (f : Fact), time f ≤ t → (holds w f ↔ holds w' f), iseqv := ⋯ }, antitone_sim := ⋯ }
      Instances For
        source
        inductive Temporal.OForm (Atom : Type u_1) :
        Type u_1

        The object language L of T × W logic ([vK97] §1).

        • atom {Atom : Type u_1} : Atom → OForm Atom

          A sentential constant.

        • neg {Atom : Type u_1} : OForm Atom → OForm Atom

          Negation.

        • and {Atom : Type u_1} : OForm Atom → OForm Atom → OForm Atom

          Conjunction.

        • G {Atom : Type u_1} : OForm Atom → OForm Atom

          G — "it will always be that" (∀ later times, same world).

        • H {Atom : Type u_1} : OForm Atom → OForm Atom

          H — "it has always been that" (∀ earlier times, same world).

        • N {Atom : Type u_1} : OForm Atom → OForm Atom

          N — historical necessity (∀ ∼ₜ-alternatives, same time).

        • box {Atom : Type u_1} : OForm Atom → OForm Atom

          box — truth in all worlds (von Kutschera's N₄).

        Instances For
          source
          def Temporal.instDecidableEqOForm.decEq {Atom✝ : Type u_1} [DecidableEq Atom✝] (x✝ x✝¹ : OForm Atom✝) :
          Decidable (x✝ = x✝¹)
          Equations
          Instances For
            source
            @[instance_reducible]
            instance Temporal.instDecidableEqOForm {Atom✝ : Type u_1} [DecidableEq Atom✝] :
            DecidableEq (OForm Atom✝)
            Equations
            source
            def Temporal.TWFrame.sat {T : Type u} {World : Type v} {Atom : Type u_1} [Preorder T] (F : TWFrame World T) (V : Atom → T → World → Prop) :
            OForm Atom → T → World → Prop

            Satisfaction V_{t,w}(A) ([vK97]) relative to an atomic valuation V. G/H/N/box are the Kripke boxes □ over, respectively, future precedence <, past precedence >, historical equivalence sim t, and the universal relation — making the object logic a multimodal Kripke logic by construction.

            Equations
            Instances For
              source
              def Temporal.TWFrame.entails {T : Type u} {World : Type v} {Atom : Type u_1} [Preorder T] (F : TWFrame World T) (V : Atom → T → World → Prop) (a b : OForm Atom) :
              Prop

              In a model a entails b when b holds wherever a does.

              Equations
              • F.entails V a b = ∀ (t : T) (w : World), F.sat V a t w → F.sat V b t w
              Instances For

                Derived (dual) operators #

                source
                def Temporal.OForm.M {Atom : Type u_1} (a : OForm Atom) :
                OForm Atom

                Historical possibility M = ¬N¬ (the Ockhamist ◇).

                Equations
                Instances For
                  source
                  def Temporal.OForm.Fut {Atom : Type u_1} (a : OForm Atom) :
                  OForm Atom

                  Tense F — "it will at some point be that" (¬G¬).

                  Equations
                  Instances For
                    source
                    def Temporal.OForm.Pst {Atom : Type u_1} (a : OForm Atom) :
                    OForm Atom

                    Tense P — "it was at some point that" (¬H¬).

                    Equations
                    Instances For
                      source
                      def Temporal.OForm.dia {Atom : Type u_1} (a : OForm Atom) :
                      OForm Atom

                      Possibility in all worlds ◇ = ¬□¬.

                      Equations
                      Instances For