[JadeNB]

> EDIT 2: This is all a digression anyway. Both first- and second-order PA label the start of the Z-chain as 0; so any model of PA contains 0 when interpreted as a model of PA.

Ah, good point that this was the actual source o# the discussion. This one at least can be argued, because the question is about how things should be axiomatized/defined, not how they are. And certainly the theory of the "natural numbers starting with 1" can be axiomatised just as well as the "natural numbers starting with 0." All these axioms are made by humans, and an appeal to existing axioms here can only say what's been done, not what should be. (And I say this as someone who does start my naturals at 0.)