Basic Modal Logic

Basic modal logic is the modal logic with a single unary modality.

References

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

@[instance_reducible]

def Cslib.Frame.rel {τ : PFunctor.{u_1, u_2}} [Unique τ.A] {World : Type u_3} (f : Frame World τ) : World → World → Prop

The accessibility relation of a unimodal frame.

Equations

• f.rel = f.diagonal default

theorem Cslib.Frame.rel_iff_diagonal {τ : PFunctor.{u_2, u_3}} [Unique τ.A] {World : Type u_1} (f : Frame World τ) (w w' : World) : f.rel w w' ↔ f.diagonal default w w'

@[instance_reducible]

def Cslib.Frame.ofRelation {τ : PFunctor.{u_1, u_2}} [τ.Unary] {World : Type u_3} (r : World → World → Prop) : Frame World τ

Builds a unimodal frame out of a binary relation.

Equations

• Cslib.Frame.ofRelation r = { r := fun (x : τ.A) (w : World) (ws : τ.B x → World) => r w (ws default) }

@[simp]

theorem Cslib.Frame.ofRelation_rel {τ : PFunctor.{u_2, u_3}} [τ.Unary] [Unique τ.A] {World : Type u_1} (r : World → World → Prop) : (ofRelation r).rel = r

instance Cslib.Frame.instReflRelOfRelation {τ : PFunctor.{u_2, u_3}} [τ.Unary] [Unique τ.A] {World : Type u_1} {r : World → World → Prop} [Std.Refl r] : Std.Refl (ofRelation r).rel

instance Cslib.Frame.instSymmRelOfRelation {τ : PFunctor.{u_2, u_3}} [τ.Unary] [Unique τ.A] {World : Type u_1} {r : World → World → Prop} [Std.Symm r] : Std.Symm (ofRelation r).rel

instance Cslib.Frame.instIsTransRelOfRelation {τ : PFunctor.{u_2, u_3}} [τ.Unary] [Unique τ.A] {World : Type u_1} {r : World → World → Prop} [IsTrans World r] : IsTrans World (ofRelation r).rel

theorem Cslib.Frame.ofRelation_rel_iff {τ : PFunctor.{u_2, u_3}} [τ.Unary] [Unique τ.A] {World : Type u_1} (r : World → World → Prop) (w w' : World) : (ofRelation r).rel w w' ↔ r w w'

theorem Cslib.Frame.ofRelation_rel_of {τ : PFunctor.{u_2, u_3}} [τ.Unary] [Unique τ.A] {World : Type u_1} {r : World → World → Prop} {w w' : World} (h : r w w') : (ofRelation r).rel w w'

theorem Cslib.Frame.preservesMap_const_iff_preserves {τ : PFunctor.{u_2, u_3}} [τ.Unary] [Unique τ.A] {α : Type u_1} {r : α → α → Prop} {P : α → Prop} : ((ofRelation r).PreservesMap default P fun (x : τ.B default) => P) ↔ Relation.Preserves r P

theorem Cslib.Logic.Modal.Satisfies.diamond_iff_exists {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} {w : World} {m : Model World τ Atom} {φ : Proposition τ Atom} : ⇓{ m := m, w := w, φ := HasDiamond.diamond φ } ↔ ∃ (w' : World), m.rel w w' ∧ ⇓{ m := m, w := w', φ := φ }

theorem Cslib.Logic.Modal.Satisfies.diamond_of {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} {w w' : World} {m : Model World τ Atom} {φ : Proposition τ Atom} (hr : m.rel w w') (hφ : ⇓{ m := m, w := w', φ := φ }) : ⇓{ m := m, w := w, φ := HasDiamond.diamond φ }

theorem Cslib.Logic.Modal.Satisfies.box_iff_forall {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} {w : World} {m : Model World τ Atom} {φ : Proposition τ Atom} : ⇓{ m := m, w := w, φ := HasBox.box φ } ↔ ∀ (w' : World), m.rel w w' → ⇓{ m := m, w := w', φ := φ }

theorem Cslib.Logic.Modal.Satisfies.unimodal_k {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} (f : Frame World τ) (φ₁ φ₂ : Proposition τ Atom) : InferenceSystem.derivation (Axiom f) (HasImp.imp (HasBox.box (HasImp.imp φ₁ φ₂)) (HasImp.imp (HasBox.box φ₁) (HasBox.box φ₂)))

Axiom K for unimodal logic.

theorem Cslib.Logic.Modal.Satisfies.unimodal_dual {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} (f : Frame World τ) (φ : Proposition τ Atom) : InferenceSystem.derivation (Axiom f) (HasIff.iff (HasDiamond.diamond φ) (HasNot.not (HasBox.box (HasNot.not φ))))

The dual axiom for unimodal logic.

theorem Cslib.Logic.Modal.Satisfies.diamond_and {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} (f : Frame World τ) (φ₁ φ₂ : Proposition τ Atom) : InferenceSystem.derivation (Axiom f) (HasImp.imp (HasDiamond.diamond (HasAnd.and φ₁ φ₂)) (HasAnd.and (HasDiamond.diamond φ₁) (HasDiamond.diamond φ₂)))

theorem Cslib.Logic.Modal.Satisfies.diamond_and_box {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} (f : Frame World τ) (φ₁ φ₂ : Proposition τ Atom) : InferenceSystem.derivation (Axiom f) (HasImp.imp (HasAnd.and (HasDiamond.diamond φ₁) (HasBox.box φ₂)) (HasDiamond.diamond (HasAnd.and φ₁ φ₂)))

theorem Cslib.Logic.Modal.Satisfies.diamond_of_box {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} (f : Frame World τ) (φ₁ φ₂ : Proposition τ Atom) : InferenceSystem.derivation (Axiom f) (HasImp.imp (HasAnd.and (HasBox.box φ₁) (HasDiamond.diamond φ₂)) (HasDiamond.diamond φ₁))

theorem Cslib.Logic.Modal.Satisfies.unimodal_t {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} (f : Frame World τ) [instRefl : Std.Refl f.rel] (φ : Proposition τ Atom) : InferenceSystem.derivation (Axiom f) (HasImp.imp φ (HasDiamond.diamond φ))

Axiom T.

theorem Cslib.Logic.Modal.Satisfies.unimodal_t_refl {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} (f : Frame World τ) [Nonempty Atom] (h : ∀ (φ : Proposition τ Atom), InferenceSystem.derivation (Axiom f) (HasImp.imp φ (HasDiamond.diamond φ))) : Std.Refl f.rel

Any frame that admits T is reflexive.

theorem Cslib.Logic.Modal.Satisfies.t_box_diamond {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} {w : World} {φ : Proposition τ Atom} {m : Model World τ Atom} [Std.Refl m.rel] : ⇓{ m := m, w := w, φ := HasImp.imp (HasBox.box φ) φ } ↔ ⇓{ m := m, w := w, φ := HasImp.imp φ (HasDiamond.diamond φ) }

In any reflexive model, □φ → φ is equivalent to φ → ◇φ.

theorem Cslib.Logic.Modal.Satisfies.unimodal_b {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} (f : Frame World τ) [Std.Symm f.rel] (φ : Proposition τ Atom) : InferenceSystem.derivation (Axiom f) (HasImp.imp φ (HasBox.box (HasDiamond.diamond φ)))

Axiom B.

theorem Cslib.Logic.Modal.Satisfies.unimodal_b_symm {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} (f : Frame World τ) [Nonempty Atom] (h : ∀ (φ : Proposition τ Atom), InferenceSystem.derivation (Axiom f) (HasImp.imp φ (HasBox.box (HasDiamond.diamond φ)))) : Std.Symm f.rel

Any frame that admits B is symmetric.

theorem Cslib.Logic.Modal.Satisfies.unimodal_four {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} (f : Frame World τ) [IsTrans World f.rel] (φ : Proposition τ Atom) : InferenceSystem.derivation (Axiom f) (HasImp.imp (HasDiamond.diamond (HasDiamond.diamond φ)) (HasDiamond.diamond φ))

Axiom 4, valid for all transitive frames.

theorem Cslib.Logic.Modal.Satisfies.unimodal_four_trans {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} (f : Frame World τ) [Nonempty Atom] (h : ∀ (φ : Proposition τ Atom), InferenceSystem.derivation (Axiom f) (HasImp.imp (HasDiamond.diamond (HasDiamond.diamond φ)) (HasDiamond.diamond φ))) : IsTrans World f.rel

Any frame that admits 4 is transitive.

theorem Cslib.Logic.Modal.Satisfies.unimodal_five {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} (f : Frame World τ) [Relation.RightEuclidean f.rel] (φ : Proposition τ Atom) : InferenceSystem.derivation (Axiom f) (HasImp.imp (HasDiamond.diamond φ) (HasBox.box (HasDiamond.diamond φ)))

Axiom 5.

theorem Cslib.Logic.Modal.Satisfies.unimodal_five_rightEuclidean {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} (f : Frame World τ) [Nonempty Atom] (h : ∀ (φ : Proposition τ Atom), InferenceSystem.derivation (Axiom f) (HasImp.imp (HasDiamond.diamond φ) (HasBox.box (HasDiamond.diamond φ)))) : Relation.RightEuclidean f.rel

Any frame that admits 5 is right Euclidean.

theorem Cslib.Logic.Modal.Satisfies.d {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} (f : Frame World τ) [Relation.Serial f.rel] (φ : Proposition τ Atom) : InferenceSystem.derivation (Axiom f) (HasImp.imp (HasBox.box φ) (HasDiamond.diamond φ))

Axiom D, valid for all serial frames.

theorem Cslib.Logic.Modal.Satisfies.d_serial {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} (f : Frame World τ) [Nonempty Atom] (h : ∀ (φ : Proposition τ Atom), InferenceSystem.derivation (Axiom f) (HasImp.imp (HasBox.box φ) (HasDiamond.diamond φ))) : Relation.Serial f.rel

Any model that admits D is serial.

theorem Cslib.Logic.Modal.Satisfies.l {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} (f : Frame World τ) [IsTrans World f.rel] (hwf : Relation.Terminating f.rel) (φ : Proposition τ Atom) : InferenceSystem.derivation (Axiom f) (HasImp.imp (HasBox.box (HasImp.imp (HasBox.box φ) φ)) (HasBox.box φ))

The L axiom, or Löb's theorem, valid for all transitive and converse well-founded models.

theorem Cslib.Logic.Modal.Satisfies.l_induction {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} {φ : Proposition τ Atom} (m : Model World τ Atom) [IsTrans World m.rel] (hwf : Relation.Terminating m.rel) (hstep : ∀ (w : World), ⇓{ m := m, w := w, φ := HasImp.imp (HasBox.box φ) φ }) (w : World) : ⇓{ m := m, w := w, φ := φ }

Löb induction, via the L axiom.

theorem Cslib.Logic.Modal.Satisfies.pointTwo {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} (f : Frame World τ) (h : Relation.Diamond f.rel) (φ : Proposition τ Atom) : InferenceSystem.derivation (Axiom f) (HasImp.imp (HasDiamond.diamond (HasBox.box φ)) (HasBox.box (HasDiamond.diamond φ)))

Axiom .2, valid for all frames with the diamond property.

theorem Cslib.Logic.Modal.Satisfies.pointTwo_diamond {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} (f : Frame World τ) [Nonempty Atom] (h : ∀ (φ : Proposition τ Atom), InferenceSystem.derivation (Axiom f) (HasImp.imp (HasDiamond.diamond (HasBox.box φ)) (HasBox.box (HasDiamond.diamond φ)))) : Relation.Diamond f.rel

Any model that admits axiom .2 has the diamond property.

theorem Cslib.Logic.Modal.Proposition.diamond_and_equiv_of_preserves {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} {m : Model World τ Atom} [IsTrans World m.rel] {φ₁ φ₂ : Proposition τ Atom} (hd : Relation.Diamond m.rel) (h₁ : Relation.Preserves m.rel fun (x : World) => ⇓{ m := m, w := x, φ := φ₁ }) (h₂ : Relation.Preserves m.rel fun (x : World) => ⇓{ m := m, w := x, φ := φ₂ }) : Congruence.r (Equiv m) (HasDiamond.diamond (HasAnd.and φ₁ φ₂)) (HasAnd.and (HasDiamond.diamond φ₁) (HasDiamond.diamond φ₂))

In a transitive diamond model, possibility distributes over conjunction for propositions whose satisfaction is preserved along accessibility.

theorem Cslib.Logic.Modal.Proposition.diamond_diamond_equiv {τ : PFunctor.{u_3, u_4}} [τ.Unary] [Unique τ.A] {World : Type u_1} {Atom : Type u_2} {m : Model World τ Atom} [Std.Refl m.rel] [IsTrans World m.rel] (φ : Proposition τ Atom) : Congruence.r (Equiv m) (HasDiamond.diamond (HasDiamond.diamond φ)) (HasDiamond.diamond φ)

In a reflexive and transitive model, diamond absorbs itself (idempotency).

@[match_pattern]

def Cslib.Logic.Modal.Proposition.Context.diamond {τ : PFunctor.{u_1, u_2}} [τ.Unary] [Unique τ.A] {Atom : Type u_3} (c : Context τ Atom) : Context τ Atom

Context constructor for the diamond modality.

Equations

• c.diamond = c.dynDiamond default

def Cslib.Logic.Modal.τUnimodal : Type u → PFunctor.{u, u}

Constructs a signature for basic modal logic at the same universe level of the input type.

Equations

• Cslib.Logic.Modal.τUnimodal x✝ = { A := PUnit.{?u.1 + 1}, B := fun (x : PUnit.{?u.1 + 1}) => PUnit.{?u.1 + 1} }

@[instance_reducible]

instance Cslib.Logic.Modal.instUnaryτUnimodal {α : Type u_1} : (τUnimodal α).Unary

Equations

• Cslib.Logic.Modal.instUnaryτUnimodal = { unary := fun (x : (Cslib.Logic.Modal.τUnimodal α).A) => id inferInstance }

@[instance_reducible]

instance Cslib.Logic.Modal.instUniqueAτUnimodal {α : Type u_1} : Unique (τUnimodal α).A

Equations

• Cslib.Logic.Modal.instUniqueAτUnimodal = id inferInstance

@[instance_reducible]

instance Cslib.Logic.Modal.instDecidableEqChildrenτUnimodal {α : Type u_1} : (τUnimodal α).DecidableEqChildren

Equations

• Cslib.Logic.Modal.instDecidableEqChildrenτUnimodal = { decidableEq := inferInstance }

@[simp]

theorem Cslib.Frame.ofRelation_unimodal_rel_iff {World : Type u_1} (r : World → World → Prop) (w w' : World) : (ofRelation r).rel w w' ↔ r w w'

@[reducible, inline]

abbrev Cslib.Logic.Modal.Unimodal.Model (World : Type u_1) (Atom : Type u_2) : Type (max u_1 u_2)

A basic model, constructed on τUnimodal.

Equations

• Cslib.Logic.Modal.Unimodal.Model World Atom = Cslib.Logic.Modal.Model World (Cslib.Logic.Modal.τUnimodal Atom) Atom

@[reducible, inline]

abbrev Cslib.Logic.Modal.Unimodal.Proposition (Atom : Type u_1) : Type u_1

The language of modal propositions instantiated for τUnimodal Atom.

Equations

• Cslib.Logic.Modal.Unimodal.Proposition Atom = Cslib.Logic.Modal.Proposition (Cslib.Logic.Modal.τUnimodal Atom) Atom