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