Nuprl Definition : vr_AC1p
vr_AC1p ==
[T:Type]
F:T 
. ((X:T . ((F X) 
(
x:T. (X x)))) (f:T T. X:T . ((F X) (X (f X)))))
Definitions occuring in Statement :
uall: [x:A]. B[x],
prop: ,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
apply: f a,
function: x:A B[x],
universe: Type
FDL editor aliases :
vr_AC1p
vr\_AC1p ==
\mforall{}[T:Type]
\mforall{}F:T {}\mrightarrow{} \mBbbP{} {}\mrightarrow{} \mBbbP{}
((\mforall{}X:T {}\mrightarrow{} \mBbbP{}. ((F X) {}\mRightarrow{} (\mexists{}x:T. (X x)))) {}\mRightarrow{} (\mexists{}f:T {}\mrightarrow{} \mBbbP{} {}\mrightarrow{} T. \mforall{}X:T {}\mrightarrow{} \mBbbP{}. ((F X) {}\mRightarrow{} (X (f X)))))
Date html generated:
2012_02_20-PM-03_33_27
Last ObjectModification:
2012_02_02-PM-01_55_21
Home
Index