Nuprl Definition : brouwer_prin_for_num_27_2
T will be a functions which computed the correlate
number b by becoming non-zero when it has seen enough
of the infinite sequence to compute b.
the computed b is actually obtained by monusing by 1
because 0 is reserved for signaling "not_computed_yet"
brouwer_prin_for_num_27_2{i:l}() ==
A:
((f: . 
b:. (A f b))
(T: List
f: . (!y:. (T mklist(y;f)) > 0 
(y:. (((T mklist(y;f)) > 0) (A f (T mklist(y;f)--1)))))))
Definitions occuring in Statement :
monus: (a--b),
nat: ,
prop: ,
gt: i > j,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
and: P Q,
apply: f a,
function: x:A B[x],
natural_number: $n,
mklist: mklist(n;f)
FDL editor aliases :
brouwer_prin_for_num_27_2
brouwer\_prin\_for\_num\_27\_2\{i:l\}() ==
\mforall{}A:\mBbbN{} {}\mrightarrow{} \mBbbN{} {}\mrightarrow{} \mBbbN{} {}\mrightarrow{} \mBbbP{}
((\mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. \mexists{}b:\mBbbN{}. (A f b))
{}\mRightarrow{} (\mexists{}T:\mBbbN{} List {}\mrightarrow{} \mBbbN{}
\mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}
(\mexists{}!y:\mBbbN{}. (T mklist(y;f)) > 0
\mwedge{} (\mforall{}y:\mBbbN{}. (((T mklist(y;f)) > 0) {}\mRightarrow{} (A f (T mklist(y;f)--1)))))))
Date html generated:
2013_03_20-AM-10_38_10
Last ObjectModification:
2013_03_17-PM-05_06_46
Home
Index