Semantics of Modal Logic

structure Cslib.Logic.Modal.Model (World : Type u) (τ : PFunctor.{u_1, u_2}) (Atom : Type v) extends Cslib.Frame World τ : Type (max (max (max u u_1) u_2) v)

A model is a frame equipped with a valuation of atoms at worlds.

• r (op : τ.A) : World → (τ.B op → World) → Prop
• v : World → Atom → Prop

  Valuation of atoms at a world.

def Cslib.Logic.Modal.Satisfies {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} (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 Cslib.Logic.Modal.Proposition.false = False
• Cslib.Logic.Modal.Satisfies m w φ.not = ¬Cslib.Logic.Modal.Satisfies m w φ
• Cslib.Logic.Modal.Satisfies m w (φ₁.or φ₂) = (Cslib.Logic.Modal.Satisfies m w φ₁ ∨ Cslib.Logic.Modal.Satisfies m w φ₂)
• Cslib.Logic.Modal.Satisfies m w (Cslib.Logic.Modal.Proposition.triangle op φs) = ∃ (ws : τ.B op → World), m.r op w ws ∧ ∀ (i : τ.B op), Cslib.Logic.Modal.Satisfies m (ws i) (φs i)

structure Cslib.Logic.Modal.Judgement (World : Type u_1) (τ : PFunctor.{u_2, u_3}) (Atom : Type u_4) : Type (max (max (max u_1 u_2) u_3) u_4)

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} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} (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} {τ : PFunctor.{u_3, u_4}} {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} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} {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} {τ✝ : PFunctor.{u_3, u_4}} {m : Model World✝ τ✝ Atom} {w : World✝} {a : Atom} : ⇓{ m := m, w := w, φ := Proposition.atom a } ↔ m.v w a

@[simp]

theorem Cslib.Logic.Modal.Satisfies.false {World✝ : Type u_1} {τ✝ : PFunctor.{u_2, u_3}} {Atom✝ : Type u_4} {m : Model World✝ τ✝ Atom✝} {w : World✝} : ⇓{ m := m, w := w, φ := ⊥ } ↔ False

theorem Cslib.Logic.Modal.Satisfies.not_iff_not {World✝ : Type u_1} {τ✝ : PFunctor.{u_2, u_3}} {Atom✝ : Type u_4} {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.

@[simp]

theorem Cslib.Logic.Modal.Satisfies.true {World✝ : Type u_1} {τ✝ : PFunctor.{u_2, u_3}} {Atom✝ : Type u_4} {m : Model World✝ τ✝ Atom✝} {w : World✝} : ⇓{ m := m, w := w, φ := ⊤ }

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

theorem Cslib.Logic.Modal.Satisfies.triangle_iff_exists {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} {w : World} {op : τ.A} {φs : τ.B op → Proposition τ Atom} {m : Model World τ Atom} : ⇓{ m := m, w := w, φ := HasTriangle.triangle op φs } ↔ ∃ (ws : τ.B op → World), m.r op w ws ∧ ∀ (i : τ.B op), ⇓{ m := m, w := ws i, φ := φs i }

theorem Cslib.Logic.Modal.Satisfies.triangle_not_iff_exists_not {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} {w : World} {op : τ.A} {φs : τ.B op → Proposition τ Atom} {m : Model World τ Atom} : ⇓{ m := m, w := w, φ := HasTriangle.triangle op (HasNot.not φs) } ↔ ∃ (ws : τ.B op → World), m.r op w ws ∧ ∀ (i : τ.B op), ¬⇓{ m := m, w := ws i, φ := φs i }

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

Characterisation of the ∧ connective.

Conjunction 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} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} {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} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} {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.nabla_iff_forall {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} {w : World} {op : τ.A} {φs : τ.B op → Proposition τ Atom} {m : Model World τ Atom} : ⇓{ m := m, w := w, φ := HasNabla.nabla op φs } ↔ ∀ (ws : τ.B op → World), m.r op w ws → ∃ (i : τ.B op), ⇓{ m := m, w := ws i, φ := φs i }

Characterisation of ∇.

Necessity 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.finiteAnd_iff_forall {World✝ : Type u_1} {τ✝ : PFunctor.{u_2, u_3}} {Atom✝ : Type u_4} {m : Model World✝ τ✝ Atom✝} {s : World✝} {φs : List (Proposition τ✝ Atom✝)} : ⇓{ m := m, w := s, φ := finiteAnd φs } ↔ ∀ φ ∈ φs, ⇓{ m := m, w := s, φ := φ }

A state satisfies a finite conjunction iff it satisfies all conjuncts.

theorem Cslib.Logic.Modal.Satisfies.finiteOr_iff_exists {World✝ : Type u_1} {τ✝ : PFunctor.{u_2, u_3}} {Atom✝ : Type u_4} {m : Model World✝ τ✝ Atom✝} {s : World✝} {φs : List (Proposition τ✝ Atom✝)} : ⇓{ m := m, w := s, φ := finiteOr φs } ↔ ∃ φ ∈ φs, ⇓{ m := m, w := s, φ := φ }

A state satisfies a finite disjunction iff it satisfies some disjunct.

@[reducible, inline]

abbrev Cslib.Logic.Modal.theory {World : Type u_1} {τ : PFunctor.{u_3, u_4}} {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} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} (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} {τ✝ : PFunctor.{u_2, u_3}} {Atom✝ : Type u_4} {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} {τ✝ : PFunctor.{u_2, u_3}} {Atom✝ : Type u_4} {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} {τ✝ : PFunctor.{u_2, u_3}} {Atom✝ : Type u_4} {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} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} {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 : Type u_1} {τ : PFunctor.{u_2, u_3}} (f : Frame World τ) : Type

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

@[instance_reducible]

instance Cslib.Logic.Modal.instInferenceSystemAxiomProposition {World : Type u_1} {τ : PFunctor.{u_3, u_4}} {Atom : Type u_2} (f : Frame World τ) : InferenceSystem (Axiom f) (Proposition τ Atom)

A proposition φ is an axiom under a frame f 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} {τ : PFunctor.{u_2, u_3}} {Atom✝ : Type u_4} {φ : Proposition τ Atom✝} (f : Frame World τ) : (∀ (v : World → Atom✝ → Prop) (w : World), ⇓{ m := { toFrame := f, v := v }, w := w, φ := φ }) ↔ InferenceSystem.derivation (Axiom f) φ

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

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

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

theorem Cslib.Logic.Modal.Satisfies.subst_apply_iff {τ : PFunctor.{u_1, u_2}} {op : τ.A} {Atom : Type u_3} {World✝ : Type u_4} {m : Model World✝ τ Atom} {w : World✝} [DecidableEq (τ.B op)] {φs : PropositionMap τ op Atom} {i j : τ.B op} {φ : Proposition τ Atom} : ⇓{ m := m, w := w, φ := φs[i := φ] j } ↔ j = i ∧ ⇓{ m := m, w := w, φ := φ } ∨ j ≠ i ∧ ⇓{ m := m, w := w, φ := φs j }

theorem Cslib.Logic.Modal.Satisfies.k {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {op : τ.A} {Atom : Type u_4} (f : Frame World τ) {φs : PropositionMap τ op Atom} [DecidableEq (τ.B op)] {i : τ.B op} {φ₁ φ₂ : Proposition τ Atom} (hi : φs i = HasImp.imp φ₁ φ₂) : InferenceSystem.derivation (Axiom f) (HasImp.imp (HasNabla.nabla op φs) (HasImp.imp (HasNabla.nabla op φs[i := φ₁]) (HasNabla.nabla op φs[i := φ₂])))

Axiom K, valid for all frames.

This is from Definition 4.13 in [BRV01].

theorem Cslib.Logic.Modal.Satisfies.dual {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {op : τ.A} {Atom : Type u_4} (f : Frame World τ) {φs : PropositionMap τ op Atom} : InferenceSystem.derivation (Axiom f) (HasIff.iff (HasTriangle.triangle op φs) (HasNot.not (HasNabla.nabla op (HasNot.not φs))))

The dual axiom, valid for all frames.

This is from Definition 4.13 in [BRV01].

theorem Cslib.Logic.Modal.Satisfies.triangle_and {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {op : τ.A} {Atom : Type u_4} (f : Frame World τ) (φs₁ φs₂ : PropositionMap τ op Atom) : InferenceSystem.derivation (Axiom f) (HasImp.imp (HasTriangle.triangle op (HasAnd.and φs₁ φs₂)) (HasAnd.and (HasTriangle.triangle op φs₁) (HasTriangle.triangle op φs₂)))

Possibility preserves conjunction.

theorem Cslib.Logic.Modal.Satisfies.triangle_and_nabla {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} {op : τ.A} {w : World} {φs₁ φs₂ : τ.B op → Proposition τ Atom} {m : Model World τ Atom} [DecidableEq (τ.B op)] (h : ⇓{ m := m, w := w, φ := HasAnd.and (HasTriangle.triangle op φs₁) (HasNabla.nabla op φs₂) }) : ∃ (i : τ.B op), ⇓{ m := m, w := w, φ := HasTriangle.triangle op φs₁[i := HasAnd.and (φs₁ i) (φs₂ i)] }

Possibility can be combined with necessity.

This generalises the unimodal law ◇φ₁ ∧ □φ₂ → ◇(φ₁ ∧ φ₂).

theorem Cslib.Logic.Modal.Satisfies.triangle_of_nabla {τ : PFunctor.{u_1, u_2}} {op : τ.A} {Atom : Type u_3} {World✝ : Type u_4} {m : Model World✝ τ Atom} {w : World✝} {φs₁ φs₂ : PropositionMap τ op Atom} [DecidableEq (τ.B op)] (h : ⇓{ m := m, w := w, φ := HasAnd.and (HasNabla.nabla op φs₁) (HasTriangle.triangle op φs₂) }) : ∃ (i : τ.B op), ⇓{ m := m, w := w, φ := HasTriangle.triangle op φs₂[i := φs₁ i] }

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

This generalises the unimodal law □φ₁ ∧ ◇φ₂ → ◇φ₁.

theorem Cslib.Logic.Modal.Satisfies.triangle_of_diagonal {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} {m : Model World τ Atom} {op : τ.A} {w : World} {φ : Proposition τ Atom} [instRefl : Std.Refl (m.diagonal op)] (h : ⇓{ m := m, w := w, φ := φ }) : ⇓{ m := m, w := w, φ := HasTriangle.triangle op (PropositionMap.const op φ) }

If the diagonal relation for op is reflexive, a world satisfying φ also satisfies Δ[op] with φ at every argument position.

theorem Cslib.Logic.Modal.Satisfies.t {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {op : τ.A} {Atom : Type u_4} (f : Frame World τ) [instRefl : Std.Refl (f.diagonal op)] (φ : Proposition τ Atom) : InferenceSystem.derivation (Axiom f) (HasImp.imp φ (HasTriangle.triangle op (PropositionMap.const op φ)))

Axiom T, valid for all frames with reflexive diagonals.

This generalises the unimodal law φ → ◇φ.

theorem Cslib.Logic.Modal.Satisfies.t_refl {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} (f : Frame World τ) {op : τ.A} [Nonempty Atom] (h : ∀ (φ : Proposition τ Atom), InferenceSystem.derivation (Axiom f) (HasImp.imp φ (HasTriangle.triangle op (PropositionMap.const op φ)))) : Std.Refl (f.diagonal op)

Any frame admitting T for op has a reflexive diagonal relation.

theorem Cslib.Logic.Modal.Satisfies.t_nabla_triangle {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {op : τ.A} {Atom✝ : Type u_4} {φ : Proposition τ Atom✝} (f : Frame World τ) [Std.Refl (f.diagonal op)] : InferenceSystem.derivation (Axiom f) (HasIff.iff (HasImp.imp (HasNabla.nabla op (PropositionMap.const op φ)) φ) (HasImp.imp φ (HasTriangle.triangle op (PropositionMap.const op φ))))

In any model whose diagonal relation for op is reflexive, ∇[op]φ → φ is equivalent to φ → Δ[op]φ.

theorem Cslib.Logic.Modal.Satisfies.b {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {op : τ.A} {Atom : Type u_4} (f : Frame World τ) [f.DiagonalSymm op] (φ : Proposition τ Atom) : InferenceSystem.derivation (Axiom f) (HasImp.imp φ (HasNabla.nabla op (PropositionMap.const op (HasTriangle.triangle op (PropositionMap.const op φ)))))

Axiom B, valid for diagonally symmetric frames.

theorem Cslib.Logic.Modal.Satisfies.b_symm {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} {op : τ.A} (f : Frame World τ) [Nonempty Atom] (h : ∀ (φ : Proposition τ Atom), InferenceSystem.derivation (Axiom f) (HasImp.imp φ (HasNabla.nabla op (PropositionMap.const op (HasTriangle.triangle op (PropositionMap.const op φ)))))) : f.DiagonalSymm op

Any frame that admits B at op is diagonally symmetric at op.

theorem Cslib.Logic.Modal.Satisfies.four {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {op : τ.A} {Atom : Type u_4} (f : Frame World τ) [f.Trans op] (φs ψs : PropositionMap τ op Atom) (i : τ.B op) (hi : φs i = HasTriangle.triangle op ψs) : InferenceSystem.derivation (Axiom f) (HasImp.imp (HasTriangle.triangle op φs) (HasTriangle.triangle op ψs))

The 4 axiom, valid for transitive frames.

theorem Cslib.Logic.Modal.Satisfies.four_trans {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} {op : τ.A} (f : Frame World τ) [Nonempty Atom] (e : τ.B op ↪ Atom) (h : ∀ (φs ψs : PropositionMap τ op Atom) (i : τ.B op), φs i = HasTriangle.triangle op ψs → InferenceSystem.derivation (Axiom f) (HasImp.imp (HasTriangle.triangle op φs) (HasTriangle.triangle op ψs))) : f.Trans op

Any frame that admits 4 at op is transitive at op.

theorem Cslib.Logic.Modal.Satisfies.five {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {op : τ.A} {Atom : Type u_4} (f : Frame World τ) [f.RightEuclidean op] (φs : PropositionMap τ op Atom) : InferenceSystem.derivation (Axiom f) (HasImp.imp (HasTriangle.triangle op φs) (HasNabla.nabla op (PropositionMap.const op (HasTriangle.triangle op φs))))

Axiom 5, valid for right-Euclidean frames.

theorem Cslib.Logic.Modal.Satisfies.five_rightEuclidean {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {op : τ.A} {Atom : Type u_4} (f : Frame World τ) (e : τ.B op ↪ Atom) (h : ∀ (φs : PropositionMap τ op Atom), InferenceSystem.derivation (Axiom f) (HasImp.imp (HasTriangle.triangle op φs) (HasNabla.nabla op (PropositionMap.const op (HasTriangle.triangle op φs))))) : f.RightEuclidean op

Any frame that admits 5 at op is right-Euclidean at op.

def Cslib.Logic.Modal.Proposition.valid {World : Type u_1} {τ : PFunctor.{u_3, u_4}} {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.

Corresponds to Definition 1.28 (for classes of models) in [BRV01].

Equations

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

def Cslib.Logic.Modal.logic {World : Type u_1} {τ : PFunctor.{u_3, u_4}} {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.

Corresponds to Definition 1.28 (for classes of models) in [BRV01].

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} {τ : PFunctor.{u_3, u_4}} {Atom : Type u_2} : Antitone logic

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

@[reducible, inline]

abbrev Cslib.Logic.Modal.modelsOfFrame {World : Type u_1} {τ : PFunctor.{u_3, u_4}} {Atom : Type u_2} (f : Frame World τ) : Set (Model World τ Atom)

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

Equations

• Cslib.Logic.Modal.modelsOfFrame f = {m : Cslib.Logic.Modal.Model World τ Atom | m.toFrame = f}

theorem Cslib.Logic.Modal.axiom_iff_mem_logic_modelsOfFrame {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {Atom : Type u_4} (f : Frame World τ) (φ : Proposition τ Atom) : InferenceSystem.derivation (Axiom f) φ ↔ φ ∈ logic (modelsOfFrame f)

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