I've heard that if you assume the existence of (Dedekind) infinitely many objects, you can derive -- in second-order logic, given suitable definitions -- the (second-order) Peano axioms for arithmetic. I was wondering how much second-order logic is actually needed for that result, and how exactly the natural numbers are defined in that context. (Do we need Choice? how much second-order comprehension needs to be assumed?) Any advice on relevant literature or a sketch of the proof would be highly appreciated.

I've heard that if you assume the existence of (Dedekind) infinitely many objects, you can derive -- in second-order logic, given suitable definitions -- the (second-order) Peano axioms for arithmetic. I was wondering how much second-order logic is actually needed for that result, and how exactly the natural numbers are defined in that context. The obvious way would be to start by an application of (countable) Choice, to get representatives for the natural numbers. How much second-order comprehension is then needed subsequently? And is it possible to get this result without Choice? Any advice on relevant literature or a sketch of the proof would be highly appreciated.