Major applications of the internal language of toposes

Question

What are the major applications of the internal language of toposes?

Here are a few applications I know:

• Mulvey's proof of the Serre–Swan theorem in which he interprets the intuitionistically valid result of Kaplansky that each finitely generated projective module over a local ring has a finite basis in sheaf toposes. See Mulvey's paper Intuitionistic Algebra and Representations of Rings.
• Blechschmidt's proof of Grothendieck's generic freeness lemma. See his PhD thesis.
• In Sheaves in Geometry and Logic, Mac Lane and Moerdijk use the internal language in the proof that the elementary theory of the category of sets and bounded Zermelo set theory with choice are equiconsistent.

Are there other big theorems in mathematics whose proofs use the internal language of toposes (or other types of categories like cartesian closed categories)?

Some people might object with my usage of "uses", since each proof using the internal language can mechanically be rewritten so that it doesn't use the internal language anymore (by unwinding the interpretation of the internal language). In this case I want to put the question as: are there other big theorems in mathematics whose proofs benefit (e.g., increase the chance readers will understand the proof) from presenting it using the internal language of toposes?

Let's create a list!

Answer 1

I don't know if this counts as an application of the internal language or as an avoidance of it, but I think it is worth listing anyway.

In the development of homological algebra and homotopy theory in a Grothendieck topos, there is a technique of reducing proofs to the classical case by either:

• assuming that there are enough points and taking stalks everywhere, or
• applying Barr's theorem and passing to a Grothendieck topos that (is boolean and) satisfies the (external) axiom of choice.

(I mention homological algebra and homotopy theory here because, if I recall correctly, the former strategy was used – in the first instance – in the foundations of those topics, before the development of "direct" proofs.)

The first strategy is completely rigorous and unobjectionable except perhaps for its lack of generality. Because it reduces questions of truth (of certain propositions preserved by geometric morphisms and reflected by surjective geometric morphisms) to literally what happens in $\textbf{Set}$, it is unnecessary to know how the original theorems are proved (in $\textbf{Set}$); it is enough to know that they are true. In a sense, this is an avoidance of reasoning in the internal language. Instances of this can be found in: Artin and Mazur [1969, Étale homotopy], Verdier [1972, SGA 4 Exposé V], Brown [1973, Abstract homotopy theory and generalized sheaf cohomology], ...

On the other hand, the only way I see of making rigorous the second strategy is to interpret it as an implicit claim that, for the theorems in question, there are classical proofs that can soundly interpreted not just in $\textbf{Set}$ but also any Grothendieck topos that satisfies the axiom of choice. In other words, classical theorems cannot be treated as black boxes for this strategy, and this is an implicit claim that it is possible to reason in the internal language (of a Grothendieck topos that satisfies the axiom of choice) the same way as in $\textbf{Set}$. Instances of this can be found in: Joyal [1984, Letter to Grothendieck], Jardine [1996, Boolean localization, in practice], ...

It is also possible to continue avoiding having to think about proofs, in the fashion of the first strategy, by being more careful about what structures one really needs preserved/reflected to transfer theorems. For example, van Osdol [1977, Simplicial homotopy in an exact category] extended Brown's theory from toposes of sheaves on topological spaces to exact categories (including all Grothendieck toposes), essentially by observing that because the definitions only involve finite limits and regular epimorphisms, it is enough to assume that there are enough exact functors to $\textbf{Set}$, but this is guaranteed by (another theorem of) Barr. In a sense, this is even more of an avoidance of reasoning in the internal language: the proper internal language of exact categories is much more restrictive than that of a topos, so a proof in the internal language would be much more constrained than a proof in classical mathematics. But I think this still demonstrates the benefit of formulating propositions using the internal language, even if one does not formulate proofs in it.

Answer 2

Your "list" would consist of the majority of the body of pure mathematics.

If you construct your objects (call them "sets" if you like) using

• "Cartesian" products (with pairing and projections),
• "subsets" carved out of an object by means of a predicate,
• powersets

then you are using the "internal" language of a topos.

Zermelo pretty much set this out in 1908. Unfortunately, he chose to use unordered pairs instead of ordered ones. I doubt whether he would have had strong opinions about this, had a time-traveller tapped him on the shoulder and suggested he modify his axioms.

There was an utterly redundant body of material in the undergraduate textbooks of my day that corrects this mistake, encoding ordered pairs and functions using lots of curly brackets. These provide what we now call product, coproduct and exponential, although they were very widely used mathematical constructions before universal properties were explicitly defined. Coproduct is disjoint union, whilst the "union" provided directly by Zermelo's axioms is useless and annoying.

Zermelo's problem was that he was doing this long before logic was written down in a common-sense way by Gentzen and the basic processes of algebra by Noether. Category theory and topos theory distill the essence of the decades of mathematical experience after Zermelo.

Yes, it is true that some constructions involve infinite limits or colimits of objects. What is generally required here is a more careful understanding of why you're doing the construction.

I am by no means saying that every argument in the traditional language is valid in a topos, because many arguments use the Axiom of Choice or Excluded Middle. However, that issue comes under a different heading, constructivity.

Despite having had a standard pure mathematical education (as it was in the 1980s), including all of the mythology of set theory, I honestly have no idea how to formulate mathematics "in the internal language of set theory".

There are many textbooks explaining the relationship between the vernacular language of mathematics and the categorical definition of a topos. For example mine, Practical Foundations of Mathematics and Introduction to Higher Order Categorical Logic by Jim Lambek and Phil Scott. Both of these were published by Cambridge University Press.

As to whether this "answers the question", we only have to re-read the single sentence of the question itself,

What are the major applications of the internal language of toposes?

This has a clear sub-text that it is exotic to use this language.

OK, it was, in the 1970s when it was when various people including Barry Mitchell Jean Bénabou and Gerhard Osius first did it. Peter Johnstone's first book (Topos Theory, 1977) makes it look exotic by printing variables in bold type. But the students of these people realised that they weren't writing in an "exotic" language, but the vernacular of pure mathematics.

It sends the wrong message to "ordinary" mathematicians (those that don't specialise in category theory) if we don't challenge the idea that "the language of a topos" is any different from the language that other mathematicians use.

As Mike Shulman points out below, many of the examples discussed on this page are about comparing the properties of different toposes, or transporting properties along, for example, inverse image functors.

Ingo Blechschmidt's thesis is remarkable, not for using "internal" lanaguages, but for choosing a particular topos, working in that and reproducing the results of algebraic geometry. This is in the tradition of Synthetic Differential Geometry, Synthetic Domain Theory, Synthetic Topology, Synthetic Metric Spaces and Synthetic Computability.

So there are several ways that this question could have been re-rewritten, without the mis-conception that the "internal" language is per sec exotic, to obtain lists of examples of these ideas.

By the way, we need to change this term "internal language". I propose "proper language" instead, where "proper" means "its own", cf propre in French.

You know what an "internal group" is, for example a topological group is an internal group in the category of topological spaces. It is easy to follow this pattern to say what an "internal category" is, or an "internal algebra" for whatever kind of algebra. The same also works for things that need to be expressed in more complex forms of logic.

Now, the term "language" has not been formally appropriated, but there are many ways that one might formalise the idea mathematically. Such a formalism could be interpreted "internally" in a topos or other suitable category.

The problem is that the customary term "internal language" is not an instance of this standard pattern of "internal gadgets" in a category.