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).



Consistency proof in topos logic
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$.


