Internal logic of topoi

There is a distinction often made between the internal and external logic of topoi, for example in Goldblatt's book Topoi, or in the nLab. I have the impression that I understand the external logic of topoi, as a way to generalise set models of theories. Instead of interpreting a theory $T$ (operation symbols, relation symbols and axioms) in the category of sets, we try to interpret $T$ in another topos. This works better when the proofs we consider from $T$ are constructive, because the excluded middle principle is not valid in every topos. More potential models of $T$ give more ways of proving that $T$ is consistent. And if $P$ is a conjecture in the language of $T$, those extra models can also serve to prove the consistency of $T+\{P\}$ or $T+\{\lnot P\}$.

Goldblatt calls "external" this usage of topoi to make models of theories, and adds: "From the viewpoint that topoi offer a complete alternative to the category Set as a context for doing mathematics it is finally the internal structure that is important". This last claim is mysterious to me. In this other question, an example is given of lifting a traditional algebraic proof about $A$-modules into the internal language of the sheaf topos $Sh(X)$. So the internal logic would be a way to reinterpret proofs in different topoi, producing theorems for free. But that simply seems an application of the soundness theorem: for any proposition $P$ provable in the source theory $T$, the interpretation of $P$ in any model of $T$ will be true. And then we are back with the external logic of topoi.

Are there other applications of the internal logic of topoi, that would not be related to models of theories in topoi?

Solution 1:

Not having read Goldblatt, I am not exactly sure what he's getting at.

However, there is a concept which he might be addressing.

A lot of applications of internal logic go something like this:

We are given some sort of property $P$ about objects and morphisms in a topos. We then try to translate this property into some property $Q$ such that if $P$ holds in the external logic, then $Q$ holds in the internal logic.

We then prove in constructive logic that $Q \to R$, so we know that $Q \to R$ must hold in the internal logic by soundness.

Finally, we show that if $R$ holds in the internal logic, then $S$ holds in the external logic.

This gives us a complete proof that $P \to S$ in the external logic.

For example, take the lemma in the answer that you cited.

Let $\mathcal{F}$ be an $\mathcal{O}_X$-module locally of finite type. Then $\mathcal{F}$ is locally free iff its rank is constant.

Here, $X$ is a reduced scheme.

$P$ is the statement "$\mathcal{F}$ is an $\mathcal{O}_X$-module locally of finite type, and $X$ is a reduced scheme". The corresponding statement in the internal logic is $Q = $"$\mathcal{F}$ is a finitely generated $\mathcal{O}_X$-vector space, and $X$ is a field". Note that since we are working in constructive logic, it's critical to pick the right definition of "field", but we'll gloss over that little detail for now.

We then switch to "internal logic mode", put on our intuitionist hats, and prove in constructive logic the statement $Q \to R$, where $R$ is the statement "$\mathcal{F}$ is a free vector space if and only if there is some smallest $n \in \mathbb{N}$ such that $\mathcal{F}$ is generated by $n$ elements as a vector space".

Therefore, we know that $R$ holds in the internal logic. The fact that $R$ holds in the internal logic allows us to conclude statement $S$, which is "$\mathcal{F}$ is locally free iff its rank is constant".

More abstractly, we come up with a "global model" of the first-order sentence $Q$, which we then determine is also a global model of the first-order sentence $R$. We then interpret this in the external logic to get free theorems.

However, consider that models can also exist locally. In other words, we may have $\Vdash \exists M (M \models R)$ without there actually being a model of $R$ in the topos. This is different than coming up with a structure $M$ and then proving $\Vdash M \models R$. Note that this requires a form of the internal logic which can quantify over objects.

The interpretation of $\Vdash \exists M (M \models R)$ in the topos $E$ is that there is some epi $V \to 1$ and some structure $M$ in the topos $E / V$ such that in the internal logic of $E / V$, we have $\Vdash M \models R$.

So in other words, if we have a topos $E$ which believes that there is a model of $R$, we can find a nontrivial slice of $E$ for which there actually is a model of $R$.

This means that if we can prove the existence of a model of a formula in a nontrivial topos, we can come up with some other nontrivial topos where there actually is such a model.