Q. What is the weakest system that proves Dedekind's categoricity theorem for second-order arithmetic?
In his classic essay 'Was sind und was sollen die Zahlen?', Dedekind proved the categoricity of the second-order Peano axioms, i.e. that all simply infinite systems---in modern terminology, models of those axioms---are isomorphic to one another. This proof was carried out in Dedekind's informal system of set theory.
Feferman and Hellman (1995) carried out a proof of this result in their system EFSC, the "Elementary theory of Finite Sets and Classes". This system has an