Solution to Lawvere's first problem: a Grothendieck topos that has proper class many quotient topoi
Yuhi Kamio, Ryuya Hora
TL;DR
The paper resolves Lawvere's first open problem by constructing a Grothendieck topos with a proper class of quotient topoi, exemplified by the presheaf topos $\mathbf{PSh}(M_{\omega})$ on the countably generated free monoid. The strategy introduces the encoding topos $\mathcal{E}_{\mathcal{L}}$ and the classifying topos of inhabited objects $\mathbb{A}^{\circ}$, then reduces quotient-topoi considerations to rigidity phenomena via inhabited-topos-rigid objects and a pairing mechanism. A key component is the development of a length/minimal-expression theory for objects in the classifying topos $\textbf{A}$ and its inhabited subtopos $\textbf{A}^{\circ}$, enabling precise control over endomorphisms and projections. The main technical achievements are: (i) showing the existence of proper class many inhabited-topos-rigid objects in the encoding topos through a Relational-Structure framework, (ii) constructing a countable relational language $\mathcal{L}$ yielding proper class many non-isomorphic inhabited-lex-rigid $\mathcal{L}$-structures, and (iii) establishing a presheaf-encoding bridge in which $\mathcal{E}_{\mathcal{L}}$ is a quotient topos of $\mathbf{PSh}(M_{\omega})$ (and vice versa), thereby solving Lawvere's problem in a concrete setting with explicit encodings.
Abstract
This paper solves the first of the open problems in topos theory posted by William Lawvere, concerning the existence of a Grothendieck topos that has proper class many quotient topoi. This paper concretely constructs such Grothendieck topoi, including the presheaf topos on the free monoid generated by countably infinitely many elements PSh(M_ω). Utilizing the combinatorics of the classifying topos of the theory of inhabited objects and with the help of a system of pairing functions, the problem is reduced to a theorem of Vopenka, Pultr, and Hedrlin, which states that any set admits a rigid relational structure.
