Nuprl Definition : brouwer_prin_27

Nuprl Definition : brouwer_prin_27_5

another version of brouwer's principle.
It is important because it is used in Kleene's
proof of brouwer's non-classical fan thm
Kleene suggests that it can be proved from
brouwer_prin_for_num_27_2
I will try to do the proof if I have time

brouwer_prin_27_5{i:l}() ==

A:

.

g:

List

.
(spr(g)

(

f:

. ((f

spr(g))

(

b:

. (A f b))))

(

T:

List

f:

((f

spr(g))

(

!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), in_spr: (f

spr(g)), 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_27_5
brouwer\_prin\_27\_5\{i:l\}() == \mforall{}A:\mBbbN{} {}\mrightarrow{} \mBbbN{} {}\mrightarrow{} \mBbbN{} {}\mrightarrow{} \mBbbP{}. \mforall{}g:\mBbbN{} List {}\mrightarrow{} \mBbbN{}. (spr(g) {}\mRightarrow{} (\mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((f \mmember{} spr(g)) {}\mRightarrow{} (\mexists{}b:\mBbbN{}. (A f b)))) {}\mRightarrow{} (\mexists{}T:\mBbbN{} List {}\mrightarrow{} \mBbbN{} \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{} ((f \mmember{} spr(g)) {}\mRightarrow{} (\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_40 Last ObjectModification: 2013_03_17-PM-04_51_11 Home Index