Basic Temporal Logic (BTL)

The basic temporal language has two unary modalities: F (sometime in the future) and P (sometime in the past).

Notation

Open Cslib.Logic.Modal.BTL for the directions F and P and the judgement BTL[m,w ⊨ φ]. With Cslib.Logic open, use the standard dynamic modalities d⟨F⟩φ and d⟨P⟩φ for sometime in the future and past, and d[F]φ and d[P]φ for always in the future and past. Satisfaction is expressed by ⇓BTL[m,w ⊨ φ], using the modal inference system.

References

• P. Blackburn, M. de Rijke, Y. Venema, Modal Logic

inductive Cslib.Logic.Modal.BTL.Direction : Type

The two directions of the basic temporal language.

• F : Direction

  Into the future.

• P : Direction

  Into the past.

@[instance_reducible]

instance Cslib.Logic.Modal.BTL.instDecidableEqDirection : DecidableEq Direction

Equations

• Cslib.Logic.Modal.BTL.instDecidableEqDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev Cslib.Logic.Modal.BTL.τBTL : PFunctor.{0, 0}

The modal signature of the basic temporal language.

Equations

• Cslib.Logic.Modal.BTL.τBTL = PFunctor.mkUnary Cslib.Logic.Modal.BTL.Direction

@[reducible, inline]

abbrev Cslib.Logic.Modal.BTL.Proposition (Atom : Type u_1) : Type u_1

Temporal propositions, with a unary modality for each direction.

Equations

• Cslib.Logic.Modal.BTL.Proposition Atom = Cslib.Logic.Modal.Proposition Cslib.Logic.Modal.BTL.τBTL Atom

theorem Cslib.Logic.Modal.BTL.Proposition.always_eq_not_future_not {Atom : Type u_1} (φ : Proposition Atom) : HasDynamicBox.dynBox F φ = HasNot.not (HasDynamicDiamond.dynDiamond F (HasNot.not φ))

theorem Cslib.Logic.Modal.BTL.Proposition.hasAlwaysBeen_eq_not_past_not {Atom : Type u_1} (φ : Proposition Atom) : HasDynamicBox.dynBox P φ = HasNot.not (HasDynamicDiamond.dynDiamond P (HasNot.not φ))

structure Cslib.Logic.Modal.BTL.Model (World : Sort u_1) (Atom : Sort u_2) : Sort (max (max 1 u_1) u_2)

A temporal model consists of an accessibility relation and a valuation at each world.

No order properties are imposed on the relation. In particular, the modalities include the present only when the relation is reflexive at the current world, and the flow of time is modelled only when the relation is transitive.

• r : World → World → Prop

  The accessibility relation.

• v : World → Atom → Prop

  Valuation of atoms at each world.

def Cslib.Logic.Modal.BTL.Model.toFrame {World : Type u_1} {Atom : Sort u_2} (m : Model World Atom) : Frame World τBTL

The bidirectional frame of a temporal model.

This definition guarantees by construction that the future and past accessibility relations are inverse of each other. Modally, this is witnessed by btl_future_past_prop and btl_past_future_prop.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.Logic.Modal.BTL.Model.toModal {World : Type u_1} {Atom : Type u_2} (m : Model World Atom) : Modal.Model World τBTL Atom

Interprets a temporal model as a unary modal model.

Equations

• m.toModal = { toFrame := m.toFrame, v := m.v }

@[simp]

theorem Cslib.Logic.Modal.BTL.Model.toModal_toFrame {World : Type u_1} {Atom : Type u_2} (m : Model World Atom) : m.toModal.toFrame = m.toFrame

@[simp]

theorem Cslib.Logic.Modal.BTL.Model.toFrame_future_iff {World : Type u_1} {Atom : Sort u_2} (m : Model World Atom) (w w' : World) : m.toFrame.diagonal F w w' ↔ m.r w w'

@[simp]

theorem Cslib.Logic.Modal.BTL.Model.toFrame_past_iff {World : Type u_1} {Atom : Sort u_2} (m : Model World Atom) (w w' : World) : m.toFrame.diagonal P w w' ↔ m.r w' w

def Cslib.Logic.Modal.BTL.«termBTL[_,_⊨_]» : Lean.ParserDescr

Shortcut for Modal[BTL.Model.toModal m,w ⊨ φ].

Equations

• One or more equations did not get rendered due to their size.

instance Cslib.Logic.Modal.BTL.instDiagonalInverseToModalFP {World : Type u_1} {Atom : Type u_2} (m : Model World Atom) : m.toModal.DiagonalInverse F P

The future and past modalities in a BTL model have inverse diagonal relations.

theorem Cslib.Logic.Modal.Satisfies.btl_atom_iff {World : Type u_2} {Atom : Type u_1} {m : BTL.Model World Atom} {w : World} {a : Atom} : ⇓{ m := m.toModal, w := w, φ := Proposition.atom a } ↔ m.v w a

theorem Cslib.Logic.Modal.Satisfies.btl_future_sometime_iff {World : Type u_2} {Atom : Type u_1} {m : BTL.Model World Atom} {w : World} {φ : BTL.Proposition Atom} : ⇓{ m := m.toModal, w := w, φ := HasDynamicDiamond.dynDiamond BTL.F φ } ↔ ∃ (w' : World), m.r w w' ∧ ⇓{ m := m.toModal, w := w', φ := φ }

theorem Cslib.Logic.Modal.Satisfies.btl_past_sometime_iff {World : Type u_2} {Atom : Type u_1} {m : BTL.Model World Atom} {w : World} {φ : BTL.Proposition Atom} : ⇓{ m := m.toModal, w := w, φ := HasDynamicDiamond.dynDiamond BTL.P φ } ↔ ∃ (w' : World), m.r w' w ∧ ⇓{ m := m.toModal, w := w', φ := φ }

theorem Cslib.Logic.Modal.Satisfies.btl_future_always_iff {World : Type u_2} {Atom : Type u_1} {m : BTL.Model World Atom} {w : World} {φ : BTL.Proposition Atom} : ⇓{ m := m.toModal, w := w, φ := HasDynamicBox.dynBox BTL.F φ } ↔ ∀ (w' : World), m.r w w' → ⇓{ m := m.toModal, w := w', φ := φ }

theorem Cslib.Logic.Modal.Satisfies.btl_past_always_iff {World : Type u_2} {Atom : Type u_1} {m : BTL.Model World Atom} {w : World} {φ : BTL.Proposition Atom} : ⇓{ m := m.toModal, w := w, φ := HasDynamicBox.dynBox BTL.P φ } ↔ ∀ (w' : World), m.r w' w → ⇓{ m := m.toModal, w := w', φ := φ }

theorem Cslib.Logic.Modal.Satisfies.btl_future_sometime_intro {World : Type u_1} {Atom : Type u_2} {m : BTL.Model World Atom} {w w' : World} {φ : BTL.Proposition Atom} (hr : m.r w w') (h : ⇓{ m := m.toModal, w := w', φ := φ }) : ⇓{ m := m.toModal, w := w, φ := HasDynamicDiamond.dynDiamond BTL.F φ }

theorem Cslib.Logic.Modal.Satisfies.btl_past_sometime_intro {World : Type u_1} {Atom : Type u_2} {m : BTL.Model World Atom} {w w' : World} {φ : BTL.Proposition Atom} (hr : m.r w' w) (h : ⇓{ m := m.toModal, w := w', φ := φ }) : ⇓{ m := m.toModal, w := w, φ := HasDynamicDiamond.dynDiamond BTL.P φ }

theorem Cslib.Logic.Modal.Satisfies.btl_future_always_elim {World : Type u_2} {Atom : Type u_1} {m : BTL.Model World Atom} {w w' : World} {φ : BTL.Proposition Atom} (h : ⇓{ m := m.toModal, w := w, φ := HasDynamicBox.dynBox BTL.F φ }) (hr : m.r w w') : ⇓{ m := m.toModal, w := w', φ := φ }

theorem Cslib.Logic.Modal.Satisfies.btl_past_always_elim {World : Type u_2} {Atom : Type u_1} {m : BTL.Model World Atom} {w w' : World} {φ : BTL.Proposition Atom} (h : ⇓{ m := m.toModal, w := w, φ := HasDynamicBox.dynBox BTL.P φ }) (hr : m.r w' w) : ⇓{ m := m.toModal, w := w', φ := φ }

theorem Cslib.Logic.Modal.Satisfies.btl_future_past {World : Type u_2} {Atom : Type u_1} {m : BTL.Model World Atom} {w : World} {φ : BTL.Proposition Atom} : ⇓{ m := m.toModal, w := w, φ := HasImp.imp φ (HasDynamicBox.dynBox BTL.F (HasDynamicDiamond.dynDiamond BTL.P φ)) }

If a proposition holds now, then it is always going to be the case that it was true.

theorem Cslib.Logic.Modal.Satisfies.btl_past_future {World : Type u_2} {Atom : Type u_1} {m : BTL.Model World Atom} {w : World} {φ : BTL.Proposition Atom} : ⇓{ m := m.toModal, w := w, φ := HasImp.imp φ (HasDynamicBox.dynBox BTL.P (HasDynamicDiamond.dynDiamond BTL.F φ)) }

If a proposition holds now, then it has always been the case that it will be true.