# Consistency proof in topos logic

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$$.
• Great answer, Andrej, but I think you slightly overstated. What this shows is that, for each $n \in \nats$, topos-with-nno logic can build a model of PA$_{n+1}$. I've edited my question to make this clearer. Oct 19, 2021 at 6:23
• Another way to see this answer is: $HOL_N$ (classical higher-order logic with NNO; the logic of a Boolean topos with NMO) clearly proves the consistency of each $PA_n$. But $HOL_N$ translates into $IHOL_N$ via the double-negation translation. Oct 19, 2021 at 6:37
• @PaulBlainLevy: off the top of my head, I’m not sure of a reference that gives it syntactically — my first hope was Lambek & Scott, but I can’t find it there. Mac Lane and Moerdijk Theorem VI.1.3 shows that “in any topos, the subtopos of $\lnot \lnot$-sheaves is Boolean”, which directly implies the syntactic translation. Oct 23, 2021 at 20:14