T × W tense-modal logic: the modal algebra of satisfaction

[vK97] [Tho84]

Basic semantic lemmas for Core.Logic.Temporal satisfaction: the satisfaction-clause @[simp] lemmas, the dual operators (M/dia/Fut/Pst), the modality hierarchy box ⊃ N ⊃ A, and the fact that historical necessity N and the all-worlds box are S5 modalities. Since sat's G/H/N/box clauses are Core.Logic.Modal.box Kripke modalities, the hierarchy and S5 axioms are derived from modal correspondence theory (box_T/box_four/box_restrict) rather than re-proved — N is S5 because ∼ₜ is an equivalence, box because the universal relation is ([vK97] A4, A5).

Main results

• sat_neg/sat_and/sat_G/sat_H/sat_N/sat_box — satisfaction clauses (@[simp]).
• sat_M — historical possibility M is ∃ over ∼ₜ-alternatives.
• sat_box_imp_N, sat_N_imp_self, sat_box_imp_self — the box ⊃ N ⊃ A hierarchy.
• sat_N_imp_N_N, sat_M_imp_N_M — N is S5 (axioms 4 and 5).
• sat_box_imp_box_box, sat_dia_imp_box_dia — box is S5.
• N_isIndicial — N is a Kripke (indicial) modality ([Gal75]).

Satisfaction clauses

@[simp]

theorem Core.Logic.Temporal.TWFrame.sat_atom {Time : Type u_1} {World : Type u_2} {Atom : Type u_3} [LinearOrder Time] (F : TWFrame Time World) (V : Atom → Time → World → Prop) (p : Atom) (t : Time) (w : World) : F.sat V (OForm.atom p) t w ↔ V p t w

@[simp]

theorem Core.Logic.Temporal.TWFrame.sat_neg {Time : Type u_1} {World : Type u_2} {Atom : Type u_3} [LinearOrder Time] (F : TWFrame Time World) (V : Atom → Time → World → Prop) (a : OForm Atom) (t : Time) (w : World) : F.sat V a.neg t w ↔ ¬F.sat V a t w

@[simp]

theorem Core.Logic.Temporal.TWFrame.sat_and {Time : Type u_1} {World : Type u_2} {Atom : Type u_3} [LinearOrder Time] (F : TWFrame Time World) (V : Atom → Time → World → Prop) (a b : OForm Atom) (t : Time) (w : World) : F.sat V (a.and b) t w ↔ F.sat V a t w ∧ F.sat V b t w

@[simp]

theorem Core.Logic.Temporal.TWFrame.sat_G {Time : Type u_1} {World : Type u_2} {Atom : Type u_3} [LinearOrder Time] (F : TWFrame Time World) (V : Atom → Time → World → Prop) (a : OForm Atom) (t : Time) (w : World) : F.sat V a.G t w ↔ ∀ (t' : Time), t < t' → F.sat V a t' w

@[simp]

theorem Core.Logic.Temporal.TWFrame.sat_H {Time : Type u_1} {World : Type u_2} {Atom : Type u_3} [LinearOrder Time] (F : TWFrame Time World) (V : Atom → Time → World → Prop) (a : OForm Atom) (t : Time) (w : World) : F.sat V a.H t w ↔ ∀ t' < t, F.sat V a t' w

@[simp]

theorem Core.Logic.Temporal.TWFrame.sat_N {Time : Type u_1} {World : Type u_2} {Atom : Type u_3} [LinearOrder Time] (F : TWFrame Time World) (V : Atom → Time → World → Prop) (a : OForm Atom) (t : Time) (w : World) : F.sat V a.N t w ↔ ∀ (w' : World), F.sim t w w' → F.sat V a t w'

@[simp]

theorem Core.Logic.Temporal.TWFrame.sat_box {Time : Type u_1} {World : Type u_2} {Atom : Type u_3} [LinearOrder Time] (F : TWFrame Time World) (V : Atom → Time → World → Prop) (a : OForm Atom) (t : Time) (w : World) : F.sat V a.box t w ↔ ∀ (w' : World), F.sat V a t w'

Dual operators

@[simp]

theorem Core.Logic.Temporal.TWFrame.sat_M {Time : Type u_1} {World : Type u_2} {Atom : Type u_3} [LinearOrder Time] (F : TWFrame Time World) (V : Atom → Time → World → Prop) (a : OForm Atom) (t : Time) (w : World) : F.sat V a.M t w ↔ ∃ (w' : World), F.sim t w w' ∧ F.sat V a t w'

@[simp]

theorem Core.Logic.Temporal.TWFrame.sat_dia {Time : Type u_1} {World : Type u_2} {Atom : Type u_3} [LinearOrder Time] (F : TWFrame Time World) (V : Atom → Time → World → Prop) (a : OForm Atom) (t : Time) (w : World) : F.sat V a.dia t w ↔ ∃ (w' : World), F.sat V a t w'

@[simp]

theorem Core.Logic.Temporal.TWFrame.sat_Fut {Time : Type u_1} {World : Type u_2} {Atom : Type u_3} [LinearOrder Time] (F : TWFrame Time World) (V : Atom → Time → World → Prop) (a : OForm Atom) (t : Time) (w : World) : F.sat V a.Fut t w ↔ ∃ (t' : Time), t < t' ∧ F.sat V a t' w

@[simp]

theorem Core.Logic.Temporal.TWFrame.sat_Pst {Time : Type u_1} {World : Type u_2} {Atom : Type u_3} [LinearOrder Time] (F : TWFrame Time World) (V : Atom → Time → World → Prop) (a : OForm Atom) (t : Time) (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 Core.Logic.Modal.box modalities, so the hierarchy and S5 axioms come from modal correspondence theory: box ⊃ N from box_restrict (the universal relation contains ∼ₜ); the T axioms from reflexivity (box_T); the 4 axioms from transitivity (box_four); the 5 axioms from euclideanness of ∼ₜ.

theorem Core.Logic.Temporal.TWFrame.sat_box_imp_N {Time : Type u_1} {World : Type u_2} {Atom : Type u_3} [LinearOrder Time] (F : TWFrame Time World) (V : Atom → Time → World → Prop) {a : OForm Atom} {t : Time} {w : World} : F.sat V a.box t w → F.sat V a.N t w

theorem Core.Logic.Temporal.TWFrame.sat_N_imp_self {Time : Type u_1} {World : Type u_2} {Atom : Type u_3} [LinearOrder Time] (F : TWFrame Time World) (V : Atom → Time → World → Prop) {a : OForm Atom} {t : Time} {w : World} : F.sat V a.N t w → F.sat V a t w

theorem Core.Logic.Temporal.TWFrame.sat_box_imp_self {Time : Type u_1} {World : Type u_2} {Atom : Type u_3} [LinearOrder Time] (F : TWFrame Time World) (V : Atom → Time → World → Prop) {a : OForm Atom} {t : Time} {w : World} : F.sat V a.box t w → F.sat V a t w

theorem Core.Logic.Temporal.TWFrame.sat_N_imp_N_N {Time : Type u_1} {World : Type u_2} {Atom : Type u_3} [LinearOrder Time] (F : TWFrame Time World) (V : Atom → Time → World → Prop) {a : OForm Atom} {t : Time} {w : World} : F.sat V a.N t w → F.sat V a.N.N t w

theorem Core.Logic.Temporal.TWFrame.sat_box_imp_box_box {Time : Type u_1} {World : Type u_2} {Atom : Type u_3} [LinearOrder Time] (F : TWFrame Time World) (V : Atom → Time → World → Prop) {a : OForm Atom} {t : Time} {w : World} : F.sat V a.box t w → F.sat V a.box.box t w

theorem Core.Logic.Temporal.TWFrame.sat_M_imp_N_M {Time : Type u_1} {World : Type u_2} {Atom : Type u_3} [LinearOrder Time] (F : TWFrame Time World) (V : Atom → Time → World → Prop) {a : OForm Atom} {t : Time} {w : World} : F.sat V a.M t w → F.sat V a.M.N t w

theorem Core.Logic.Temporal.TWFrame.sat_dia_imp_box_dia {Time : Type u_1} {World : Type u_2} {Atom : Type u_3} [LinearOrder Time] (F : TWFrame Time World) (V : Atom → Time → World → Prop) {a : OForm Atom} {t : Time} {w : World} : F.sat V a.dia t w → F.sat V a.dia.box t w

theorem Core.Logic.Temporal.TWFrame.N_isIndicial {Time : Type u_1} {World : Type u_2} [LinearOrder Time] (F : TWFrame Time World) (t : Time) : Modal.IsIndicial (Modal.box (F.sim t))

Historical necessity N is a Kripke (indicial) modality — Core.Logic.Modal.box over ∼ₜ, [Gal75]'s indicial necessity. (G/H are tense over the time order, not world-PropOps, so they fall outside this world-indexed classification.)

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 Core.Logic.Temporal.TWFrame.Fut_adjoint_H {Time : Type u_1} {World : Type u_2} {Atom : Type u_3} [LinearOrder Time] (F : TWFrame Time World) (V : Atom → Time → World → Prop) (a b : OForm Atom) : F.entails V a.Fut b ↔ F.entails V a b.H

theorem Core.Logic.Temporal.TWFrame.Pst_adjoint_G {Time : Type u_1} {World : Type u_2} {Atom : Type u_3} [LinearOrder Time] (F : TWFrame Time World) (V : Atom → Time → World → Prop) (a b : OForm Atom) : F.entails V a.Pst b ↔ F.entails V a b.G