Nuprl Definition : dl_KS
dl_KS ==
dl_KripkeStructure
"Rref":∀i:worlds(self). iRi
"Rtrans":∀r,s,t:worlds(self). (rRs ⇒ sRt ⇒ rRt)
"FP":∀i:worlds(self). ∀a:ℕ. (atmFrc_prop(self;a;i) ⇒ (∀j:worlds(self). (iRj ⇒ atmFrc_prop(self;a;j))))
Definitions occuring in Statement :
dl_KripkeStructure: dl_KripkeStructure,
atmFrc_prop: atmFrc_prop(k;a;s),
KrRel: sRt,
worlds: worlds(k),
record+: record+,
nat: ℕ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
token: "$token"
Definitions occuring in definition :
record+: record+,
dl_KripkeStructure: dl_KripkeStructure,
token: "$token",
nat: ℕ,
all: ∀x:A. B[x],
worlds: worlds(k),
implies: P ⇒ Q,
KrRel: sRt,
atmFrc_prop: atmFrc_prop(k;a;s)
FDL editor aliases :
dl_KS
Latex:
dl\_KS ==
dl\_KripkeStructure
"Rref":\mforall{}i:worlds(self). iRi
"Rtrans":\mforall{}r,s,t:worlds(self). (rRs {}\mRightarrow{} sRt {}\mRightarrow{} rRt)
"FP":\mforall{}i:worlds(self). \mforall{}a:\mBbbN{}.
(atmFrc\_prop(self;a;i) {}\mRightarrow{} (\mforall{}j:worlds(self). (iRj {}\mRightarrow{} atmFrc\_prop(self;a;j))))
Date html generated:
2020_05_20-AM-09_01_25
Last ObjectModification:
2019_11_27-PM-02_07_57
Theory : dynamic!logic
Home
Index