| Intuitionism is a constructive approach to mathematics introduced in the early part of the twentieth century by L. E. J. Brouwer and formalized by his student A. Heyting. A. N. Kolmogorov, in 1932, gave a natural but non-rigorous interpretation of intuitionism as a calculus of problems. In this document, we present a rigorous implementation of Kolmogorov's ideas to higher-order intuitionistic logic using sheaves over the poset of Turing degrees with the topology of upward closed sets. This model is aptly named as the Muchnik topos, since the lattice of upward closed subsets of Turing degrees is isomorphic to the lattice of Muchnik degrees which were introduced in 1963 by A. A. Muchnik in an attempt to formalize the notion of a problem in Kolmogorov's calculus of problems. |
