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
• 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.

• neg {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.

def Cslib.Logic.Modal.«term¬_» : Lean.ParserDescr

Negation.

Equations

• Cslib.Logic.Modal.«term¬_» = Lean.ParserDescr.node `Cslib.Logic.Modal.«term¬_» 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "¬") (Lean.ParserDescr.cat `term 40))

def Cslib.Logic.Modal.«term_∧_» : Lean.TrailingParserDescr

Conjunction.

Equations

• Cslib.Logic.Modal.«term_∧_» = Lean.ParserDescr.trailingNode `Cslib.Logic.Modal.«term_∧_» 36 37 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∧ ") (Lean.ParserDescr.cat `term 37))

def Cslib.Logic.Modal.«term◇_» : Lean.ParserDescr

Possibility.

Equations

• Cslib.Logic.Modal.«term◇_» = Lean.ParserDescr.node `Cslib.Logic.Modal.«term◇_» 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "◇") (Lean.ParserDescr.cat `term 40))

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

Disjunction.

Equations

• φ₁.or φ₂ = (φ₁.neg.and φ₂.neg).neg

def Cslib.Logic.Modal.«term_∨_» : Lean.TrailingParserDescr

Disjunction.

Equations

• Cslib.Logic.Modal.«term_∨_» = Lean.ParserDescr.trailingNode `Cslib.Logic.Modal.«term_∨_» 35 36 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∨ ") (Lean.ParserDescr.cat `term 36))

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

Implication.

Equations

• φ₁.impl φ₂ = φ₁.neg.or φ₂

def Cslib.Logic.Modal.«term_→_» : Lean.TrailingParserDescr

Implication.

Equations

• Cslib.Logic.Modal.«term_→_» = Lean.ParserDescr.trailingNode `Cslib.Logic.Modal.«term_→_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " → ") (Lean.ParserDescr.cat `term 31))

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

Bi-implication.

Equations

• φ₁.iff φ₂ = (φ₁.impl φ₂).and (φ₂.impl φ₁)

def Cslib.Logic.Modal.«term_↔_» : Lean.TrailingParserDescr

Bi-implication.

Equations

• Cslib.Logic.Modal.«term_↔_» = Lean.ParserDescr.trailingNode `Cslib.Logic.Modal.«term_↔_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↔ ") (Lean.ParserDescr.cat `term 31))

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

Necessity.

Equations

• φ.box = φ.neg.diamond.neg

def Cslib.Logic.Modal.«term□_» : Lean.ParserDescr

Necessity.

Equations

• Cslib.Logic.Modal.«term□_» = Lean.ParserDescr.node `Cslib.Logic.Modal.«term□_» 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "□") (Lean.ParserDescr.cat `term 40))

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 φ.neg = ¬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.φ

@[implicit_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} : InferenceSystem.derivation InferenceSystem.Default { m := m, w := w, φ := φ } = Satisfies m w φ

theorem Cslib.Logic.Modal.neg_satisfies {World✝ : Type u_1} {Atom✝ : Type u_2} {m : Model World✝ Atom✝} {w : World✝} {φ : Proposition Atom✝} : InferenceSystem.derivation InferenceSystem.Default { m := m, w := w, φ := φ.neg } ↔ ¬InferenceSystem.derivation InferenceSystem.Default { m := m, w := w, φ := φ }

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

theorem Cslib.Logic.Modal.Satisfies.or_iff_or {World : Type u_1} {Atom : Type u_2} {w : World} {φ₁ φ₂ : Proposition Atom} {m : Model World Atom} : InferenceSystem.derivation InferenceSystem.Default { m := m, w := w, φ := φ₁.or φ₂ } ↔ InferenceSystem.derivation InferenceSystem.Default { m := m, w := w, φ := φ₁ } ∨ InferenceSystem.derivation InferenceSystem.Default { 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.impl_iff_impl {World : Type u_1} {Atom : Type u_2} {w : World} {φ₁ φ₂ : Proposition Atom} {m : Model World Atom} : InferenceSystem.derivation InferenceSystem.Default { m := m, w := w, φ := φ₁.impl φ₂ } ↔ InferenceSystem.derivation InferenceSystem.Default { m := m, w := w, φ := φ₁ } → InferenceSystem.derivation InferenceSystem.Default { 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.box_iff_forall {World : Type u_1} {Atom : Type u_2} {w : World} {φ : Proposition Atom} {m : Model World Atom} : InferenceSystem.derivation InferenceSystem.Default { m := m, w := w, φ := φ.box } ↔ ∀ (w' : World), m.r w w' → InferenceSystem.derivation InferenceSystem.Default { 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 satifies.

Equations

• Cslib.Logic.Modal.theory m w = {φ : Cslib.Logic.Modal.Proposition Atom | Cslib.Logic.InferenceSystem.derivation Cslib.Logic.InferenceSystem.Default { 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✝), InferenceSystem.derivation InferenceSystem.Default { m := m, w := w₁, φ := φ } ∧ ¬InferenceSystem.derivation InferenceSystem.Default { 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₁ φ) : InferenceSystem.derivation InferenceSystem.Default { 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✝} : InferenceSystem.derivation InferenceSystem.Default { m := m, w := w, φ := (φ₁.impl φ₂).box.impl (φ₁.box.impl φ₂.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✝} : InferenceSystem.derivation InferenceSystem.Default { m := m, w := w, φ := φ.diamond.iff φ.neg.box.neg }

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) : InferenceSystem.derivation InferenceSystem.Default { m := m, w := w, φ := φ.impl φ.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}, InferenceSystem.derivation InferenceSystem.Default { m := { r := r, v := v }, w := w, φ := φ.impl φ.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] : InferenceSystem.derivation InferenceSystem.Default { m := m, w := w, φ := φ.box.impl φ } ↔ InferenceSystem.derivation InferenceSystem.Default { m := m, w := w, φ := φ.impl φ.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) : InferenceSystem.derivation InferenceSystem.Default { m := m, w := w, φ := φ.impl φ.diamond.box }

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}, InferenceSystem.derivation InferenceSystem.Default { m := { r := r, v := v }, w := w, φ := φ.impl φ.diamond.box }) : 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) : InferenceSystem.derivation InferenceSystem.Default { m := m, w := w, φ := φ.diamond.diamond.impl φ.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}, InferenceSystem.derivation InferenceSystem.Default { m := { r := r, v := v }, w := w, φ := φ.diamond.diamond.impl φ.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) : InferenceSystem.derivation InferenceSystem.Default { m := m, w := w, φ := φ.diamond.impl φ.diamond.box }

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}, InferenceSystem.derivation InferenceSystem.Default { m := { r := r, v := v }, w := w, φ := φ.diamond.impl φ.diamond.box }) : 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) : InferenceSystem.derivation InferenceSystem.Default { m := m, w := w, φ := φ.box.impl φ.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}, InferenceSystem.derivation InferenceSystem.Default { m := { r := r, v := v }, w := w, φ := φ.box.impl φ.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), Cslib.Logic.InferenceSystem.derivation Cslib.Logic.InferenceSystem.Default { 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 φ}