Задача Колмогорова и пучки

В своей работе 1931г. Колмогоров предложил интерпретацию интуиционистской логики в терминах задач. Так, если $\alpha$ обозначает задачу "поделить любой заданный угол на 7 равных частей циркулем и линейкой", то отрицание $\neg\alpha$ можно понимать как задачу "показать, что предположение об осуществимости указанного построения ведёт к противоречию", а дизъюнкция $\alpha\lor\neg\alpha$ будет задачей "провести указанное построение либо доказать его невозможность". Соображение о том, что всякую задачу вида $\alpha\lor\neg\alpha$ в принципе должно быть возможно разрешить, "исходя из принципа исключённого третьего", не поможет студенту, которому эта задача досталась на экзамене (по теории Галуа). Поэтому принцип исключённого третьего, невыводимый в интуиционистской логике, к задачам не применим.
В комментарии к своему собранию сочинений 1985г. Колмогоров сообщил: "Работа [1931г.] писалась в надежде на то, что логика решения задач сделается со временем постоянным разделом курса логики. Предполагалось создание единого логического аппарата, имеющего дело с объектами двух типов - высказываниями и задачами." Целью доклада является построение указанного аппарата, соединяющего классическую и интуиционистскую логику, а также его модели, в которой высказываниям соответствуют подмножества фиксированного топологического пространства (по аналогии с диаграммами Венна), а задачам - пучки множеств на этом пространстве. По сравнению с классической и интуиционистской логикой в языке нового исчисления добавляются только два функтора между ними, которые устанавливают соответствие Галуа между частично упорядоченными множествами задач и высказываний, профакторизованных по эквивалентности и упорядоченных по импликации.