@TimothyChow: I'm not confusing anything. I didn't say we have to stop at PA at all. Didn't I mention ATR? The point is, the real world seems to have something like a standard model of PA, and that is the reason we even invented PA in the first place. Your argument about being able to add true arithmetic sentences applies only if you can justify your additional axioms as true. It gets harder and harder to do so, and it's unclear if you can go much further than ATR. — user21820 9 hours ago

@TimothyChow: I think you're seriously misreading my answer. I explicitly stated "standard model of PA minus". The axioms of PA− very clearly correlate to real-world counting. We get from PA− to an interpretation of PA via standardness, and then to ACA0 via the syntactic interpretation of sets as simply arithmetical properties, and then to ACA via PA-based meta-reasoning. I did not at any point appeal to categoricity of PA2 to define $ℕ$, as categoricity is an illusion. — user21820 52 secs ago