Basic subtoposes of the effective topos (Q387125)

This article studies the lattice of local operators in M.~Hyland's \textit{effective topos}. Reminding that subtoposes of a topos \(\varepsilon\) are in 1-1 correspondence with local operators in \(\varepsilon\), and that local operators are some endomaps on the subobject classifier of \(\varepsilon\), since many variations on realizability arise as the internal logic of subtoposes of the effective topos, the motivation of the paper is clear: to provide instruments and insight on realizability models in toposes. The first technical contribution of the work is to show that every local operator is the internal join of a family of subsets of \(\mathbb{N}\) (Theorem~2.4 in the article). But the main innovation presented here is the technical notion of \textit{sight}, a tool by which it becomes viable to study inequalities between basic local operators. Sights are then used to present a concrete definition of truth for first-order arithmetic in subtoposes corresponding to local operators. The paper is very technical and the reader must be well acquainted with topos theory in general, and the construction and the properties of the effective topos in particular. Nevertheless, the conceptual width and depth of the paper is of interest for any researcher wishing to study realizability, and how it connects to topos theory, providing essential instruments to study effectiveness in a completely abstract way.