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][Blackburn2001]
@[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
Instances For
@[simp]
theorem
Cslib.Frame.ofRelation_rel
{τ : PFunctor.{u_2, u_3}}
[τ.Unary]
[Unique τ.A]
{World : Type u_1}
(r : World → World → Prop)
:
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)
:
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}
:
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}
:
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}
:
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 φ)))
:
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 φ))))
:
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)
:
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 φ)))
:
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)
:
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 φ))))
:
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 φ)))
:
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)
:
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)
:
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 φ))))
:
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
Instances For
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} }
Instances For
@[instance_reducible]
Equations
- Cslib.Logic.Modal.instUnaryτUnimodal = { unary := fun (x : (Cslib.Logic.Modal.τUnimodal α).A) => id inferInstance }
@[instance_reducible]
@[instance_reducible]
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)
:
@[reducible, inline]
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
Instances For
@[reducible, inline]
The language of modal propositions instantiated for τUnimodal Atom.