zbMATH — the first resource for mathematics

What do Freyd’s toposes classify? (English) Zbl 1291.03121
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.
03G30 Categorical logic, topoi
03E25 Axiom of choice and related propositions
18B25 Topoi
Full Text: DOI
[1] Blass, A.R., Scedrov, A.: Freyd’s Models for the independence of the axiom of choice. Memoirs Am. Math. Soc. 404, (1989) · Zbl 0687.03031
[2] Fourman M.P.: Sheaf models for set theory. J. Pure Appl. Algebra. 19, 91–101 (1980) · Zbl 0446.03041 · doi:10.1016/0022-4049(80)90096-1
[3] Fourman, M.P., Hyland, J.M.E.: Sheaf models for analysis. In: Applications of Sheaves, Lecture Notes in Mathematics, vol. 753, pp. 280–301. Springer, Berlin (1979) · Zbl 0427.03028
[4] Freyd P.J.: The axiom of choice. J. Pure Appl. Algebra. 19, 103–125 (1980) · Zbl 0446.03042 · doi:10.1016/0022-4049(80)90097-3
[5] Johnstone, P.T.: Sketches of an Elephant: a Topos Theory Compendium. In: Oxford logic guides, vols. 1–2, pp. 44–45. Oxford University Press, Oxford (2002) · Zbl 1071.18001
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.