$0 \in \mathbb{N}$

[felixpernegger]

Also see this.

Right now, it is not a fixed convention in pi base whether $0$ is a natural number and we usually avoid talking about it.
It is famously disputed, but it seems like $0 \in \mathbb{N}$ is now the overwhelming opinion (making $(\mathbb{N},+)$ a monoid, for example also in Lean.

So stating that $0 \in \mathbb{N}$ in say the wiki, would likely be beneficial.

On a similar note, using $\omega$ very often (as is the case right now) might be mathematically alright, but I doubt anyone who has not done set theory really knows about that convention. So while you can easily google it, why make it harder for most people for no reason?

[prabau]

In the literature, whether $\mathbb N$ contains $0$ or not really depends on the convention of each author. That's why it's always a good idea to explicitly mention which convention is followed whenever we make use of $\mathbb N$.

(And just because Lean uses one convention does not necessarily mean we need to impose the same.)

On the other hand, $\omega$ is not ambiguous. It's the first infinite ordinal, i.e., the set of all finite ordinals, which is exactly $\{0,1,2,\dots\}$. I think $\omega$ is often used in set theoretical topology/general topology under the influence of set theory. The people who started pi-base were set-theoretical topologists, which explains the widespread use of $\omega$ here.

Personally, I don't have a problem sometimes saying for example:
" $n\in\mathbb N$ with $\mathbb N=\{1,2,\dots\}$ " (or with $\mathbb N=\{0,1,\dots\}$)
every time we use it.

Or even $n=1,2,\dots$ if we don't need to use $\mathbb N$ as a set.

@StevenClontz any comment?

[Moniker1998]

Also, do note that $(\mathbb{N}, +)$ being a monoid or not is not a big deal. It's still a semigroup either way.

There's two arguments that I can think of that I would consider, for and against including $0$ into $\mathbb{N}$:

1. You cannot divide by $0$. (for example, we would like to write $\{\frac{1}{n} : n\in\mathbb{N}\}$)
2. How we count cardinals is starting with $0$.