is the NNO in a sheaf topos a model of classical PA?

Question

In their book Models for Smooth Infinitesimal Analysis Moerdijk and Reyes claim that the natural number object in any Grothendieck topos is a model of all classical provable statements of first order Peano arithmetic. Is this true? They do not provide a proof other than "do an induction on the formula". The semantic is the forcing semantic (equivalently the standard categorical semantic).

Answer 1

Yes.

In general, consider a Boolean topos $T$ and a topos $S$, and suppose we have a functor $F : T \to S$ which preserves finite limits and has a right adjoint (in other words, is the left part of a geometric morphism).

Even without the assumption that $T$ is Boolean, we see that $F$ is a coherent functor. This means that $F$ preserves finite limits, finite joins, and images. In other words, $F$ preserves the fragment of the internal logic consisting of $\top, \bot, \land, \lor$, $=$, and $\exists x \in A$. This is fairly easy to verify.

When we add in the assumption that $T$ is Boolean, it turns out that $F$ is also a Heyting functor. This means that $F$ also preserves the Heyting implication and dual images. So $F$ preserves the full $\Delta_0$ logic of $T$- that is, the full logic where we can quantify over elements.

Now, we may observe that given any cocomplete topos $S$, the functor $\Delta : Set \to S$ preserves finite limits and has a right adjoint - namely, the global sections functor $Hom(1, -)$. Recall that we may define $\Delta S = \coprod\limits_{s \in S} 1$.

In particular, note that $\Delta \mathbb{N}$ is the natural numbers object in $S$ (and of course the operations $0, 1, +, \cdot, succ$ are preserved by the functor). Therefore, for all sentences $\phi$ in the language of PA, if $\mathbb{N} \models \phi$ holds in the category of sets, then we also have $\Delta \mathbb{N} \models \phi$ in $S$. So in a sense, the arithmetic of $\mathbb{N}$ is absolute along the inclusion $\Delta : Set \to S$.

In fact, the left part of a geometric morphism must always preserve well-founded relations. This gives us a nice way of showing that $\Delta \mathbb{N}$ is the NNO. This is because an NNO can be axiomatised in the internal logic by the second-order Peano axioms (in Heyting arithmetic), which consist of first-order coherent axioms and the axiom that the relation $R = \{(x, succ(x)) \mid x \in \mathbb{N}\}$ is well-founded. All of these axioms are therefore preserved by $\Delta$ (even if $Set$ isn’t Boolean).

Finally, note the assumption of excluded middle for $Set$ is critical. For we could instead consider a model of constructive set theory in which Church’s thesis holds, which contradicts Peano arithmetic. But then we could take any Boolean Grothendieck topos $T$ (in particular, the double negation sheaves on $Set$ work nicely), and the functor $\Delta : Set \to T$ would be the left part of a geometric morphism but wouldn’t preserve $Set$’s arithmetic, since Peano arithmetic holds in $T$.