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

The object language and Kripke semantics of T × W logic ([Tho84], [vK97]): linear tense (G/H) with historical modality (N over historical alternatives ∼ₜ, box over all worlds) on worlds sharing one time order. A Core restatement of the Semantics.Modality.HistoricalAlternatives substrate, kept Semantics-free for the metatheory (soundness; [DMZ94] definability).

Main definitions

• TWFrame — a T × W frame (linear time + per-time, backward-closed historical equivalence).
• OForm — the object language L.
• TWFrame.sat — the satisfaction relation.
• OForm.M — historical possibility ¬N¬ (the Ockhamist ◇).

structure Core.Logic.Temporal.TWFrame (Time : Type u) (World : Type v) [LinearOrder Time] : Type (max u v)

A T × W frame ([Tho84], [vK97]): linear time, worlds, and a per-time historical-equivalence sim that is an equivalence and backward-closed.

• sim : Time → World → World → Prop

  Historical equivalence ∼ₜ: sim t w w' holds iff w, w' share their history up to t.

• sim_equiv (t : Time) : Equivalence (self.sim t)

  Each ∼ₜ is an equivalence relation.

• sim_backward {t t' : Time} (w w' : World) : t' ≤ t → self.sim t w w' → self.sim t' w w'

  Backward closure: agreement up to t implies agreement up to any earlier t'.

inductive Core.Logic.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₄).

def Core.Logic.Temporal.instDecidableEqOForm.decEq {Atom✝ : Type u_1} [DecidableEq Atom✝] (x✝ x✝¹ : OForm Atom✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Core.Logic.Temporal.instDecidableEqOForm.decEq (Core.Logic.Temporal.OForm.atom a) (Core.Logic.Temporal.OForm.atom b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq (Core.Logic.Temporal.OForm.atom a) a_1.neg = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq (Core.Logic.Temporal.OForm.atom a) (a_1.and a_2) = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq (Core.Logic.Temporal.OForm.atom a) a_1.G = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq (Core.Logic.Temporal.OForm.atom a) a_1.H = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq (Core.Logic.Temporal.OForm.atom a) a_1.N = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq (Core.Logic.Temporal.OForm.atom a) a_1.box = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.neg (Core.Logic.Temporal.OForm.atom a_1) = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.neg b.neg = if h : a = b then h ▸ have inst := Core.Logic.Temporal.instDecidableEqOForm.decEq a a; isTrue ⋯ else isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.neg (a_1.and a_2) = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.neg a_1.G = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.neg a_1.H = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.neg a_1.N = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.neg a_1.box = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq (a.and a_1) (Core.Logic.Temporal.OForm.atom a_2) = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq (a.and a_1) a_2.neg = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq (a.and a_1) a_2.G = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq (a.and a_1) a_2.H = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq (a.and a_1) a_2.N = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq (a.and a_1) a_2.box = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.G (Core.Logic.Temporal.OForm.atom a_1) = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.G a_1.neg = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.G (a_1.and a_2) = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.G b.G = if h : a = b then h ▸ have inst := Core.Logic.Temporal.instDecidableEqOForm.decEq a a; isTrue ⋯ else isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.G a_1.H = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.G a_1.N = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.G a_1.box = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.H (Core.Logic.Temporal.OForm.atom a_1) = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.H a_1.neg = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.H (a_1.and a_2) = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.H a_1.G = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.H b.H = if h : a = b then h ▸ have inst := Core.Logic.Temporal.instDecidableEqOForm.decEq a a; isTrue ⋯ else isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.H a_1.N = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.H a_1.box = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.N (Core.Logic.Temporal.OForm.atom a_1) = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.N a_1.neg = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.N (a_1.and a_2) = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.N a_1.G = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.N a_1.H = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.N b.N = if h : a = b then h ▸ have inst := Core.Logic.Temporal.instDecidableEqOForm.decEq a a; isTrue ⋯ else isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.N a_1.box = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.box (Core.Logic.Temporal.OForm.atom a_1) = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.box a_1.neg = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.box (a_1.and a_2) = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.box a_1.G = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.box a_1.H = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.box a_1.N = isFalse ⋯
• Core.Logic.Temporal.instDecidableEqOForm.decEq a.box b.box = if h : a = b then h ▸ have inst := Core.Logic.Temporal.instDecidableEqOForm.decEq a a; isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Logic.Temporal.instDecidableEqOForm {Atom✝ : Type u_1} [DecidableEq Atom✝] : DecidableEq (OForm Atom✝)

Equations

• Core.Logic.Temporal.instDecidableEqOForm = Core.Logic.Temporal.instDecidableEqOForm.decEq

def Core.Logic.Temporal.TWFrame.sat {Time : Type u} {World : Type v} {Atom : Type u_1} [LinearOrder Time] (F : TWFrame Time World) (V : Atom → Time → World → Prop) : OForm Atom → Time → World → Prop

Satisfaction V_{t,w}(A) ([vK97]) relative to an atomic valuation V. G/H/N/box are Core.Logic.Modal.box Kripke modalities 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

• F.sat V (Core.Logic.Temporal.OForm.atom p) x✝¹ x✝ = V p x✝¹ x✝
• F.sat V a.neg x✝¹ x✝ = ¬F.sat V a x✝¹ x✝
• F.sat V (a.and b) x✝¹ x✝ = (F.sat V a x✝¹ x✝ ∧ F.sat V b x✝¹ x✝)
• F.sat V a.G x✝¹ x✝ = Core.Logic.Modal.box (fun (x1 x2 : Time) => x1 < x2) (fun (t' : Time) => F.sat V a t' x✝) x✝¹
• F.sat V a.H x✝¹ x✝ = Core.Logic.Modal.box (fun (x1 x2 : Time) => x1 > x2) (fun (t' : Time) => F.sat V a t' x✝) x✝¹
• F.sat V a.N x✝¹ x✝ = Core.Logic.Modal.box (F.sim x✝¹) (fun (w' : World) => F.sat V a x✝¹ w') x✝
• F.sat V a.box x✝¹ x✝ = Core.Logic.Modal.box Core.Logic.Modal.universalR (fun (w' : World) => F.sat V a x✝¹ w') x✝

def Core.Logic.Temporal.TWFrame.entails {Time : Type u} {World : Type v} {Atom : Type u_1} [LinearOrder Time] (F : TWFrame Time World) (V : Atom → Time → World → Prop) (a b : OForm Atom) : Prop

Local entailment in a model: a entails b iff b holds wherever a does.

Equations

• F.entails V a b = ∀ (t : Time) (w : World), F.sat V a t w → F.sat V b t w

Derived (dual) operators

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

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

Equations

• a.M = a.neg.N.neg

def Core.Logic.Temporal.OForm.Fut {Atom : Type u_1} (a : OForm Atom) : OForm Atom

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

Equations

• a.Fut = a.neg.G.neg

def Core.Logic.Temporal.OForm.Pst {Atom : Type u_1} (a : OForm Atom) : OForm Atom

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

Equations

• a.Pst = a.neg.H.neg

def Core.Logic.Temporal.OForm.dia {Atom : Type u_1} (a : OForm Atom) : OForm Atom

Possibility in all worlds ◇ = ¬□¬.

Equations

• a.dia = a.neg.box.neg