Reverse mathematics and Peano categoricity

We investigate the reverse-mathematical status of several theorems to the effect that the natural number system is second-order categorical. One of our results is as follows. Define a system to be a triple A,i,f such that A is a set and i∈A and f:A→A. A subset X⊆A is said to be inductive if i∈X and ∀a (a∈X⇒f(a)∈X). The system A,i,f is said to be inductive if the only inductive subset of A is A itself. Define a Peano system to be an inductive system such that f is one-to-one and i∉the range of f. The standard example of a Peano system is N,0,S where N={0,1,2,…,n,…}=the set of natural numbers and S:N→N is given by S(n)=n+1 for all n∈N. Consider the statement that all Peano systems are isomorphic to N,0,S. We prove that this statement is logically equivalent to WKL0 over . From this and similar equivalences we draw some foundational/philosophical consequences.