i) you don't actually need to jump directly to second order logic in to get a categorical axiomatization of the natural numbers. There are several weaker ways to do the job: L_omega_omega (which allows infinitary conjunctions), adding a primitive finiteness operator, adding a primitive ancestral operator, allowing the omega rule (i.e. from the infinitely many premises P(0), P(1), ... P(n), ... infer AnP(n)). Second order logic is more powerful than these in that it gives a quasi categorical axiomatization of the universe of sets (i.e. of any two models of ZFC_2, they are either isomorphic or one is isomorphic to an initial segment of the other).
A few points:
i) you don't actually need to jump directly to second order logic in to get a categorical axiomatization of the natural numbers. There are several weaker ways to do the job: L_omega_omega (which allows infinitary conjunctions), adding a primitive finiteness operator, adding a primitive ancestral operator, allowing the omega rule (i.e. from the infinitely many premises P(0), P(1), ... P(n), ... infer AnP(n)). Second order logic is more powerful than these in that it gives a quasi categorical axiomatization of the universe of sets (i.e. of any two models of ZFC_2, they are either isomorphic or one is isomorphic to an initial segment of the other).
ii) although there is a... (read more)