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