I've heard that if you assume the existence of (Dedekind) infinitely many objects, you can derive  in secondorder logic, given suitable definitions  the (secondorder) Peano axioms for arithmetic. I was wondering how much secondorder 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 secondorder 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.

1$\begingroup$ If you have a Dedekindinfinite collection $C$ of objects, that means you have a onetoone function $S:C\to C$ and an element $z\in C$ that is not in the range of $S$. Then a reasonable definition of the set $N$ of natural numbers would be the intersection of all subsets of $C$ that contain $z$ and are closed under $S$ (with $z$ serving as zero and $S$ as the successor function). $\endgroup$ – Andreas Blass Oct 29 '19 at 18:34
First note that monadic secondorder logic (i.e. the variant of secondorder logic with secondorder quantifiers only over unary predicates) isn't sufficient. This is implied by the fact that the monadic theory $\mathsf{MSO}(\mathbb{N},0,S)$ is decidable. Thus further I consider secondorder logic with quantifiers $\forall X^n$ and $\exists X^n$ over predicates of arbitrary arity $n$.
Before discussing interpretation of natural numbers, let me discuss the correspondence between secondorder logic and positive inductive definitions. Any formula $\varphi(X^1,x)$ defines operator $F_\varphi\colon X^1\longmapsto \{x\mid \varphi(X^1,x\}$. If $X^1$ appears only positively in $\varphi$, then $F_\varphi$ is a monotone operator, i.e. $X^1\subseteq Y^1\Rightarrow F_\varphi(X^1)\subseteq F_\varphi(Y^1)$. In this situation, as usual $F_\varphi$ has the least fixed point $L_\varphi$, i.e. $F_\varphi(L_\varphi)=L_\varphi$ and $\forall X^1(F_\varphi(X^1)\subseteq X^1\to L_\varphi\subseteq X^1)$. In fact we will be interested only in the case when $\varphi$ is a firstorder formula. And in order to construct $L_\varphi$ for firstorder $\varphi$ in secondorder logic, it is enough to use $\Pi^1_1$comprehension (here $\Pi^1_1$ formulas are formulas that start with a universal secondorder prenex followed by a firstorder formula).
Naturally this is generalized to joint positive inductive definitions of several predicates of arbitrary arities. Namely formulas $\varphi_1(X^{k_1}_1,\ldots,X^{k_n}_n,x_1,\ldots,x_{k_1})$, $\ldots$, $\varphi_n(X^{k_1}_1,\ldots,X^{k_n}_n,x_1,\ldots,x_{k_n})$ determine monotone operator $$F_{\vec{\varphi}}\colon \langle X^{k_1}_1,\ldots,X^{k_n}_n\rangle\longmapsto \langle \{\langle x_1,\ldots,x_{k_1}\rangle \mid \varphi_1( X^{k_1}_1,\ldots,X^{k_n}_n,x_1,\ldots,x_{k_1})\},\ldots\rangle.$$ And for it we have the least fixed point $L_{\vec{\varphi}}=\langle L_{\vec{\varphi},1},\ldots,L_{\vec{\varphi},n}\rangle$. Again, for firstorder $\varphi_i$'s $L_{\vec{\varphi}}$ could be constructed using $\Pi^1_1$comprehension.
In order to simplify consideration, I will formalize Dedekind infiniteness by a firstorder sentence $\mathsf{DInf}$ $$\forall x,y\;(f(x)\ne f(y))\land \exists x\forall y\;(f(y)\ne x)$$ in the signature with one unary symbol. Note that we could have considered secondorder axiom stating the existence of function $f$ with the desired properties (or binary predicate giving graph of $f$).
Consider the following interpretation of firstorder arithmetic with defined equality (i.e. individual natural numbers will be interpreted by equivalence classes of individual objects in secondorder logic). The idea is to represent $0$ by the equivalence class $U_0=\{x\mid \forall y\; (x\ne f(y))\}$, and represent $n+1$ by the equivalence class $U_{n+1}=\{x\mid \forall y\in U_{n}\;(x\ne f(y))\}$. Formally our interpretation will consist of secondorder formulas $(x=y)^*$, $(S(x)=y)^*$, $(x+y=z)^*$, $(xy=z)^*$ (the domain of interpretation is $\{x\mid (x=x)^*\}$). It is possible to define all this predicates by a joint positive inductive definition. It will be fairly long to give explicitly. The idea is to make the corresponding monotone operator to update partially defined equality and arithmetical operations, that are thought as covering only numbers up to $n$, to cover numbers up to $n+1$.
It is easy to see that $\Pi^1_1\mbox{}\mathsf{CA}+\mathsf{DInf}$ could construct this interpretation and in fact prove any instance of the scheme of firstorder induction for it, giving an interpretation of firstorder arithmetic $\mathsf{PA}$. But in fact here we got more than just firstorder Peano arithmetic, we interpret secondorder arithmetic with $\Pi^1_1$comprehension. More close examination of the argument shows that this interpretation will give firstorder Peano arithmetic even in $\Pi^0_\infty\mbox{}\mathsf{CA}+\Pi^1_1\mbox{}\mathsf{CA}^{\mathsf{pf}}+\mathsf{DInf}$ (here $\Pi^1_1\mbox{}\mathsf{CA}^{\mathsf{pf}}$ is parameterfree $\Pi^1_1$comprehension scheme and $\Pi^0_\infty\mbox{}\mathsf{CA}$ is the scheme of comprehension for firstorder formulas with secondorder parameters). My conjecture is that this should be best optimal in the sense that $\Pi^0_\infty\mbox{}\mathsf{CA}+\Pi^1_1\mbox{}\mathsf{CA}^{\mathsf{pf}}+\mathsf{DInf}$ proves precisely the same sentences of firstorder arithmetic as $\mathsf{PA}$ and that the two theories are equiconsistent over $\mathsf{PRA}$.