Commit d659b15d authored by jfschaefer's avatar jfschaefer

today's stuff (semantics of FOL as view into set theory)

parent d1a1aeac
namespace https://mathhub.info/Teaching/lbs1920 ❚
import krmt http://mathhub.info/Teaching/KRMT ❚
theory proplog : ur:?LF =
prop : type ❘ # o ❙
conjunction : prop ⟶ prop ⟶ prop ❘ # 1 ∧ 2 prec 60❙
negation : prop ⟶ prop ❘ # ¬ 1 prec 80 ❙
disjunction : prop ⟶ prop ⟶ prop ❘ # 1 ∨ 2 prec 50 ❘ = [A,B] (¬ ( ¬ A ∧ ¬ B )) ❙
implication : prop ⟶ prop ⟶ prop ❘ # 1 ⇒ 2 prec 40 ❘ = [A,B] ¬ A ∨ B ❙
biimplication : prop ⟶ prop ⟶ prop ❘ # 1 ⇔ 2 prec 30 ❘ = [A, B] (A ⇒ B) ∧ (B ⇒ A) ❙
// theory TruthValues : http://mathhub.info/MitM/Foundation?DescriptionOperator = ❚
theory TruthValues : krmt:?Meta =
// booleans : 𝒰 100 ❘ # ℬ ❙ // truth values ❙
booleans : type ❘ # ℬ ❙ // truth values ❙
true : ℬ ❘ # T ❙
false : ℬ ❘ # F ❙
// 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) ❙
view proplogSemantics : ?proplog -> ?TruthValues =
prop = ℬ ❙
conjunction = max ❙
negation = switch ❙
theory folSyntax : ur:?LF =
include ?proplog ❙
individuals : type ❘ # ι ❙
forall : (ι ⟶ o) ⟶ o ❘ # ∀ 1 ❙ // example: (∀ [x:ι] ((p x) : o)) : o ❙
exists : (ι ⟶ o) ⟶ o ❘ # ∃ 1 ❘ = [p] ¬ (∀ [x] ¬ (p x)) ❙
theory folModels : krmt:?Meta =
include ☞http://mathhub.info/Teaching/KRMT?TypedSets ❙
include ?TruthValues ❙
object : type ❘ # 𝒪 ❙
domain = fullset 𝒪 ❘ # 𝒟 ❙ // set of objects ❙
set_equal : set 𝒪 ⟶ set 𝒪 ⟶ ℬ ❘
= [P1, P2] if_then_else ℬ (P1 ≐ P2) T F ❘
# 1 == 2 ❙
is_the_universe : set 𝒪 ⟶ ℬ ❘ = [P] P == 𝒟 ❙
view folSemantics : ?folSyntax -> ?folModels =
include ?proplogSemantics ❙
individuals = object ❙
// forall : (object ⟶ ℬ) ⟶ ℬ ❙
forall = [P : object ⟶ ℬ] if_then_else ℬ (in ℬ F (im P 𝒟)) F T ❙
theory MLO : ur:?LF =
include ?proplog ❙
box : o ⟶ o ❘ # □ 1 prec 20 ❙
diamond : o ⟶ o ❘ # ◇ 1 prec 20 ❘ = [x] ¬ □ ¬ x ❙
// theory KripkeFrames : ur:?LF =
include ?TruthValues ❙
worlds : type ❘ # 𝒲 ❙
acr : 𝒲 ⟶ 𝒲 ⟶ ℬ ❘ # 1 ℛ 2 ❙ // accessibility relation ❙
allAccessible :
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