What do Freyd's toposes classify? (Q382418)

Although Freyd's toposes are very well known since they provide extremely elegant and `simple' models contradicting the Axiom of Choice, there is no explicit description of the geometric theories whose generic models they contain. This article aims at closing this gap in the knowledge about Freyd's toposes. The paper is quite technical, but the results may be of interest for anyone working on independence results, as the technique it presents provides a guideline that, at least in principle, may be extended to other cases. Summarising, Freyd observed that a Boolean Grothendieck topos \(\mathbb{B}\) may always be taken to be of the form \(\mathrm{Sh}(\mathbb{C}, \mathcal{D})\) where \(\mathbb{C}\) is a small category and \(\mathcal{D}\) is the Grothendieck topology generated by the double-negation local operator in the corresponding presheaf topos. That is, \(\mathcal{D}\) consists of all stably non-empty sieves. Also, Freyd observed that there is almost no loss of generality in taking the object of \(\mathbb{C}\) to be the natural numbers. Imposing (i) there exists \(n \to m\) in \(\mathbb{C}\) whenever \(n \geq m\); (ii) if \((f: n \to m) \circ k = (g: n \to m) \circ h\) in \(\mathbb{C}\), then \(f = g\); (iii) if \(f: n \to m\) and \(g: n \to m + 1\) in \(\mathbb{C}\), then there are \(h, k: n + 1 \to n\) such that \(f \circ h = f \circ k\) but \(g \circ h \not= g \circ k\); we get what is called a Freydian category. The toposes of sheaves over a Freydian category allow us to construct explicit countermodels to the Axiom of Choice in many different ways. On the other hand, any Grothendieck topos \(\mathrm{Sh}(\mathbb{C}, \mathcal{J})\) may be presented as the classifying topos of the geometric theory of flat \(\mathcal{J}\)-continuous functors on \(\mathbb{C}\) -- in a way, one may think of the topos as `being' that theory. However, the difficulty in explicating such a description in the case of Freydian toposes comes from \(\mathcal{D}\)-continuity. So, the author constructs a coverage \(\mathcal{J}\) contained in \(\mathcal{D}\) which is much simpler to be translated into an explicit geometric theory -- which is constructed in the last part of the paper -- and, of course, any model of the theory associated with \(\mathrm{Sh}(\mathbb{C},\mathcal{D})\) will also be a model of the theory classified by \(\mathrm{Sh}(\mathbb{C},\mathcal{J})\). The author also provides an interpretation of the resulting models for the theories so constructed in the form of coloured graphs, which makes clearer and more intuitive why the independence result follows. Specifically, any such model can be viewed as a counterexample to Bar induction, which explains why the theory has no models in \(\mathrm{Set}\), the standard category of sets where countable dependent choice is assumed. The result can be easily and evidently generalised, thus the theory has no models in any two-valued topos where countable dependent choice holds.