Nuprl Definition : dl_KripkeStructure
dl_KripkeStructure ==
"w":Type
"iPO":worlds(self) ⟶ worlds(self) ⟶ ℙ
"mAR":worlds(self) ⟶ worlds(self) ⟶ ℙ
"F":ℕ ⟶ worlds(self) ⟶ ℙ
"G":ℕ ⟶ worlds(self) ⟶ worlds(self) ⟶ ℙ
Definitions occuring in Statement :
worlds: worlds(k),
record+: record+,
record: record(x.T[x]),
nat: ℕ,
top: Top,
prop: ℙ,
function: x:A ⟶ B[x],
token: "$token",
universe: Type
Definitions occuring in definition :
record+: record+,
record: record(x.T[x]),
top: Top,
universe: Type,
token: "$token",
nat: ℕ,
function: x:A ⟶ B[x],
worlds: worlds(k),
prop: ℙ
FDL editor aliases :
dl_KripkeStructure
Latex:
dl\_KripkeStructure ==
"w":Type
"iPO":worlds(self) {}\mrightarrow{} worlds(self) {}\mrightarrow{} \mBbbP{}
"mAR":worlds(self) {}\mrightarrow{} worlds(self) {}\mrightarrow{} \mBbbP{}
"F":\mBbbN{} {}\mrightarrow{} worlds(self) {}\mrightarrow{} \mBbbP{}
"G":\mBbbN{} {}\mrightarrow{} worlds(self) {}\mrightarrow{} worlds(self) {}\mrightarrow{} \mBbbP{}
Date html generated:
2019_10_15-AM-11_46_52
Last ObjectModification:
2019_05_21-AM-09_37_59
Theory : dynamic!logic
Home
Index