Nuprl Definition : dl-valid
|= phi == ∀K:Type. ∀R:ℕ ⟶ K ⟶ K ⟶ ℙ. ∀P:ℕ ⟶ K ⟶ ℙ. ∀k:K. ([|phi|] k)
Definitions occuring in Statement :
dl-prop-sem: [|phi|]
,
nat: ℕ
,
prop: ℙ
,
so_apply: x[s]
,
all: ∀x:A. B[x]
,
apply: f a
,
function: x:A ⟶ B[x]
,
universe: Type
Definitions occuring in definition :
universe: Type
,
nat: ℕ
,
function: x:A ⟶ B[x]
,
prop: ℙ
,
all: ∀x:A. B[x]
,
apply: f a
,
dl-prop-sem: [|phi|]
,
so_apply: x[s]
FDL editor aliases :
dl-valid
Latex:
|= phi == \mforall{}K:Type. \mforall{}R:\mBbbN{} {}\mrightarrow{} K {}\mrightarrow{} K {}\mrightarrow{} \mBbbP{}. \mforall{}P:\mBbbN{} {}\mrightarrow{} K {}\mrightarrow{} \mBbbP{}. \mforall{}k:K. ([|phi|] k)
Date html generated:
2019_10_15-AM-11_44_08
Last ObjectModification:
2019_03_26-AM-11_49_26
Theory : dynamic!logic
Home
Index