Documentation

Linglib.Logic.Temporal.Basic

The satisfaction clauses of T × W logic, its dual operators, and the hierarchy box ⊃ N ⊃ A. Historical necessity N is necessity along historical equivalence and box necessity along the universal relation, so both are S5 by modal correspondence: historical equivalence is a setoid, whose relation is reflexive, symmetric and transitive.

Main results #

sat_neg, sat_and, sat_G, sat_H, sat_N, sat_box: the satisfaction clauses.
sat_M: historical possibility is ∃ over historical alternatives.
sat_box_imp_N, sat_N_imp_self, sat_box_imp_self: the hierarchy box ⊃ N ⊃ A.
sat_N_imp_N_N, sat_M_imp_N_M, sat_box_imp_box_box, sat_dia_imp_box_dia: N and box are S5.
Fut_adjoint_H, Pst_adjoint_G: the tense adjunctions.

References #

Historical equivalence as accessibility #

instance Temporal.TWFrame.instIsReflAlt {T : Type u_1} {World : Type u_2} [Preorder T] (F : TWFrame World T) (t : T) :

(F.alt t).IsRefl

instance Temporal.TWFrame.instIsSymmAlt {T : Type u_1} {World : Type u_2} [Preorder T] (F : TWFrame World T) (t : T) :

(F.alt t).IsSymm

instance Temporal.TWFrame.instIsTransAlt {T : Type u_1} {World : Type u_2} [Preorder T] (F : TWFrame World T) (t : T) :

(F.alt t).IsTrans

Satisfaction clauses #

@[simp]

theorem Temporal.TWFrame.sat_atom {T : Type u_1} {World : Type u_2} {Atom : Type u_3} [Preorder T] (F : TWFrame World T) (V : Atom → T → World → Prop) (p : Atom) (t : T) (w : World) :

F.sat V (OForm.atom p) t w ↔ V p t w

@[simp]

theorem Temporal.TWFrame.sat_neg {T : Type u_1} {World : Type u_2} {Atom : Type u_3} [Preorder T] (F : TWFrame World T) (V : Atom → T → World → Prop) (a : OForm Atom) (t : T) (w : World) :

F.sat V a.neg t w ↔ ¬F.sat V a t w

@[simp]

theorem Temporal.TWFrame.sat_and {T : Type u_1} {World : Type u_2} {Atom : Type u_3} [Preorder T] (F : TWFrame World T) (V : Atom → T → World → Prop) (a b : OForm Atom) (t : T) (w : World) :

F.sat V (a.and b) t w ↔ F.sat V a t w ∧ F.sat V b t w

@[simp]

theorem Temporal.TWFrame.sat_G {T : Type u_1} {World : Type u_2} {Atom : Type u_3} [Preorder T] (F : TWFrame World T) (V : Atom → T → World → Prop) (a : OForm Atom) (t : T) (w : World) :

F.sat V a.G t w ↔ ∀ (t' : T), t < t' → F.sat V a t' w

@[simp]

theorem Temporal.TWFrame.sat_H {T : Type u_1} {World : Type u_2} {Atom : Type u_3} [Preorder T] (F : TWFrame World T) (V : Atom → T → World → Prop) (a : OForm Atom) (t : T) (w : World) :

F.sat V a.H t w ↔ ∀ t' < t, F.sat V a t' w

@[simp]

theorem Temporal.TWFrame.sat_N {T : Type u_1} {World : Type u_2} {Atom : Type u_3} [Preorder T] (F : TWFrame World T) (V : Atom → T → World → Prop) (a : OForm Atom) (t : T) (w : World) :

F.sat V a.N t w ↔ ∀ (w' : World), (F.sim t) w w' → F.sat V a t w'

@[simp]

theorem Temporal.TWFrame.sat_box {T : Type u_1} {World : Type u_2} {Atom : Type u_3} [Preorder T] (F : TWFrame World T) (V : Atom → T → World → Prop) (a : OForm Atom) (t : T) (w : World) :

F.sat V a.box t w ↔ ∀ (w' : World), F.sat V a t w'

Dual operators #

@[simp]

theorem Temporal.TWFrame.sat_M {T : Type u_1} {World : Type u_2} {Atom : Type u_3} [Preorder T] (F : TWFrame World T) (V : Atom → T → World → Prop) (a : OForm Atom) (t : T) (w : World) :

F.sat V a.M t w ↔ ∃ (w' : World), (F.sim t) w w' ∧ F.sat V a t w'

@[simp]

theorem Temporal.TWFrame.sat_dia {T : Type u_1} {World : Type u_2} {Atom : Type u_3} [Preorder T] (F : TWFrame World T) (V : Atom → T → World → Prop) (a : OForm Atom) (t : T) (w : World) :

F.sat V a.dia t w ↔ ∃ (w' : World), F.sat V a t w'

@[simp]

theorem Temporal.TWFrame.sat_Fut {T : Type u_1} {World : Type u_2} {Atom : Type u_3} [Preorder T] (F : TWFrame World T) (V : Atom → T → World → Prop) (a : OForm Atom) (t : T) (w : World) :

F.sat V a.Fut t w ↔ ∃ (t' : T), t < t' ∧ F.sat V a t' w

@[simp]

theorem Temporal.TWFrame.sat_Pst {T : Type u_1} {World : Type u_2} {Atom : Type u_3} [Preorder T] (F : TWFrame World T) (V : Atom → T → World → Prop) (a : OForm Atom) (t : T) (w : World) :

F.sat V a.Pst t w ↔ ∃ t' < t, F.sat V a t' w

The modality hierarchy `box ⊃ N ⊃ A` and S5, from modal correspondence #

N and box are necessities along relations, so the hierarchy and the S5 axioms come from modal correspondence: box ⊃ N from box_restrict, since the universal relation contains historical equivalence; the T axioms from reflexivity (box_T); the 4 axioms from transitivity (box_four); the 5 axioms from the symmetry and transitivity of historical equivalence.

theorem Temporal.TWFrame.sat_box_imp_N {T : Type u_1} {World : Type u_2} {Atom : Type u_3} [Preorder T] (F : TWFrame World T) (V : Atom → T → World → Prop) {a : OForm Atom} {t : T} {w : World} :

F.sat V a.box t w → F.sat V a.N t w

theorem Temporal.TWFrame.sat_N_imp_self {T : Type u_1} {World : Type u_2} {Atom : Type u_3} [Preorder T] (F : TWFrame World T) (V : Atom → T → World → Prop) {a : OForm Atom} {t : T} {w : World} :

F.sat V a.N t w → F.sat V a t w

theorem Temporal.TWFrame.sat_box_imp_self {T : Type u_1} {World : Type u_2} {Atom : Type u_3} [Preorder T] (F : TWFrame World T) (V : Atom → T → World → Prop) {a : OForm Atom} {t : T} {w : World} :

F.sat V a.box t w → F.sat V a t w

theorem Temporal.TWFrame.sat_N_imp_N_N {T : Type u_1} {World : Type u_2} {Atom : Type u_3} [Preorder T] (F : TWFrame World T) (V : Atom → T → World → Prop) {a : OForm Atom} {t : T} {w : World} :

F.sat V a.N t w → F.sat V a.N.N t w

theorem Temporal.TWFrame.sat_box_imp_box_box {T : Type u_1} {World : Type u_2} {Atom : Type u_3} [Preorder T] (F : TWFrame World T) (V : Atom → T → World → Prop) {a : OForm Atom} {t : T} {w : World} :

F.sat V a.box t w → F.sat V a.box.box t w

theorem Temporal.TWFrame.sat_M_imp_N_M {T : Type u_1} {World : Type u_2} {Atom : Type u_3} [Preorder T] (F : TWFrame World T) (V : Atom → T → World → Prop) {a : OForm Atom} {t : T} {w : World} :

F.sat V a.M t w → F.sat V a.M.N t w

theorem Temporal.TWFrame.sat_dia_imp_box_dia {T : Type u_1} {World : Type u_2} {Atom : Type u_3} [Preorder T] (F : TWFrame World T) (V : Atom → T → World → Prop) {a : OForm Atom} {t : T} {w : World} :

F.sat V a.dia t w → F.sat V a.dia.box t w

theorem Temporal.TWFrame.N_isIndicial {T : Type u_1} {World : Type u_2} [Preorder T] (F : TWFrame World T) (t : T) :

ModalLogic.IsIndicial (ModalLogic.Box (F.alt t))

Historical necessity N is an indicial modality in the sense of [Gal75], necessity along historical equivalence.

The temporal adjunctions `Fut ⊣ H`, `Pst ⊣ G` #

The tense operators are Galois-adjoint on each model's entailment preorder ([Bur84]): Fut (future ∃) is left adjoint to H (past ∀), and Pst (past ∃) to G (future ∀).

theorem Temporal.TWFrame.Fut_adjoint_H {T : Type u_1} {World : Type u_2} {Atom : Type u_3} [Preorder T] (F : TWFrame World T) (V : Atom → T → World → Prop) (a b : OForm Atom) :

F.entails V a.Fut b ↔ F.entails V a b.H

theorem Temporal.TWFrame.Pst_adjoint_G {T : Type u_1} {World : Type u_2} {Atom : Type u_3} [Preorder T] (F : TWFrame World T) (V : Atom → T → World → Prop) (a b : OForm Atom) :

F.entails V a.Pst b ↔ F.entails V a b.G