A topos-theorist looks at dilators (Q1121978)

The concept of a dilator is central to the development of \(\Pi^ 1_ 2\)-logic, which was investigated extensively by \textit{J.-Y. Girard} [Ann. Math. Logic 21, 75-219 (1981; Zbl 0496.03037)]. In this clearly written and interesting article, the author indicates how dilators can be looked at topos theoretically. The reader with the necessary category theoretical background will find this description clear and helpful. The stage is set by looking at the category \(\underline{\text{Lord}}\) of linearly ordered sets and strictly order preserving mappings, its full subcategory \(\underline{\text{Word}}\) of well-ordered sets and also the subcategory \underbar{Ford} of finite orders. Following Girard, a dilator is a functor \(\underline{\text{Word}}\to\) Word which preserves pullbacks and filtered colimits. The author proceeds to show that in fact dilators live in the atomic topos \({\mathcal E}=sh(\underline{\text{Ford}}^{op})\), where \(\underline{\text{Ford}}^{op}\) is an atomic site with its canonical Grothendieck topology, where every non-empty sieve is a cover. \({\mathcal E}\) is the classifying topos for the theory of dense linear orders without end points. Dilators become a full subcategory of \(\underline{\text{Lord}}({\mathcal E})\), the category of linearly ordered objects in \({\mathcal E}\). The article proceeds to analyze linearly ordered objects in an atomic topos and applies these ideas to the specific case of \({\mathcal E}\), and some of Girard's results about dilators are derived in this topos theoretic framework.