Modal Logic Cube

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

References

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

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

The modal logic K.

Equations

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

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

The modal logic T.

Equations

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

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

The modal logic B.

Equations

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

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

The modal logic 4.

Equations

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

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

The modal logic 5.

Equations

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

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

The modal logic K45.

Equations

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

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

The modal logic D.

Equations

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

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

The modal logic D4.

Equations

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

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

The modal logic D5.

Equations

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

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

The modal logic D45.

Equations

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

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

The modal logic DB.

Equations

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

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

The modal logic TB.

Equations

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

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

The modal logic KB5.

Equations

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

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

The modal logic S4.

Equations

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

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

The modal logic S5.

Equations

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

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.Unimodal.k_subset_d {World : Type u_1} {Atom : Type u_2} : K World Atom ⊆ D World Atom

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

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

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

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

theorem Cslib.Logic.Modal.Unimodal.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.Unimodal.K.k_valid {World : Type u_1} {Atom : Type u_2} {φ₁ φ₂ : Proposition Atom} : HasImp.imp (HasBox.box (HasImp.imp φ₁ φ₂)) (HasImp.imp (HasBox.box φ₁) (HasBox.box φ₂)) ∈ K World Atom

The axiom K is valid in the logic K.

theorem Cslib.Logic.Modal.Unimodal.T.t_valid {World : Type u_1} {Atom : Type u_2} {φ : Proposition Atom} : HasImp.imp φ (HasDiamond.diamond φ) ∈ T World Atom

The axiom T is valid in the logic T.