Is the consistency of classical third-order arithmetic provable in the logic of a topos with natural numbers?
(My guess would be yes, but I haven't seen this anywhere.)
Edit: in the original version I used the name PA$_3$ as an abbreviation for classical third-order arithmetic, and comments have followed suit, but I've since learnt that this name refers to a different theory (the classical theory of third order functions).
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}_n$ for each $n$, 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})$.
Supplemental: I initially claimed we can have a model of $\mathsf{PA}_\infty$, but Paul pointed out I was overstating the case. Indeed, to have a model of $\mathsf{PA}_\infty$ we would need a single object that encompasses all finite iterates $\neg\neg$-powersets ${P_{\neg\neg}}^k(\mathbb{N})$ at once, says something like $\coprod_{n \in \mathbb{N}} {P_{\neg\neg}}^k(\mathbb{N})$. However, in an elementary topos such an object need not exist. A counter-model is the set $V_{\omega + \omega}$ of sets of rank below $\omega + \omega$.
