Commit 14fbf4e8 authored by jfschaefer's avatar jfschaefer

modal semantics

parent d659b15d
......@@ -21,6 +21,8 @@ theory TruthValues : krmt:?Meta =
// switch : ℬ ⟶ ℬ ❘ = [b] if b ≐ T then F else T ❙ // switch F to T and T to F ❙
switch : ℬ ⟶ ℬ ❘ = [b] if_then_else ℬ (b ≐ T) F T ❙
max : ℬ ⟶ ℬ ⟶ ℬ ❘ = [a,b] if_then_else ℬ (a ≐ T) b F ❙ // maximum element (T > F) ❙
impl = [a, b] switch (max (switch a) b) ❙
view proplogSemantics : ?proplog -> ?TruthValues =
......@@ -60,6 +62,28 @@ theory MLO : ur:?LF =
diamond : o ⟶ o ❘ # ◇ 1 prec 20 ❘ = [x] ¬ □ ¬ x ❙
theory KripkeModel : krmt:?Meta =
include ☞http://mathhub.info/Teaching/KRMT?TypedSets ❙
include ?TruthValues ❙
world_type : type ❘ # 𝒲 ❙
accessibility_relation : 𝒲 ⟶ 𝒲 ⟶ ℬ ❘ # 1 ℛ 2 ❙
view modalSemantics : ?MLO -> ?KripkeModel =
include ?proplogSemantics ❙
prop = 𝒲 ⟶ ℬ ❙
conjunction = [A : 𝒲 ⟶ ℬ, B : 𝒲 ⟶ ℬ] [w : 𝒲] max (A w) (B w) ❙
negation = [A : 𝒲 ⟶ ℬ, w : 𝒲] switch (A w) ❙
// box = [A : 𝒲 ⟶ ℬ, w : 𝒲] ∀ ([v : 𝒲] (w ℛ v) ⇒ (A v)) ❙
box = [A : 𝒲 ⟶ ℬ, w : 𝒲]
([P : 𝒲 ⟶ ℬ] if_then_else ℬ (in ℬ F (im P (fullset 𝒲))) F T)
([v : 𝒲] impl (w ℛ v) (A v)) ❙
// theory KripkeFrames : ur:?LF =
include ?TruthValues ❙
worlds : type ❘ # 𝒲 ❙
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment