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 extension EFSC* which they say is interpretable in ACA_0, and is a conservative extension of PA.
Furthermore, they say that "The proof of the categoricity theorem (§1) uses only a small part of EFSC. This part should be interpretable in the system designated by Friedman RCA_0", and ask "What is a nice axiomatization of a subsystem of EFSC (i) in which categoricity is provable, and (ii) which is equivalent in strength to PRA?"
This suggests that Feferman and Hellman believe that the categoricity result is provable in PRA. Has anyone actually proved this result?
- R. Dedekind. Was sind und was sollen die Zahlen? 1888.
- S. Feferman and G. Hellman. Predicative foundations of arithmetic. Philosophical Logic, 24:1-17, 1995.