Modal operators and frame conditions

This file defines the relational box/diamond of Kripke semantics, the frame conditions of modal correspondence theory for accessibility relations W → W → Prop, and the per-axiom correspondences (K, T, D, B, 4, 5) connecting them; the Set-valued mathlib counterparts of the operators are Rel.core and Rel.preimage.

References

• [Kri63] — relational semantics
• [BdRV01] — Chapter 3, frame definability

Box and diamond

def ModalLogic.box {W : Type u_1} (R : W → W → Prop) (p : W → Prop) (w : W) : Prop

Restricted necessity: box R p w holds iff p v for all v accessible from w.

Equations

• ModalLogic.box R p w = ∀ (v : W), R w v → p v

def ModalLogic.diamond {W : Type u_1} (R : W → W → Prop) (p : W → Prop) (w : W) : Prop

Restricted possibility: diamond R p w holds iff p v for some v accessible from w. Dual of box.

Equations

• ModalLogic.diamond R p w = ∃ (v : W), R w v ∧ p v

def ModalLogic.«term□[_]» : Lean.ParserDescr

Restricted necessity: box R p w holds iff p v for all v accessible from w.

Equations

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

def ModalLogic.«term◇[_]» : Lean.ParserDescr

Restricted possibility: diamond R p w holds iff p v for some v accessible from w. Dual of box.

Equations

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

Duality

@[simp]

theorem ModalLogic.not_box {W : Type u_1} (R : W → W → Prop) (p : W → Prop) (w : W) : ¬box R p w ↔ diamond R (fun (v : W) => ¬p v) w

@[simp]

theorem ModalLogic.not_diamond {W : Type u_1} (R : W → W → Prop) (p : W → Prop) (w : W) : ¬diamond R p w ↔ box R (fun (v : W) => ¬p v) w

theorem ModalLogic.box_and {W : Type u_1} (R : W → W → Prop) (p q : W → Prop) (w : W) : box R (fun (v : W) => p v ∧ q v) w ↔ box R p w ∧ box R q w

Necessity distributes over conjunction ([Hin62]'s a believes A and B ↔ a believes A and a believes B).

Frame conditions

class ModalLogic.IsSerial {W : Type u_1} (R : W → W → Prop) : Prop

R is serial if every world accesses at least one world.

• serial : Relator.LeftTotal R

class ModalLogic.IsEuclidean {W : Type u_1} (R : W → W → Prop) : Prop

R is Euclidean if from any pair of R-successors of w, each is an R-successor of the other.

• eucl (w v u : W) : R w v → R w u → R v u

Frame implications and instances

instance ModalLogic.instReflTopForallForallProp_linglib {W : Type u_1} : Std.Refl ⊤

instance ModalLogic.instIsEuclideanTopForallForallProp {W : Type u_1} : IsEuclidean ⊤

instance ModalLogic.instIsSerialOfRefl {W : Type u_1} {R : W → W → Prop} [hR : Std.Refl R] : IsSerial R

Reflexive relations are serial.

instance ModalLogic.instSymmOfReflOfIsEuclidean {W : Type u_1} {R : W → W → Prop} [hR : Std.Refl R] [hE : IsEuclidean R] : Std.Symm R

Reflexive + Euclidean implies symmetric.

instance ModalLogic.instIsTransOfReflOfIsEuclidean {W : Type u_1} {R : W → W → Prop} [hR : Std.Refl R] [hE : IsEuclidean R] : IsTrans W R

Reflexive + Euclidean implies transitive.

instance ModalLogic.instIsEuclideanOfSymmOfIsTrans {W : Type u_1} {R : W → W → Prop} [hS : Std.Symm R] [hT : IsTrans W R] : IsEuclidean R

Symmetric + transitive implies euclidean.

Axiom correspondence

theorem ModalLogic.box_K {W : Type u_1} {R : W → W → Prop} {p q : W → Prop} {w : W} (hpq : box R (fun (v : W) => p v → q v) w) (hp : box R p w) : box R q w

K: □(p → q) → □p → □q, over any relation.

theorem ModalLogic.box_T {W : Type u_1} {R : W → W → Prop} {p : W → Prop} {w : W} [Std.Refl R] (h : box R p w) : p w

T: over a reflexive relation, □p → p.

theorem ModalLogic.box_D {W : Type u_1} {R : W → W → Prop} {p : W → Prop} {w : W} [hS : IsSerial R] (h : box R p w) : diamond R p w

D: over a serial relation, □p → ◇p.

theorem ModalLogic.box_B {W : Type u_1} {R : W → W → Prop} {p : W → Prop} {w : W} [Std.Symm R] (h : p w) : box R (diamond R p) w

B: over a symmetric relation, p → □◇p.

theorem ModalLogic.box_four {W : Type u_1} {R : W → W → Prop} {p : W → Prop} {w : W} [IsTrans W R] (h : box R p w) : box R (box R p) w

4: over a transitive relation, □p → □□p.

theorem ModalLogic.box_five {W : Type u_1} {R : W → W → Prop} {p : W → Prop} {w : W} [hE : IsEuclidean R] (h : diamond R p w) : box R (diamond R p) w

5: over a Euclidean relation, ◇p → □◇p.

Frame definability

Each axiom, read as an inequality between operators on W → Prop, characterizes its frame condition.

theorem ModalLogic.box_T_iff {W : Type u_1} {R : W → W → Prop} : box R ≤ id ↔ Std.Refl R

T defines reflexivity.

theorem ModalLogic.box_D_iff {W : Type u_1} {R : W → W → Prop} : box R ≤ diamond R ↔ IsSerial R

D defines seriality.

theorem ModalLogic.box_B_iff {W : Type u_1} {R : W → W → Prop} : id ≤ box R ∘ diamond R ↔ Std.Symm R

B defines symmetry.

theorem ModalLogic.box_four_iff {W : Type u_1} {R : W → W → Prop} : box R ≤ box R ∘ box R ↔ IsTrans W R

4 defines transitivity.

theorem ModalLogic.box_five_iff {W : Type u_1} {R : W → W → Prop} : diamond R ≤ box R ∘ diamond R ↔ IsEuclidean R

5 defines the Euclidean property.