Kolmogorov and Gödel's approach to intuitionistic logic: current developments
Sergei Nikolaevich Artemov · Russian Mathematical Surveys · 2004
Intuitionistic mathematics was created by Brouwer on the basis of constructive reasoning, where the existence of a proof was the criterion for truth. Kolmogorov and Godel proposed interpreting intuitionistic logic on the basis of classical notions of a problem's solution and of provability. In 1933 Godel made the first substantial step toward the building of such an interpretation. Despite much progress in the understanding of intuitionism, this task was not complete before the author's 1995 paper. This survey will cover the results of the past decade obtained within this framework.