def true_at (M : KripkeModel) (φ : M.W → Prop) (w : M.W) : Prop

Equations

• true_at M φ w = φ w

def true_in_model (M : KripkeModel) (φ : M.W → Prop) : Prop

Equations

• true_in_model M φ = ∀ (w : M.W), true_at M φ w

theorem dual_valid (M : KripkeModel) (p : M.W → Prop) (w : M.W) : diamond M p w ↔ ¬box M (fun (v : M.W) => ¬p v) w

theorem modal_axiom_K_valid (F : KripkeModel) (A B : F.W → Prop) (w : F.W) : box F (fun (w : F.W) => A w → B w) w → box F A w → box F B w

theorem modal_axiom_T_valid (F : KripkeModel) (h_refl : ∀ (w : F.W), F.R w w) (A : F.W → Prop) (w : F.W) : box F A w → A w

theorem modal_dense_valid (F : KripkeModel) (h_dense : ∀ (w u : F.W), F.R w u → ∃ (v : F.W), F.R w v ∧ F.R v u) (A : F.W → Prop) (w : F.W) : box F (box F A) w → box F A w

theorem modal_axiom_4_valid (F : KripkeModel) (h_trans : ∀ (w v u : F.W), F.R w v → F.R v u → F.R w u) (A : F.W → Prop) (w : F.W) : box F A w → box F (box F A) w

theorem modal_axiom_D_valid (F : KripkeModel) (h_serial : ∀ (w : F.W), ∃ (v : F.W), F.R w v) (A : F.W → Prop) (w : F.W) : box F A w → diamond F A w

theorem modal_axiom_B_valid (F : KripkeModel) (h_symm : ∀ (w v : F.W), F.R w v → F.R v w) (A : F.W → Prop) (w : F.W) : A w → box F (diamond F A) w

theorem modal_axiom_5_valid (F : KripkeModel) (h_euclid : ∀ (w u v : F.W), F.R w u → F.R w v → F.R u v) (A : F.W → Prop) (w : F.W) : diamond F A w → box F (diamond F A) w

def valid_on_frame (F : KripkeFrame) (φ : (M : KripkeModel) → M.W → Prop) : Prop

Equations

• valid_on_frame F φ = ∀ (V : F.W → Prop → Prop) (w : F.W), φ { toKripkeFrame := F, V := V } w

theorem valid_D_implies_serial {F : KripkeFrame} (valid_D : ∀ (M : KripkeModel), M.toKripkeFrame = F → ∀ (p : M.W → Prop) (w : M.W), box M p w → diamond M p w) (w : F.W) : ∃ (v : F.W), F.R w v

theorem valid_T_implies_reflexive {F : KripkeFrame} (valid_T : ∀ (M : KripkeModel), M.toKripkeFrame = F → ∀ (p : M.W → Prop) (w : M.W), box M p w → p w) (w : F.W) : F.R w w

theorem valid_B_implies_symmetric {F : KripkeFrame} (valid_B : ∀ (M : KripkeModel), M.toKripkeFrame = F → ∀ (p : M.W → Prop) (w : M.W), p w → box M (diamond M p) w) (u v : F.W) : F.R u v → F.R v u

theorem valid_4_implies_transitive (valid_4 : ∀ (F : KripkeFrame) (M : KripkeModel), M.toKripkeFrame = F → ∀ (p : M.W → Prop) (w : M.W), box M p w → box M (box M p) w) (F : KripkeFrame) (x y z : F.W) : F.R x y → F.R y z → F.R x z

theorem valid_5_implies_euclidean : (∀ (F : KripkeFrame) (M : KripkeModel), M.toKripkeFrame = F → ∀ (p : M.W → Prop) (w : M.W), diamond M p w → box M (diamond M p) w) → ∀ (F : KripkeFrame) (w u v : F.W), F.R w u → F.R w v → F.R u v