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


1 Answer 1


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

  • $\begingroup$ [Deleted earlier comment - I hadn't read your message carefully.] $\endgroup$ Oct 19, 2021 at 5:40
  • 2
    $\begingroup$ 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. $\endgroup$ Oct 19, 2021 at 6:23
  • 6
    $\begingroup$ 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. $\endgroup$ Oct 19, 2021 at 6:37
  • 1
    $\begingroup$ @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. $\endgroup$ Oct 23, 2021 at 20:14
  • 2
    $\begingroup$ @PeterLeFanuLumsdaine I've found a reference, Troelstra and van Dalen "Constructivism in Mathematics, an introduction", Volume 1, Chapter 3, Section 9.3. I should have searched before asking you! $\endgroup$ Oct 23, 2021 at 20:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.