A.N. Kolmogorov’s calculus of problems and homotopy type theory

In 1932 A.N. Kolmogorov proposed an original version of mathematical intuitionism where the distinction between problems and theorems plays a central role and which differs in its content from the versions of intuitionism developed by A. Heyting and other followers of L. Brouwer. In view of today’s historians and logicians, it remains a controversial point whether this distinction is to be treated as logical or Kolmogorov’s «problems» should be regarded as propositions, provided the latter term is interpreted intuitionistically. The popular BHK semantics of intuitionistic logic, so called after Brouwer, Heyting, and Kolmogorov and supposed to provide a synthesis of ideas of these authors, does not formally distinguish between problems and theorems and treats this distinction as contextual or purely linguistic. We argue that the distinction between problems and theorems is a crucial element of Kolmogorov’s approach and provide a logical interpretation of this distinction using homotopy type theory (HoTT). The notion of homotopy level of a given type in HoTT allows one to distinguish, after Kolmogorov, between problems reduced to proving a sentence and problems that require realization of higher-order constructions. Thus, HoTT provides a support for Kolmogorov’s view on intuitionistic logic in his polemics with Heyting. At the same time, HoTT does not solve the problem of finding a constructive notion of negation applicable to general problems, which is raised by Kolmogorov in the same paper and still remains open.