Return to Question

Is the consistency of classical third-order arithmetic (PA$_3$) provable in the logic of a topos with natural numbers?

(My guess would be yes, but I haven't seen this anywhere.)

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

Is the consistency of classical third-order arithmetic (PA$_3$) provable in the logic of a topos with natural numbers?

(My guess would be yes, but I haven't seen this anywhere.)

Edit:

Topos-with-nno logic, together with Excluded Middle, is interpretable in Bounded Zermelo set theory, which is conservative over higher-order arithmetic (PA$_{\omega}$). At least that seems to be the case in light of this rather inconclusive thread. Thus topos-with-nno logic can't prove the consistency of PA$_{\omega}$ (even if Excluded Middle is added). The most one can hope for is that, for each $n \in \mathbb{N}$, it proves the consistency of PA$_{n+1}$. Here I'm following the annoying usual convention where PA $=$ PA$_1$.

Is the consistency of classical third-order arithmetic (PA$_3$) provable in the logic of a topos with natural numbers?

(My guess would be yes, but I haven't seen this anywhere.)

Is the consistency of classical third-order arithmetic (PA$_3$) provable in the logic of a topos with natural numbers?

(My guess would be yes, but I haven't seen this anywhere.)

Edit:

Topos-with-nno logic is interpretable in Bounded Zermelo set theory, which is conservative over higher-order arithmetic (PA$_{\omega}$). At least that is what I infer from this rather inconclusive thread. Thus topos-with-nno logic can't prove the consistency of PA$_{\omega}$. The most one can hope for is that, for each $n \in \mathbb{N}$, it proves the consistency of PA$_{n+1}$. Here I'm following the annoying usual convention where PA $=$ PA$_1$.

Is the consistency of classical third-order arithmetic (PA$_3$) provable in the logic of a topos with natural numbers?

(My guess would be yes, but I haven't seen this anywhere.)

Edit:

Topos-with-nno logic, together with Excluded Middle, is interpretable in Bounded Zermelo set theory, which is conservative over higher-order arithmetic (PA$_{\omega}$). At least that seems to be the case in light of this rather inconclusive thread. Thus topos-with-nno logic can't prove the consistency of PA$_{\omega}$ (even if Excluded Middle is added). The most one can hope for is that, for each $n \in \mathbb{N}$, it proves the consistency of PA$_{n+1}$. Here I'm following the annoying usual convention where PA $=$ PA$_1$.