Modal Logic Cube

This module formalises the Modal Cube, including all the 15 foundational modal logics and their relationships.

References

• P. Blackburn, M. de Rijke, Y. Venema, Modal Logic

def Cslib.Logic.Modal.K (World : Type u_1) (Atom : Type u_2) : Set (Proposition Atom)

The modal logic K.

Equations

• Cslib.Logic.Modal.K World Atom = Cslib.Logic.Modal.logic Set.univ

def Cslib.Logic.Modal.T (World : Type u_1) (Atom : Type u_2) : Set (Proposition Atom)

The modal logic T.

Equations

• Cslib.Logic.Modal.T World Atom = Cslib.Logic.Modal.logic {m : Cslib.Logic.Modal.Model World Atom | Std.Refl m.r}

def Cslib.Logic.Modal.B (World : Type u_1) (Atom : Type u_2) : Set (Proposition Atom)

The modal logic B.

Equations

• Cslib.Logic.Modal.B World Atom = Cslib.Logic.Modal.logic {m : Cslib.Logic.Modal.Model World Atom | Std.Symm m.r}

def Cslib.Logic.Modal.Four (World : Type u_1) (Atom : Type u_2) : Set (Proposition Atom)

The modal logic 4.

Equations

• Cslib.Logic.Modal.Four World Atom = Cslib.Logic.Modal.logic {m : Cslib.Logic.Modal.Model World Atom | IsTrans World m.r}

def Cslib.Logic.Modal.Five (World : Type u_1) (Atom : Type u_2) : Set (Proposition Atom)

The modal logic 5.

Equations

• Cslib.Logic.Modal.Five World Atom = Cslib.Logic.Modal.logic {m : Cslib.Logic.Modal.Model World Atom | Relation.RightEuclidean m.r}

def Cslib.Logic.Modal.K45 (World : Type u_1) (Atom : Type u_2) : Set (Proposition Atom)

The modal logic K45.

Equations

• Cslib.Logic.Modal.K45 World Atom = Cslib.Logic.Modal.logic {m : Cslib.Logic.Modal.Model World Atom | IsTrans World m.r ∧ Relation.RightEuclidean m.r}

def Cslib.Logic.Modal.D (World : Type u_1) (Atom : Type u_2) : Set (Proposition Atom)

The modal logic D.

Equations

• Cslib.Logic.Modal.D World Atom = Cslib.Logic.Modal.logic {m : Cslib.Logic.Modal.Model World Atom | Relation.Serial m.r}

def Cslib.Logic.Modal.D4 (World : Type u_1) (Atom : Type u_2) : Set (Proposition Atom)

The modal logic D4.

Equations

• Cslib.Logic.Modal.D4 World Atom = Cslib.Logic.Modal.logic {m : Cslib.Logic.Modal.Model World Atom | Relation.Serial m.r ∧ IsTrans World m.r}

def Cslib.Logic.Modal.D5 (World : Type u_1) (Atom : Type u_2) : Set (Proposition Atom)

The modal logic D5.

Equations

• Cslib.Logic.Modal.D5 World Atom = Cslib.Logic.Modal.logic {m : Cslib.Logic.Modal.Model World Atom | Relation.Serial m.r ∧ Relation.RightEuclidean m.r}

def Cslib.Logic.Modal.D45 (World : Type u_1) (Atom : Type u_2) : Set (Proposition Atom)

The modal logic D45.

Equations

• Cslib.Logic.Modal.D45 World Atom = Cslib.Logic.Modal.logic {m : Cslib.Logic.Modal.Model World Atom | Relation.Serial m.r ∧ IsTrans World m.r ∧ Relation.RightEuclidean m.r}

def Cslib.Logic.Modal.DB (World : Type u_1) (Atom : Type u_2) : Set (Proposition Atom)

The modal logic DB.

Equations

• Cslib.Logic.Modal.DB World Atom = Cslib.Logic.Modal.logic {m : Cslib.Logic.Modal.Model World Atom | Relation.Serial m.r ∧ Std.Symm m.r}

def Cslib.Logic.Modal.TB (World : Type u_1) (Atom : Type u_2) : Set (Proposition Atom)

The modal logic TB.

Equations

• Cslib.Logic.Modal.TB World Atom = Cslib.Logic.Modal.logic {m : Cslib.Logic.Modal.Model World Atom | Std.Refl m.r ∧ Std.Symm m.r}

def Cslib.Logic.Modal.KB5 (World : Type u_1) (Atom : Type u_2) : Set (Proposition Atom)

The modal logic KB5.

Equations

• Cslib.Logic.Modal.KB5 World Atom = Cslib.Logic.Modal.logic {m : Cslib.Logic.Modal.Model World Atom | Std.Symm m.r ∧ Relation.RightEuclidean m.r}

def Cslib.Logic.Modal.S4 (World : Type u_1) (Atom : Type u_2) : Set (Proposition Atom)

The modal logic S4.

Equations

• Cslib.Logic.Modal.S4 World Atom = Cslib.Logic.Modal.logic {m : Cslib.Logic.Modal.Model World Atom | Std.Refl m.r ∧ IsTrans World m.r}

def Cslib.Logic.Modal.S5 (World : Type u_1) (Atom : Type u_2) : Set (Proposition Atom)

The modal logic S5.

Equations

• Cslib.Logic.Modal.S5 World Atom = Cslib.Logic.Modal.logic {m : Cslib.Logic.Modal.Model World Atom | Std.Refl m.r ∧ IsTrans World m.r ∧ Relation.RightEuclidean m.r}

Ordering of Modal Logics

This section proves the essential inclusions of modal logics. Inclusions among compound logics follow by forgetting frame conditions in their defining model classes.

theorem Cslib.Logic.Modal.k_subset_d {World : Type u_1} {Atom : Type u_2} : K World Atom ⊆ D World Atom

theorem Cslib.Logic.Modal.k_subset_b {World : Type u_1} {Atom : Type u_2} : K World Atom ⊆ B World Atom

theorem Cslib.Logic.Modal.k_subset_four {World : Type u_1} {Atom : Type u_2} : K World Atom ⊆ Four World Atom

theorem Cslib.Logic.Modal.k_subset_five {World : Type u_1} {Atom : Type u_2} : K World Atom ⊆ Five World Atom

theorem Cslib.Logic.Modal.d_subset_t {World : Type u_1} {Atom : Type u_2} : D World Atom ⊆ T World Atom

theorem Cslib.Logic.Modal.k_subset_t {World : Type u_1} {Atom : Type u_2} : K World Atom ⊆ T World Atom

Validity

This section showcases how to prove the expected validities in the different modal logics.

theorem Cslib.Logic.Modal.K.k_valid {World : Type u_1} {Atom : Type u_2} {φ₁ φ₂ : Proposition Atom} : (φ₁.impl φ₂).box.impl (φ₁.box.impl φ₂.box) ∈ K World Atom

The axiom K is valid in the logic K.

theorem Cslib.Logic.Modal.T.t_valid {World : Type u_1} {Atom : Type u_2} {φ : Proposition Atom} : φ.impl φ.diamond ∈ T World Atom

The axiom T is valid in the logic T.