[auggierose]

I added a bit to my previous answer before seeing your reply. But yes, it does not really matter in terms of notation if you use ℕ and ℕ₀, or ℕ⁺ and ℕ. But both ℕ₀ and ℕ⁺ are slightly annoying compared to just ℕ, and so it changes where you start counting from: 0 or 1. If you start counting from 0, you will mostly not need ℕ⁺, and mostly just use ℕ and ℤ. If you start counting from 1, you will use ℕ more than ℕ₀, but you will use ℕ₀ often enough so that you need ℕ, ℕ₀ and ℤ.

Logic likes to unify things, so formal definitions usually start with 0, and conflate sizing and labelling. Note that Peano first started counting from 1. Later on he changed it to 0. Doesn't mean that's the right thing to do, though. Maybe these two concepts should be kept separate: ℕ for (default) labelling, and ℕ₀ for sizing.