structure KripkeFrame : Type 1

• W : Type
• R : self.W → self.W → Prop

def KripkeFrame_is_reflexive (F : KripkeFrame) : Prop

Equations

• KripkeFrame_is_reflexive F = ∀ (w : F.W), F.R w w

def KripkeFrame_is_transitive (F : KripkeFrame) : Prop

Equations

• KripkeFrame_is_transitive F = ∀ (w v u : F.W), F.R w v → F.R v u → F.R w u

def KripkeFrame_is_symmetric (F : KripkeFrame) : Prop

Equations

• KripkeFrame_is_symmetric F = ∀ (w v : F.W), F.R w v → F.R v w

def KripkeFrame_is_serial (F : KripkeFrame) : Prop

Equations

• KripkeFrame_is_serial F = ∀ (w : F.W), ∃ (v : F.W), F.R w v

def KripkeFrame_is_dense (F : KripkeFrame) : Prop

Equations

• KripkeFrame_is_dense F = ∀ (w v : F.W), F.R w v → ∃ (u : F.W), F.R w u ∧ F.R u v

def KripkeFrame_is_euclidean (F : KripkeFrame) : Prop

Equations

• KripkeFrame_is_euclidean F = ∀ (w v u : F.W), F.R w v → F.R w u → F.R v u

structure KripkeModelextends KripkeFrame : Type 1

• W : Type
• R : self.W → self.W → Prop
• V : self.W → Prop → Prop

def box (F : KripkeModel) (φ : F.W → Prop) (w : F.W) : Prop

Equations

• box F φ w = ∀ (w' : F.W), F.R w w' → φ w'

def diamond (F : KripkeModel) (φ : F.W → Prop) (w : F.W) : Prop

Equations

• diamond F φ w = ∃ (w' : F.W), F.R w w' ∧ φ w'