Despite the name, in the usual mathematical meaning of the term, Peano arithmetic does not define arithmetic at all, only the successor operation, and everything else is built from there. Once we have those, for the model (Z_{\ge 0}, 0, ++), we certainly usually do define x0 = 0 for all x; and, you're right, if for the model (Z_{\ge 1}, 1, ++) we defined x1 = 1 for all x (as no-one could stop us from doing), then we'd just be dealing with "0 by another name." But it might be equally sensible, if our model of Peano arithmetic is (Z_{\ge 1}, 1, ++), to define x1 = x for all x, in which case we recover the expected arithmetic.
2 of the axioms are:
1. For all x, x*0 = 0
2. For all x, y: x*S(y) = x*y + y
(Now having written that and looking back, I see that, in my previous post https://news.ycombinator.com/item?id=43442074, I wrote "Despite the name, in the usual mathematical meaning of the term, Peano arithmetic does not define arithmetic at all, only the successor operation, and everything else is built from there." Perhaps this infelicitious-to-the-point-of-wrong wording of mine is the source of our difference? I meant to say that Peano arithmetic does not axiomatize arithmetic at all, but that arithmetic can be defined from the axioms. Thus the specific definition x[pt] = [pt] is eminently sensible if we consider the distinguished point [pt] to be playing the usual role of 0; but the definition x[pt] = x is also sensible if we consider it to be playing the usual role of 1, and even things like x[pt] = x + x + x + x + x can be tolerated if we think of [pt] as standing for 5, say. The axioms cannot distinguish among these options, because the axioms say nothing about multiplication.)
Enderton, “A Mathematical Introduction to Logic, 2nd Ed.”, p,203,269-270
Kleene, “Mathematical Logic”, p.206
EDIT: It seems like you're talking about Peano's original historical formulation of arithmetic? That's all well and good but it is categorically not what is meant by "Peano Arithmetic" in any modern context. I've provided two citations from pretty far apart in time editions of common logic texts (well, "Mathematical Logic" is a bit of a weird book, but Kleene is certainly an authority) and I hope that demonstrates this.
There's a lot of reasons that the theory is pretty much always discussed as a first-order theory. The biggest, of course, is that when taken as a first-order theory it fits neatly into the proof and statement of Godel's Incompleteness Theorems, but iiuc it's just generally much less useful in a model theoretic context to take it as a second order theory (to the point where I only ever saw this discussed as a historical note, not as a mathematical one).
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.
