Room 327

The Muchnik topos

Sankha S. Basu

IIIT, Delhi

We study a model of intuitionistic higher-order logic which we call the
Muchnik topos. The Muchnik topos may be defined briefly as the category of
sheaves of sets over the topological space consisting of the Turing
degrees, where the Turing cones form a base for the topology. We note that
our Muchnik topos interpretation of intuitionistic mathematics is an
extension of the well known Kolmogorov/Muchnik interpretation of
intuitionistic propositional calculus via Muchnik degrees, i.e., mass
problems under weak reducibility. Within the Muchnik topos, we introduce a
new sheaf representation of the intuitionistic real numbers, the Muchnik
reals, which are different from the Cauchy reals and the Dedekind reals.