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