On Wednesday, March 4, 2020 at 10:36:50 AM UTC-5, Benoit wrote: ... > Beware that in set.mm, the symbol NN does not denote the natural numbers, >> but only the nonzero natural numbers. Therefore, stating ~ inductionexd >> with " N e. NN0 " is more... natural. (And its proof might be shorter >> since the base case involves smaller numbers.) >> > ..
This should probably be another thread, but maybe it is time to rename "NN" to "NN1" to put this issue (which has been discussed before) to rest. As I've made known, I personally prefer NN since it is the set of "natural numbers" that books on analysis usually use, and analysis is all about the real and complex numbers that NN is a subset of. But I recognize that at some point avoiding confusion may become more important than aesthetics or conforming to literature practice. In the meantime, note that we changed most comments in set.mm to use "positive integer" instead of "natural number" for NN members to avoid ambiguity, so that is one way to tell what NN means if you forget. In early set.mm, we do call members of _om (omega), which start at zero, "natural numbers" in comments, because that is the practice of set theorists (and it would be rather hard to develop ordinals without zero). Interestingly, zero becomes inconvenient and isn't used for the Dedekind construction of reals, so we define positive ordinals with ~ df-ni (intended to be used only for the construction). Norm -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/53bc3237-8f65-4397-b0ac-77c0930002dc%40googlegroups.com.
