Nuprl Definition : weakly-infinite

w∃∞p.S[p] ==  ∀p:ℕ(¬¬(∃q:ℕ(p < q ∧ S[q])))



Definitions occuring in Statement :  nat: less_than: a < b all: x:A. B[x] exists: x:A. B[x] not: ¬A and: P ∧ Q
Definitions occuring in definition :  all: x:A. B[x] not: ¬A exists: x:A. B[x] nat: and: P ∧ Q less_than: a < b
FDL editor aliases :  weakly-infinite

Latex:
w\mexists{}\minfty{}p.S[p]  ==    \mforall{}p:\mBbbN{}.  (\mneg{}\mneg{}(\mexists{}q:\mBbbN{}.  (p  <  q  \mwedge{}  S[q])))



Date html generated: 2016_05_13-PM-03_49_51
Last ObjectModification: 2015_09_22-PM-05_45_19

Theory : bar-induction


Home Index