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.

• 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.instCoeProposition {Atom : Type u_1} : Coe Atom (Proposition Atom)

Utility to coerce atoms into atomic propositions.

Equations

• Cslib.Logic.Modal.instCoeProposition = { coe := Cslib.Logic.Modal.Proposition.atom }

@[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, φ := φ }

@[simp]

theorem Cslib.Logic.Modal.Satisfies.atom_iff {Atom : Type u_1} {World✝ : Type u_2} {m : Model World✝ Atom} {w : World✝} {a : Atom} : ⇓{ m := m, w := w, φ := Proposition.atom a } ↔ m.v w a

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 : ⇓{ m := m, w := 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.

inductive Cslib.Logic.Modal.Axiom {World : Sort u_1} (r : World → World → Prop) : Type

Every accessibility relation induces an inference system tag for proving valid axioms under the relation.

@[instance_reducible]

instance Cslib.Logic.Modal.instInferenceSystemAxiomProposition {World : Type u_1} {Atom : Type u_2} (r : World → World → Prop) : InferenceSystem (Axiom r) (Proposition Atom)

A proposition φ is an axiom under the relation r (the 'frame') if it holds for all valuations and worlds.

Equations

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

theorem Cslib.Logic.Modal.Satisfies.axiom_def {World : Type u_1} {Atom✝ : Type u_2} {φ : Proposition Atom✝} (r : World → World → Prop) : (∀ (v : World → Atom✝ → Prop) (w : World), ⇓{ m := { r := r, v := v }, w := w, φ := φ }) ↔ InferenceSystem.derivation (Axiom r) φ

theorem Cslib.Logic.Modal.Satisfies.der_of_axiom {Atom✝ : Type u_1} {φ : Proposition Atom✝} {World✝ : Type u_2} {m : Model World✝ Atom✝} {w : World✝} (h : InferenceSystem.derivation (Axiom m.r) φ) : ⇓{ m := m, w := w, φ := φ }

theorem Cslib.Logic.Modal.Satisfies.of_axiom {World : Type u_1} {Atom : Type u_2} (m : Model World Atom) (φ : Proposition Atom) (h : InferenceSystem.derivation (Axiom m.r) φ) (w : World) : ⇓{ m := m, w := w, φ := φ }

If a proposition is an axiom under the relation of a model, it is satisfied by every world.

theorem Cslib.Logic.Modal.Satisfies.k {World : Type u_1} {Atom : Type u_2} (r : World → World → Prop) (φ₁ φ₂ : Proposition Atom) : InferenceSystem.derivation (Axiom r) (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} (r : World → World → Prop) (φ : Proposition Atom) : InferenceSystem.derivation (Axiom r) (HasIff.iff (HasDiamond.diamond φ) (HasNot.not (HasBox.box (HasNot.not φ))))

The dual axiom, valid for all models.

theorem Cslib.Logic.Modal.Satisfies.diamond_and {World : Type u_1} {Atom : Type u_2} (r : World → World → Prop) (φ₁ φ₂ : Proposition Atom) : InferenceSystem.derivation (Axiom r) (HasImp.imp (HasDiamond.diamond (HasAnd.and φ₁ φ₂)) (HasAnd.and (HasDiamond.diamond φ₁) (HasDiamond.diamond φ₂)))

Possibility preserves conjunction in all models.

theorem Cslib.Logic.Modal.Satisfies.diamond_and_box {World : Type u_1} {Atom : Type u_2} (r : World → World → Prop) (φ₁ φ₂ : Proposition Atom) : InferenceSystem.derivation (Axiom r) (HasImp.imp (HasAnd.and (HasDiamond.diamond φ₁) (HasBox.box φ₂)) (HasDiamond.diamond (HasAnd.and φ₁ φ₂)))

Possibility can be combined with necessity.

theorem Cslib.Logic.Modal.Satisfies.diamond_of_box {Atom : Type u_1} {World✝ : Type u_2} {r : World✝ → World✝ → Prop} {φ₁ φ₂ : Proposition Atom} : InferenceSystem.derivation (Axiom r) (HasImp.imp (HasAnd.and (HasBox.box φ₁) (HasDiamond.diamond φ₂)) (HasDiamond.diamond φ₁))

If φ₁ is necessary and some successor exists, then some successor satisfies φ₁.

theorem Cslib.Logic.Modal.Satisfies.t {World : Type u_1} {Atom : Type u_2} (r : World → World → Prop) [instRefl : Std.Refl r] (φ : Proposition Atom) : InferenceSystem.derivation (Axiom r) (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 : ∀ (φ : Proposition Atom), InferenceSystem.derivation (Axiom r) (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} (r : World → World → Prop) [Std.Symm r] (φ : Proposition Atom) : InferenceSystem.derivation (Axiom r) (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 : ∀ (φ : Proposition Atom), InferenceSystem.derivation (Axiom r) (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} (r : World → World → Prop) [IsTrans World r] (φ : Proposition Atom) : InferenceSystem.derivation (Axiom r) (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 : ∀ (φ : Proposition Atom), InferenceSystem.derivation (Axiom r) (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} (r : World → World → Prop) [Relation.RightEuclidean r] (φ : Proposition Atom) : InferenceSystem.derivation (Axiom r) (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 : ∀ (φ : Proposition Atom), InferenceSystem.derivation (Axiom r) (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} (r : World → World → Prop) [Relation.Serial r] (φ : Proposition Atom) : InferenceSystem.derivation (Axiom r) (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 : ∀ (φ : Proposition Atom), InferenceSystem.derivation (Axiom r) (HasImp.imp (HasBox.box φ) (HasDiamond.diamond φ))) : Relation.Serial r

Any model that admits D is serial.

theorem Cslib.Logic.Modal.Satisfies.l {World : Type u_1} {Atom : Type u_2} (r : World → World → Prop) [IsTrans World r] (hwf : Relation.Terminating r) (φ : Proposition Atom) : InferenceSystem.derivation (Axiom r) (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 {World : Type u_1} {Atom : Type u_2} {φ : Proposition Atom} (m : Model World Atom) [IsTrans World m.r] (hwf : Relation.Terminating m.r) (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 {World : Type u_1} {Atom : Type u_2} (r : World → World → Prop) (h : Relation.Diamond r) (φ : Proposition Atom) : InferenceSystem.derivation (Axiom r) (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 {World : Type u_1} {Atom : Type u_2} (r : World → World → Prop) [Nonempty Atom] (h : ∀ (φ : Proposition Atom), InferenceSystem.derivation (Axiom r) (HasImp.imp (HasDiamond.diamond (HasBox.box φ)) (HasBox.box (HasDiamond.diamond φ)))) : Relation.Diamond r

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

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 φ}

theorem Cslib.Logic.Modal.logic_antitone {World : Type u_1} {Atom : Type u_2} : Antitone logic

Modal logic is antitone (wrt the class of models).

@[reducible, inline]

abbrev Cslib.Logic.Modal.modelsOfRelation {World : Type u_1} {Atom : Type u_2} (r : World → World → Prop) : Set (Model World Atom)

The class of all models generated by a frame (relation).

Equations

• Cslib.Logic.Modal.modelsOfRelation r = {m : Cslib.Logic.Modal.Model World Atom | m.r = r}

theorem Cslib.Logic.Modal.axiom_iff_mem_logic_modelsOfRelation {World : Type u_1} {Atom : Type u_2} (r : World → World → Prop) (φ : Proposition Atom) : InferenceSystem.derivation (Axiom r) φ ↔ φ ∈ logic (modelsOfRelation r)

A proposition is an axiom of a frame exactly when it belongs to the logic of all models over that frame.