Исчисление задач А.Н. Колмогорова и гомотопическая теория типов

А.Н. Колмогоров в 1932 г. предложил оригинальный вариант математического интуиционизма Л. Бауэра, в котором центральную роль играет различие задач и теорем, отличающихся по своему содержанию от интуиционизма А. Гейтинга и других последователей. У современных историков и логиков существуют разные мнения по вопросу о том, следует ли считать различие между задачами и теоремами у А.Н. Колмогорова логическим или же в интуиционистской интерпретации высказываний можно считать «проблемы» А.Н. Колмогорова просто альтернативным термином для теорем. В популярной ВНК-интерпретации интуиционистской логики, названной так по именам Л. Брауэра, А. Гейтинга и А.Н. Колмогорова, предлагается синтез подходов этих трех авторов, в котором различие между задачами выносится за пределы логики и трактуется как контекстуальное или чисто лингвистическое. В статье показывается, что различие между задачами и теоремами играет ключевую роль в подходе А.Н. Колмогорова, и приводится логическая интерпретация этого различия с использованием гомотопической теории типов (ГТТ). Используемое в этой теории понятие гомотопического уровня позволяет вслед за А.Н. Колмогоровым различать задачи, которые сводятся к доказательству утверждений, и задачи на реализацию конструкций более высоких уровней. Таким образом, ГТТ соотносится с точкой зрения А.Н. Колмогорова в его полемике с А. Гейтингом. В то же время в ГТТ не решается поставленная А.Н. Колмогоровым задача поиска конструктивного понятия отрицания, применимого к задачам общего вида, которая на сегодняшний день остается по-прежнему открытой.