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