Modal Logic

Modal logic is a logic for reasoning about relational structures, studying statements about necessity (□φ) and possibility ◇φ.

References

• [P. Blackburn, M. de Rijke, Y. Venema, Modal Logic][Blackburn2001]
• The definitions of theory equivalence and the denotational semantics of worlds are inspired by the development of Cslib.Logic.HML.

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

A model consists of a relation between worlds r and a valuation v.

• r : World → World → Prop

  World accessibility relation.

• v : World → Atom → Prop

  Valuation of atoms at a world.

inductive Cslib.Logic.Modal.Proposition (Atom : Type u) : Type u

Propositions.

• atom {Atom : Type u} (p : Atom) : Proposition Atom

  Atomic proposition.

• not {Atom : Type u} (φ : Proposition Atom) : Proposition Atom

  Negation.

• and {Atom : Type u} (φ₁ φ₂ : Proposition Atom) : Proposition Atom

  Conjunction.

• diamond {Atom : Type u} (φ : Proposition Atom) : Proposition Atom

  Possibility.

@[instance_reducible]

instance Cslib.Logic.Modal.instHasNotProposition {Atom : Type u_1} : HasNot (Proposition Atom)

Equations

• Cslib.Logic.Modal.instHasNotProposition = { not := Cslib.Logic.Modal.Proposition.not }

@[instance_reducible]

instance Cslib.Logic.Modal.instHasAndProposition {Atom : Type u_1} : HasAnd (Proposition Atom)

Equations

• Cslib.Logic.Modal.instHasAndProposition = { and := Cslib.Logic.Modal.Proposition.and }

@[instance_reducible]

instance Cslib.Logic.Modal.instHasDiamondProposition {Atom : Type u_1} : HasDiamond (Proposition Atom)

Equations

• Cslib.Logic.Modal.instHasDiamondProposition = { diamond := Cslib.Logic.Modal.Proposition.diamond }

theorem Cslib.Logic.Modal.Proposition.not_def {Atom : Type u_1} (φ : Proposition Atom) : φ.not = HasNot.not φ

theorem Cslib.Logic.Modal.Proposition.and_def {Atom : Type u_1} (φ₁ φ₂ : Proposition Atom) : φ₁.and φ₂ = HasAnd.and φ₁ φ₂

theorem Cslib.Logic.Modal.Proposition.diamond_def {Atom : Type u_1} (φ : Proposition Atom) : φ.diamond = HasDiamond.diamond φ

def Cslib.Logic.Modal.Proposition.or {Atom : Type u_1} (φ₁ φ₂ : Proposition Atom) : Proposition Atom

Disjunction.

Equations

• φ₁.or φ₂ = Cslib.Logic.HasNot.not (Cslib.Logic.HasAnd.and (Cslib.Logic.HasNot.not φ₁) (Cslib.Logic.HasNot.not φ₂))

@[instance_reducible]

instance Cslib.Logic.Modal.instHasOrProposition {Atom : Type u_1} : HasOr (Proposition Atom)

Equations

• Cslib.Logic.Modal.instHasOrProposition = { or := Cslib.Logic.Modal.Proposition.or }

theorem Cslib.Logic.Modal.Proposition.or_def {Atom : Type u_1} (φ₁ φ₂ : Proposition Atom) : φ₁.or φ₂ = HasOr.or φ₁ φ₂

def Cslib.Logic.Modal.Proposition.imp {Atom : Type u_1} (φ₁ φ₂ : Proposition Atom) : Proposition Atom

Implication.

Equations

• φ₁.imp φ₂ = Cslib.Logic.HasOr.or (Cslib.Logic.HasNot.not φ₁) φ₂

@[instance_reducible]

instance Cslib.Logic.Modal.instHasImpProposition {Atom : Type u_1} : HasImp (Proposition Atom)

Equations

• Cslib.Logic.Modal.instHasImpProposition = { imp := Cslib.Logic.Modal.Proposition.imp }

theorem Cslib.Logic.Modal.Proposition.imp_def {Atom : Type u_1} (φ₁ φ₂ : Proposition Atom) : φ₁.imp φ₂ = HasImp.imp φ₁ φ₂

def Cslib.Logic.Modal.Proposition.iff {Atom : Type u_1} (φ₁ φ₂ : Proposition Atom) : Proposition Atom

Bi-implication.

Equations

• φ₁.iff φ₂ = Cslib.Logic.HasAnd.and (Cslib.Logic.HasImp.imp φ₁ φ₂) (Cslib.Logic.HasImp.imp φ₂ φ₁)

@[instance_reducible]

instance Cslib.Logic.Modal.instHasIffProposition {Atom : Type u_1} : HasIff (Proposition Atom)

Equations

• Cslib.Logic.Modal.instHasIffProposition = { iff := Cslib.Logic.Modal.Proposition.iff }

theorem Cslib.Logic.Modal.Proposition.iff_def {Atom : Type u_1} (φ₁ φ₂ : Proposition Atom) : φ₁.iff φ₂ = HasIff.iff φ₁ φ₂

def Cslib.Logic.Modal.Proposition.box {Atom : Type u_1} (φ : Proposition Atom) : Proposition Atom

Necessity.

Equations

• φ.box = Cslib.Logic.HasNot.not (Cslib.Logic.HasDiamond.diamond (Cslib.Logic.HasNot.not φ))

@[instance_reducible]

instance Cslib.Logic.Modal.instHasBoxProposition {Atom : Type u_1} : HasBox (Proposition Atom)

Equations

• Cslib.Logic.Modal.instHasBoxProposition = { box := Cslib.Logic.Modal.Proposition.box }

theorem Cslib.Logic.Modal.Proposition.box_def {Atom : Type u_1} (φ : Proposition Atom) : φ.box = HasBox.box φ

def Cslib.Logic.Modal.Satisfies {World : Type u_1} {Atom : Type u_2} (m : Model World Atom) (w : World) : Proposition Atom → Prop

Satisfaction relation. Satisfies m w φ means that, in the model m, the world w satisfies the proposition φ.

Equations

• Cslib.Logic.Modal.Satisfies m w (Cslib.Logic.Modal.Proposition.atom p) = m.v w p
• Cslib.Logic.Modal.Satisfies m w φ.not = ¬Cslib.Logic.Modal.Satisfies m w φ
• Cslib.Logic.Modal.Satisfies m w (φ₁.and φ₂) = (Cslib.Logic.Modal.Satisfies m w φ₁ ∧ Cslib.Logic.Modal.Satisfies m w φ₂)
• Cslib.Logic.Modal.Satisfies m w φ.diamond = ∃ (w' : World), m.r w w' ∧ Cslib.Logic.Modal.Satisfies m w' φ

structure Cslib.Logic.Modal.Judgement (World : Type u_1) (Atom : Type u_2) : Type (max u_1 u_2)

Judgement, representing the conclusions one reaches in modal logic.

• m : Model World Atom

  Model.

• w : World

  The world satisfying the proposition φ.

• φ : Proposition Atom

  The proposition satisfied by the world w.

def Cslib.Logic.Modal.«termModal[_,_⊨_]» : Lean.ParserDescr

Constructs a judgement.

Equations

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

def Cslib.Logic.Modal.Satisfies.Bundled {World : Type u_1} {Atom : Type u_2} (j : Judgement World Atom) : Prop

Satisfaction for judgements. This just refers to the unbundled Satisfies.

Equations

• Cslib.Logic.Modal.Satisfies.Bundled j = Cslib.Logic.Modal.Satisfies j.m j.w j.φ

@[instance_reducible]

instance Cslib.Logic.Modal.instHasInferenceSystemJudgement {World : Type u_1} {Atom : Type u_2} : HasInferenceSystem (Judgement World Atom)

Equations

• Cslib.Logic.Modal.instHasInferenceSystemJudgement = { derivation := Cslib.Logic.Modal.Satisfies.Bundled }

theorem Cslib.Logic.Modal.derivation_def {World : Type u_1} {Atom : Type u_2} {m : Model World Atom} {w : World} {φ : Proposition Atom} : Satisfies m w φ = ⇓{ m := m, w := w, φ := φ }

theorem Cslib.Logic.Modal.Satisfies.not_iff_not {World✝ : Type u_1} {Atom✝ : Type u_2} {m : Model World✝ Atom✝} {w : World✝} {φ : Proposition Atom✝} : ⇓{ m := m, w := w, φ := HasNot.not φ } ↔ ¬⇓{ m := m, w := w, φ := φ }

A world satisfies a proposition iff it does not satisfy the negation of the proposition.

theorem Cslib.Logic.Modal.Satisfies.and_iff_and {World : Type u_1} {Atom : Type u_2} {w : World} {φ₁ φ₂ : Proposition Atom} {m : Model World Atom} : ⇓{ m := m, w := w, φ := HasAnd.and φ₁ φ₂ } ↔ ⇓{ m := m, w := w, φ := φ₁ } ∧ ⇓{ m := m, w := w, φ := φ₂ }

theorem Cslib.Logic.Modal.Satisfies.diamond_iff_exists {World : Type u_1} {Atom : Type u_2} {w : World} {φ : Proposition Atom} {m : Model World Atom} : ⇓{ m := m, w := w, φ := HasDiamond.diamond φ } ↔ ∃ (w' : World), m.r w w' ∧ ⇓{ m := m, w := w', φ := φ }

theorem Cslib.Logic.Modal.Satisfies.or_iff_or {World : Type u_1} {Atom : Type u_2} {w : World} {φ₁ φ₂ : Proposition Atom} {m : Model World Atom} : ⇓{ m := m, w := w, φ := HasOr.or φ₁ φ₂ } ↔ ⇓{ m := m, w := w, φ := φ₁ } ∨ ⇓{ m := m, w := w, φ := φ₂ }

Characterisation of the ∨ connective.

Disjunction is defined in terms of the more primitive connectives given in Proposition. This result proves that the definition is correct.

theorem Cslib.Logic.Modal.Satisfies.imp_iff_imp {World : Type u_1} {Atom : Type u_2} {w : World} {φ₁ φ₂ : Proposition Atom} {m : Model World Atom} : ⇓{ m := m, w := w, φ := HasImp.imp φ₁ φ₂ } ↔ ⇓{ m := m, w := w, φ := φ₁ } → ⇓{ m := m, w := w, φ := φ₂ }

Characterisation of the → connective.

Implication is defined in terms of the more primitive connectives given in Proposition. This result proves that the definition is correct.

theorem Cslib.Logic.Modal.Satisfies.iff_iff_iff {World : Type u_1} {Atom : Type u_2} {w : World} {φ₁ φ₂ : Proposition Atom} {m : Model World Atom} : ⇓{ m := m, w := w, φ := HasIff.iff φ₁ φ₂ } ↔ (⇓{ m := m, w := w, φ := φ₁ } ↔ ⇓{ m := m, w := w, φ := φ₂ })

Characterisation of the ↔ connective.

Bi-implication is defined in terms of the more primitive connectives given in Proposition. This result proves that the definition is correct.

theorem Cslib.Logic.Modal.Satisfies.box_iff_forall {World : Type u_1} {Atom : Type u_2} {w : World} {φ : Proposition Atom} {m : Model World Atom} : ⇓{ m := m, w := w, φ := HasBox.box φ } ↔ ∀ (w' : World), m.r w w' → ⇓{ m := m, w := w', φ := φ }

Characterisation of the □ modality.

Necessity is defined in terms of the more primitive connectives given in Proposition. This result proves that the definition is correct.

@[reducible, inline]

abbrev Cslib.Logic.Modal.theory {World : Type u_1} {Atom : Type u_2} (m : Model World Atom) (w : World) : Set (Proposition Atom)

The theory of a world in a model is the set of all propositions that it satisfies.

Equations

• Cslib.Logic.Modal.theory m w = {φ : Cslib.Logic.Modal.Proposition Atom | ⇓{ m := m, w := w, φ := φ }}

@[reducible, inline]

abbrev Cslib.Logic.Modal.TheoryEq {World : Type u_1} {Atom : Type u_2} (m : Model World Atom) (w₁ w₂ : World) : Prop

Two worlds are theory-equivalent under a model if they have the same theory.

Equations

• Cslib.Logic.Modal.TheoryEq m w₁ w₂ = (Cslib.Logic.Modal.theory m w₁ = Cslib.Logic.Modal.theory m w₂)

theorem Cslib.Logic.Modal.TheoryEq.ext_iff {World✝ : Type u_1} {Atom✝ : Type u_2} {m : Model World✝ Atom✝} {w₁ w₂ : World✝} : TheoryEq m w₁ w₂ ↔ ∀ (φ : Proposition Atom✝), φ ∈ theory m w₁ ↔ φ ∈ theory m w₂

theorem Cslib.Logic.Modal.satisfies_theory {World✝ : Type u_1} {Atom✝ : Type u_2} {m : Model World✝ Atom✝} {w : World✝} {φ : Proposition Atom✝} (h : Satisfies m w φ) : φ ∈ theory m w

Any proposition satisfied by a world is in the theory of that world.

theorem Cslib.Logic.Modal.not_theoryEq_satisfies {World✝ : Type u_1} {Atom✝ : Type u_2} {m : Model World✝ Atom✝} {w₁ w₂ : World✝} (h : ¬TheoryEq m w₁ w₂) : ∃ (φ : Proposition Atom✝), ⇓{ m := m, w := w₁, φ := φ } ∧ ¬⇓{ m := m, w := w₂, φ := φ }

If two worlds are not theory equivalent, there exists a distinguishing proposition.

theorem Cslib.Logic.Modal.theoryEq_satisfies {World : Type u_1} {Atom : Type u_2} {w₁ w₂ : World} {φ : Proposition Atom} {m : Model World Atom} (h : TheoryEq m w₁ w₂) (hs : Satisfies m w₁ φ) : ⇓{ m := m, w := w₂, φ := φ }

If two worlds are theory equivalent and the former satisfies a proposition, the latter does as well.

theorem Cslib.Logic.Modal.Satisfies.k {World✝ : Type u_1} {Atom✝ : Type u_2} {m : Model World✝ Atom✝} {w : World✝} {φ₁ φ₂ : Proposition Atom✝} : ⇓{ m := m, w := w, φ := HasImp.imp (HasBox.box (HasImp.imp φ₁ φ₂)) (HasImp.imp (HasBox.box φ₁) (HasBox.box φ₂)) }

The K axiom, valid for all models.

theorem Cslib.Logic.Modal.Satisfies.dual {World✝ : Type u_1} {Atom✝ : Type u_2} {m : Model World✝ Atom✝} {w : World✝} {φ : Proposition Atom✝} : ⇓{ m := m, w := w, φ := HasIff.iff (HasDiamond.diamond φ) (HasNot.not (HasBox.box (HasNot.not φ))) }

The dual axiom, valid for all models.

theorem Cslib.Logic.Modal.Satisfies.t {World : Type u_1} {Atom : Type u_2} {m : Model World Atom} [instRefl : Std.Refl m.r] {w : World} (φ : Proposition Atom) : ⇓{ m := m, w := w, φ := HasImp.imp φ (HasDiamond.diamond φ) }

The T axiom, valid for all reflexive models.

theorem Cslib.Logic.Modal.Satisfies.t_refl {World : Type u_1} {Atom : Type u_2} {r : World → World → Prop} [Nonempty Atom] (h : ∀ {v : World → Atom → Prop} {w : World} {φ : Proposition Atom}, ⇓{ m := { r := r, v := v }, w := w, φ := HasImp.imp φ (HasDiamond.diamond φ) }) : Std.Refl r

Any model that admits the axiom T is reflexive.

theorem Cslib.Logic.Modal.Satisfies.t_box_diamond {World✝ : Type u_1} {Atom✝ : Type u_2} {m : Model World✝ Atom✝} {w : World✝} {φ : Proposition Atom✝} [Std.Refl m.r] : ⇓{ 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.b {World : Type u_1} {Atom : Type u_2} {m : Model World Atom} [Std.Symm m.r] {w : World} (φ : Proposition Atom) : ⇓{ m := m, w := w, φ := HasImp.imp φ (HasBox.box (HasDiamond.diamond φ)) }

The B axiom, valid for all symmetric models.

theorem Cslib.Logic.Modal.Satisfies.b_symm {World : Type u_1} {Atom : Type u_2} {r : World → World → Prop} [Nonempty Atom] (h : ∀ {v : World → Atom → Prop} {w : World} {φ : Proposition Atom}, ⇓{ m := { r := r, v := v }, w := w, φ := HasImp.imp φ (HasBox.box (HasDiamond.diamond φ)) }) : Std.Symm r

Any model that admits the axiom B is symmetric.

theorem Cslib.Logic.Modal.Satisfies.four {World : Type u_1} {Atom : Type u_2} {m : Model World Atom} [IsTrans World m.r] {w : World} (φ : Proposition Atom) : ⇓{ m := m, w := w, φ := HasImp.imp (HasDiamond.diamond (HasDiamond.diamond φ)) (HasDiamond.diamond φ) }

The 4 axiom, valid for all transitive models.

theorem Cslib.Logic.Modal.Satisfies.four_trans {World : Type u_1} {Atom : Type u_2} {r : World → World → Prop} [Nonempty Atom] (h : ∀ {v : World → Atom → Prop} {w : World} {φ : Proposition Atom}, ⇓{ m := { r := r, v := v }, w := w, φ := HasImp.imp (HasDiamond.diamond (HasDiamond.diamond φ)) (HasDiamond.diamond φ) }) : IsTrans World r

Any model that admits 4 is transitive.

theorem Cslib.Logic.Modal.Satisfies.five {World : Type u_1} {Atom : Type u_2} {m : Model World Atom} [Relation.RightEuclidean m.r] {w : World} (φ : Proposition Atom) : ⇓{ m := m, w := w, φ := HasImp.imp (HasDiamond.diamond φ) (HasBox.box (HasDiamond.diamond φ)) }

The 5 axiom, valid for all Euclidean models.

theorem Cslib.Logic.Modal.Satisfies.five_rightEuclidean {World : Type u_1} {Atom : Type u_2} {r : World → World → Prop} [Nonempty Atom] (h : ∀ {v : World → Atom → Prop} {w : World} {φ : Proposition Atom}, ⇓{ m := { r := r, v := v }, w := w, φ := HasImp.imp (HasDiamond.diamond φ) (HasBox.box (HasDiamond.diamond φ)) }) : Relation.RightEuclidean r

Any model that admits 5 is Euclidean.

theorem Cslib.Logic.Modal.Satisfies.d {World : Type u_1} {Atom : Type u_2} {m : Model World Atom} [Relation.Serial m.r] {w : World} (φ : Proposition Atom) : ⇓{ m := m, w := w, φ := HasImp.imp (HasBox.box φ) (HasDiamond.diamond φ) }

The D axiom, valid for all serial models.

theorem Cslib.Logic.Modal.Satisfies.d_serial {World : Type u_1} {Atom : Type u_2} {r : World → World → Prop} [Nonempty Atom] (h : ∀ {v : World → Atom → Prop} {w : World} {φ : Proposition Atom}, ⇓{ m := { r := r, v := v }, w := w, φ := HasImp.imp (HasBox.box φ) (HasDiamond.diamond φ) }) : Relation.Serial r

Any model that admits D is serial.

def Cslib.Logic.Modal.Proposition.valid {World : Type u_1} {Atom : Type u_2} (S : Set (Model World Atom)) (φ : Proposition Atom) : Prop

A proposition is valid in a class of models S (modelled as a set) if it is satisfied under all models in S for all worlds.

Equations

• Cslib.Logic.Modal.Proposition.valid S φ = ∀ m ∈ S, ∀ (w : World), ⇓{ m := m, w := w, φ := φ }

def Cslib.Logic.Modal.logic {World : Type u_1} {Atom : Type u_2} (S : Set (Model World Atom)) : Set (Proposition Atom)

The modal logic of a class of models S is the set of all propositions valid in S.

Equations

• Cslib.Logic.Modal.logic S = {φ : Cslib.Logic.Modal.Proposition Atom | Cslib.Logic.Modal.Proposition.valid S φ}