Lawvere-Tierney topologies for computability theorists

TL;DR

This paper introduces computable reduction games with imperfect information to characterize Lawvere-Tierney topologies on the effective topos, revealing structural properties and limitations of these topologies.

Contribution

It provides a concrete game-theoretic description of the lattice of Lawvere-Tierney topologies on the effective topos, extending previous work and exploring their structural properties.

Findings

No minimal Lawvere-Tierney topology strictly above the identity topology exists.

The paper offers a new game-theoretic framework for understanding topologies on the effective topos.

It generalizes notions of Turing and Weihrauch reductions within a unified setting.

Abstract

In this article, we introduce certain kinds of computable reduction games with imperfect information. One can view such a game as an extension of the notion of Turing reduction, and generalized Weihrauch reduction as well. Based on the work by Lee and van Oosten, we utilize these games for providing a concrete description of the lattice of the Lawvere-Tierney topologies on the effective topos (equivalently, the subtoposes of the effective topos preordered by geometric inclusion). As an application, for instance, we show that there exists no minimal Lawvere-Tierney topology which is strictly above the identity topology on the effective topos.