Nuprl Definition : cWO
cWO(T;x,y.R[x; y]) == ∀f:ℕ ⟶ T. (↓∃n:ℕ. (¬R[f n; f (n + 1)]))
Definitions occuring in Statement :
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
squash: ↓T,
apply: f a,
function: x:A ⟶ B[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
squash: ↓T,
exists: ∃x:A. B[x],
nat: ℕ,
not: ¬A,
apply: f a,
add: n + m,
natural_number: $n
FDL editor aliases :
cWO
Latex:
cWO(T;x,y.R[x; y]) == \mforall{}f:\mBbbN{} {}\mrightarrow{} T. (\mdownarrow{}\mexists{}n:\mBbbN{}. (\mneg{}R[f n; f (n + 1)]))
Date html generated:
2016_05_13-PM-03_51_47
Last ObjectModification:
2015_09_22-PM-05_45_25
Theory : bar-induction
Home
Index