Let $\Omega_{\neg\neg} = \{p \in \Omega \mid \neg\neg p \Rightarrow p\}$ be the object of $\neg\neg$-stable truth values, and let us write $P_{\neg\neg}(A) = {\Omega_{\neg\neg}}^A$ for the object of $\neg\neg$-stable subobjects of $A$. Observe that $\Omega_{\neg\neg}$ is a complete Boolean algebra, and this fact can be shown in the internal logic of a topos.

Now, it seems to me that one can build a model of $\mathsf{PA}_\infty$ by interpreting its logic in $\Omega_{\neg\neg}$, and the (higher-order) predicates as elements of the iterates of the $\neg\neg$-powersets ${P_{\neg\neg}}^k(\mathbb{N})$.