What does a proof in an internal logic actually look like?

Question

The nLab has a lot of nice things to say about how you can use the internal logic of various kinds of categories to prove interesting statements using more or less ordinary mathematical reasoning. However, I can't find a single example on the nLab of what such a proof actually looks like. (The nLab has a frustrating lack of examples in general.)

Can anyone supply me with some examples? I'd be particularly interested in the following kinds of examples:

• I've heard in a topos one can internalize the real numbers and, in the topos $\text{Sh}(X)$ of sheaves on a topological space, this reproduces the sheaf of continuous real-valued functions $X \to \mathbb{R}$. Moreover, one can internalize "finitely generated projective $\mathbb{R}$-module" and in $\text{Sh}(X)$ this reproduces real vector bundles on $X$. What can you prove about vector bundles this way?

• I'd also like to see examples of what you can do in the internal logic of Cartesian closed categories.

This MO question is related but it doesn't really satisfy my curiosity.

Answer 1

Here is an arbitrary example from algebraic geometry. We'll prove the following well-known statement about $\mathcal{O}_X$-modules on reduced schemes $X$ by reducing to constructive linear algebra interpreted in the topos $\mathrm{Sh}(X)$ of sheaves on $X$:

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

We can translate this statement into the internal language of $\mathrm{Sh}(X)$ by the following dictionary:

• In the internal language, the sheaf of rings $\mathcal{O}_X$ looks like an ordinary ring.
• Accordingly, $\mathcal{F}$ looks like an ordinary module on that ring.
• $\mathcal{F}$ is locally of finite type iff it is finitely generated from the internal point of view.
• $\mathcal{F}$ is locally free iff it is a free module from the internal point of view.
• Internally, we can define the rank of $\mathcal{F}$ as the minimal number of elements needed to generate $\mathcal{F}$. But constructively, the natural numbers may fail to have minima of arbitrary inhabited sets (see this enlightening blog post by Andrej Bauer), so this minimal number might not actually be an (internal) natural number, but be an element of a suitable completion. Externally, the rank defined this way induces a upper semicontinuous function on $X$ (see nLab and the Mulvey reference therein); it is constant iff internally, the minimal number of generators is an actual natural number.
• Finally, the scheme $X$ is reduced iff $\mathcal{O}_X$ looks like an ordinary reduced ring from the internal perspective. This in turn is equivalent to $\mathcal{O}_X$ being a so-called residue field from the internal point of view (i.e. a non-trivial ring with every non-unit being zero).

So the statement follows if we can give a constructive proof of the following linear algebra fact:

Let $A$ be a residue field and let $M$ be a finitely generated $A$-module. Then $A$ is free iff the minimal number of elements needed to generate $M$ as an $A$-module is an actual natural number.

The direction "$\Rightarrow$" is clear. For the direction "$\Leftarrow$", consider a minimal generating family $x_1,\ldots,x_n$ of $M$ (which exists by assumption). This family is linearly independent (and therefore a basis): Let $\sum_i \lambda_i x_i = 0$. If any $\lambda_i$ were invertible, the family $x_1,\ldots,x_{i-1},x_{i+1},\ldots,x_n$ would too generate $M$, contradicting the minimality. So each $\lambda_i$ is not invertible and thus zero (by assumption on $A$).

Answer 2

Joyal and Tierney's 1984 monograph, An extension of the Galois theory of Grothendieck, is an example of a substantial piece of mathematics written using informal reasoning in internal logic. The main result is the following:

Theorem. Every open surjection of toposes is an effective descent morphism. In particular, every Grothendieck topos is equivalent to the category of equivariant sheaves on a localic groupoid.

If you look at Chapter I, you will find that reads just like any other mathematical text, save for the avoidance of classical logic and certain kinds of set-theoretic operations. The main difficulty with using internal logic is the interpretation of the conclusions – this requires much care! For example, the proposition scheme $$(\forall b : B . \exists a : A . f(a) = b) \to (\forall h : B^T . \exists g : A^T . h = g \circ f)$$ where $B$ is fixed but $f : A \to B$ and $T$ are allowed to vary, says that "if $f$ is surjective, then for any $h : T \to B$, there exists $g : T \to B$ such that $h = g \circ f$", or in short, "$B$ is a projective object"... but in the canonical semantics, it is neither necessary nor sufficient that $B$ be projective for the statement to hold! That is because what the formula actually means is the following,

If $f : A \to B$ is an epimorphism, then $f^T : A^T \to B^T$ is also an epimorphism.

whereas $B$ being projective is the statement below:

If $f : A \to B$ is an epimorphism, then $\mathrm{Hom}(T, f) : \mathrm{Hom}(T, A) \to \mathrm{Hom}(T, B)$ is a split surjection of sets.

If the topos in question has a projective terminal object, then the first statement (internal projectivity) implies the second, and if the topos is well-pointed, then the second statement implies the first.

So much for projective objects. What about finitely generated modules? Again there are subtleties, but the most straightforward way to formulate it is to take a mixed approach. Let $R$ be an internal ring. Then $M$ is a finitely-generated $R$-module if there exist global elements $m_1, \ldots, m_n$ (i.e. morphisms $1 \to M$) such that $$\forall m : M . \exists r_1 : R . \cdots . \exists r_n : R . m = r_1 m_1 + \cdots + r_n m_n$$ holds in the internal logic. This amounts to saying that the evident homomorphism $R^{\oplus n} \to M$ is an epimorphism, which is what we want. It is tempting to formulate the whole statement internally, but this cannot work: at best one will obtain an internal characterisation of modules that are locally finitely generated.

---

Perhaps I should give a positive example. I'm afraid I can't think of anything interesting, so I'll opt for something simple instead. It is well-known that a two-sided unit element of a magma is unique if it exists. This is also true for internal magmas in any topos, and the proof is exactly the same (so long as it is formulated directly). More explicitly:

Let $M$ be a magma. Suppose $u$ is a left unit element in $M$ and $v$ is a right unit element in $M$. Then, $u = u v = v$.

Formally, we are deducing that $$\forall u : M. \forall v : M. (\forall m : M. u m = m) \land (\forall m : M. m v = m) \to (u = v)$$ which means that, for all $u : S \to M$ and $v : T \to M$, if $\mu \circ (u \times \mathrm{id}_M) = \pi_2$ and $\mu \circ (\mathrm{id}_M \times v) = \pi_1$, then $u \circ \pi_1 = v \circ \pi_2$ as morphisms $S \times T \to M$.

Now, suppose we have an internal magma $M$ for which $$\exists u : M . \forall m : M. (u m = m) \land (m u = m)$$ holds in the internal logic, i.e. there exists a morphism $u : T \to M$ satisfying the relevant equations, such that the unique morphism $T \to 1$ is an epimorphism. (The latter is the true content of the quantifier $\exists$.) We wish to show that $M$ has a global unit element, i.e. a morphism $e : 1 \to M$ satisfying the obvious equations. Applying the above result in the case $u = v$, we deduce that $u$ must factor through the coequaliser of $\pi_1, \pi_2 : T \times T \to T$. But this coequaliser computes the coimage of the unique morphism $T \to 1$, and we assumed $T \to 1$ is an epimorphism, so $T \to 1$ is itself the coequaliser of $\pi_1$ and $\pi_2$. Thus $u$ factors through $1$ (in a unique way), yielding the required $e : 1 \to M$.

Of course, the above paragraph takes place in the external logic, but this is unavoidable: there is no way to formulate the existence of a global element in the internal logic. I suppose the point is that, once you have built up a stock of these metatheorems that interpret statements in the internal logic, you can then prove various results using internal logic if so desired.

Answer 3

There are a number of examples in "Sketches of an elephant" by Johnstone, but two that stand out are D1.3.13 and D1.3.14, dealing with regular categories and their internal logic. The first shows that every cover is a coequalizer, and the second shows that the square formed by $A_1,A_2,A_1 \cap A_2$ and $A_1 \cup A_2$, along with their inclusions, is a pushout. The great thing about these two examples is that they are also proven earlier using categorical methods, in A1.3.4 and A1.4.3. This way you can see that the proofs with the internal language are much more familiar than the categorical way.

For vector bundles, the paper "A generalization of Swan's theorem" by Mulvey uses the internal language, if I remember correctly.

Also look at "Generic Galois theory of local rings" by Wraith, for examples related to the etale topos.

Answer 4

You can find examples in the work by Christopher Mulvey, for example

Intuitionistic algebra and representations of rings. In Recent advances in the representation theory of rings and C*-algebras. Mem. Amer. Math. Soc., 148, 3-57 (1974).

develops (essentially) topos theory and its internal logic from scratch and discusses the example of vector bundles.