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 is an element of A and f : A -> A. A subset X subset of A is said to be inductive if i is an element of X and for all a (a is an element of X double right arrow f (a) is an element of 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 is not an element of 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 is an element of 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 RCA(0)*. From this and similar equivalences we draw some foundational/philosophical consequences. (c) 2012 Elsevier B.V. All rights reserved.