[sixo]

It's a leaky abstraction, in software terms. Ideally, an abstraction models the semantics of the problem domain "opaquely"; ideally our natural numbers have only the properties of the natural numbers and no others. An additional property leaking through is not like handy "bonus", but a point of confusion. You can't rely on it in proofs involving natural numbers without being careful to delineate which conclusions follow from the construction vs. which are inherent.

[measurablefunc]

Arithmetic is not a categorical theory, meaning there is no unique model for it: https://math.stackexchange.com/questions/4667959/are-there-n...