Nuprl Definition : AC_1_0
AC_1_0{i:l}() == ∀R:(ℕ ⟶ ℕ) ⟶ ℕ ⟶ ℙ. ((∀f:ℕ ⟶ ℕ. (↓∃n:ℕ. (R f n))) ⇒ (↓∃F:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f:ℕ ⟶ ℕ. (R f (F f))))
Definitions occuring in Statement :
nat: ℕ,
prop: ℙ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
squash: ↓T,
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x]
Definitions occuring in definition :
prop: ℙ,
implies: P ⇒ Q,
squash: ↓T,
exists: ∃x:A. B[x],
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
nat: ℕ,
apply: f a
FDL editor aliases :
AC_1_0
Latex:
AC\_1\_0\{i:l\}() ==
\mforall{}R:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{} {}\mrightarrow{} \mBbbP{}
((\mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. (\mdownarrow{}\mexists{}n:\mBbbN{}. (R f n))) {}\mRightarrow{} (\mdownarrow{}\mexists{}F:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. (R f (F f))))
Date html generated:
2016_05_14-PM-04_15_36
Last ObjectModification:
2015_09_22-PM-06_02_31
Theory : fan-theorem
Home
Index