T × W tense-modal logic: the TW calculus and soundness

The Hilbert calculus TW of [vK97] and its soundness for T × W frames ([Tho84]): every axiom is valid and every rule preserves validity. The distinctive rule is Gabbay's irreflexivity rule Provable.ir, whose soundness rests on a coincidence lemma — a formula's truth depends only on the valuation of the atoms it mentions.

Main definitions

• OForm.imp, OForm.or — derived connectives.
• OForm.mentions — the atoms occurring in a formula.
• Valid — truth at every point of every T × W model.
• Provable — the TW Hilbert calculus.

Main results

• TWFrame.sat_iff_of_agree — the coincidence lemma.
• soundness — Provable a → Valid a.

Derived connectives

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

Material implication a ⊃ b := ¬(a ∧ ¬b).

Equations

• a.imp b = (a.and b.neg).neg

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

Disjunction a ∨ b := ¬(¬a ∧ ¬b).

Equations

• a.or b = (a.neg.and b.neg).neg

def Core.Logic.Temporal.OForm.mentions {Atom : Type u_1} : OForm Atom → Atom → Prop

The sentential constants occurring in a formula.

Equations

• (Core.Logic.Temporal.OForm.atom p).mentions x✝ = (p = x✝)
• a.neg.mentions x✝ = a.mentions x✝
• (a.and b).mentions x✝ = (a.mentions x✝ ∨ b.mentions x✝)
• a.G.mentions x✝ = a.mentions x✝
• a.H.mentions x✝ = a.mentions x✝
• a.N.mentions x✝ = a.mentions x✝
• a.box.mentions x✝ = a.mentions x✝

@[simp]

theorem Core.Logic.Temporal.TWFrame.sat_imp {Atom : Type u_1} {Time : Type u_2} {World : 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.imp b) t w ↔ F.sat V a t w → F.sat V b t w

@[simp]

theorem Core.Logic.Temporal.TWFrame.sat_or {Atom : Type u_1} {Time : Type u_2} {World : 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.or b) t w ↔ F.sat V a t w ∨ F.sat V b t w

Coincidence lemma

A formula's truth at a point depends only on the valuation of the atoms it mentions.

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

Validity

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

A formula is valid when it is true at every point of every T × W model.

Equations

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

The TW calculus

inductive Core.Logic.Temporal.Provable {Atom : Type u_1} : OForm Atom → Prop

The Hilbert calculus TW ([vK97]): propositional axioms, the tense axioms A1–A3, the modal axioms A4–A5, the interaction axioms A6–A8, modus ponens, necessitation for H/N/□, and Gabbay's irreflexivity rule.

• impK {Atom : Type u_1} (a b : OForm Atom) : Provable (a.imp (b.imp a))

  Propositional K combinator.

• impS {Atom : Type u_1} (a b c : OForm Atom) : Provable ((a.imp (b.imp c)).imp ((a.imp b).imp (a.imp c)))

  Propositional S combinator.

• contra {Atom : Type u_1} (a b : OForm Atom) : Provable ((a.neg.imp b.neg).imp (b.imp a))

  Classical contraposition.

• andI {Atom : Type u_1} (a b : OForm Atom) : Provable (a.imp (b.imp (a.and b)))

  Conjunction introduction.

• andL {Atom : Type u_1} (a b : OForm Atom) : Provable ((a.and b).imp a)

  Conjunction elimination (left).

• andR {Atom : Type u_1} (a b : OForm Atom) : Provable ((a.and b).imp b)

  Conjunction elimination (right).

• a1a {Atom : Type u_1} (a b : OForm Atom) : Provable (((a.imp b).G.and a.G).imp b.G)

  A1a — K axiom for G.

• a1b {Atom : Type u_1} (a b : OForm Atom) : Provable (((a.imp b).H.and a.H).imp b.H)

  A1b — K axiom for H.

• a1c {Atom : Type u_1} (a : OForm Atom) : Provable (a.imp a.Fut.H)

  A1c — Prior conversion A ⊃ HFA.

• a1d {Atom : Type u_1} (a : OForm Atom) : Provable (a.imp a.Pst.G)

  A1d — Prior conversion A ⊃ GPA.

• a2 {Atom : Type u_1} (a : OForm Atom) : Provable (a.G.imp a.G.G)

  A2 — 4 axiom for G (transitivity).

• a3a {Atom : Type u_1} (a : OForm Atom) : Provable (a.Fut.imp (a.Fut.or (a.or a.Pst)).G)

  A3a — future linearity (.3).

• a3b {Atom : Type u_1} (a : OForm Atom) : Provable (a.Pst.imp (a.Fut.or (a.or a.Pst)).H)

  A3b — past linearity (.3).

• a4a {Atom : Type u_1} (a : OForm Atom) : Provable (a.N.imp a)

  A4a — T axiom for N.

• a4b {Atom : Type u_1} (a b : OForm Atom) : Provable (((a.imp b).N.and a.N).imp b.N)

  A4b — K axiom for N.

• a4c {Atom : Type u_1} (a : OForm Atom) : Provable (a.M.imp a.M.N)

  A4c — 5 axiom for N.

• a5a {Atom : Type u_1} (a b : OForm Atom) : Provable (((a.imp b).box.and a.box).imp b.box)

  A5a — K axiom for □.

• a5b {Atom : Type u_1} (a : OForm Atom) : Provable (a.dia.imp a.dia.box)

  A5b — 5 axiom for □.

• a6 {Atom : Type u_1} (a : OForm Atom) : Provable (a.N.Pst.imp a.Pst.N)

  A6 — past/necessity interaction PNA ⊃ NPA.

• a7 {Atom : Type u_1} (a : OForm Atom) : Provable (a.box.imp a.N)

  A7 — □ dominates N (□A ⊃ NA).

• a8a {Atom : Type u_1} (a : OForm Atom) : Provable (a.box.Pst.imp a.Pst.box)

  A8a — past/□ interaction P□A ⊃ □PA.

• a8b {Atom : Type u_1} (a : OForm Atom) : Provable (a.box.Fut.imp a.Fut.box)

  A8b — future/□ interaction F□A ⊃ □FA.

• mp {Atom : Type u_1} {a b : OForm Atom} : Provable (a.imp b) → Provable a → Provable b

  Modus ponens.

• necH {Atom : Type u_1} {a : OForm Atom} : Provable a → Provable a.H

  Necessitation for H.

• necN {Atom : Type u_1} {a : OForm Atom} : Provable a → Provable a.N

  Necessitation for N.

• necBox {Atom : Type u_1} {a : OForm Atom} : Provable a → Provable a.box

  Necessitation for □.

• ir {Atom : Type u_1} {a : OForm Atom} (q : Atom) : Provable (((OForm.atom q).neg.and (OForm.atom q).G).box.imp a) → ¬a.mentions q → Provable a

  Gabbay's irreflexivity rule: from □(¬q ∧ Gq) ⊃ A with q not in A, infer A.

Soundness

theorem Core.Logic.Temporal.soundness {Atom : Type u_1} {a : OForm Atom} (h : Provable a) : Valid a

Soundness of TW ([vK97]): every TW-provable formula is T × W-valid.