УДК: 1:51

DOI: https://doi.org/10.17072/2078-7898/2022-3-368-379

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

Родин Андрей Вячеславович
доктор философских наук, научный сотрудник

Русское общество истории и философии науки,
109240, Москва, Гончарная, 12/1;
e-mail: andrei@philomatica.org
ORCID: https://orcid.org/0000-0002-3541-8867
ResearcherID: N-1546-2013

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

Ключевые слова: исчисление задач, интуиционистская логика, гомотопическая теория типов, конструктивное отрицание.

Введение

Наследие Андрея Николаевича Колмогорова в области математической логики включает в себя всего две статьи [Колмогоров А.Н., 1925; Kolmogoroff A., 1932], опубликованные в довоенный период; к ним примыкает философская статья «Современные споры о природе математики» [Колмогоров А.Н., 1929], содержащая критический анализ текущих дебатов между сторонниками формализма Д. Гильберта и интуиционизма Л. Брауэра¹.

Вклад этих небольших по объему работ А.Н. Колмогорова в развитие математической и философской логики XX века является очень значительным. В статье «О принципе tertium non datur» [Колмогоров А.Н., 1925] А.Н. Колмогоров предложил исторически первую частичную аксиоматизацию интуиционистской логики высказываний [Troelstra A.S., 1990];   построенное в этой работе пропозициональное исчисление может быть охарактеризовано в современных терминах как  негативно-импликативный фрагмент минимального пропозиционального исчисления, предложенного в 1937 г. Иогансоном   [Плиско В.Е., 1988].   Фундаментальным результатом статьи А.Н. Колмогорова 1925 г. является интерпретация классической логики высказываний внутри данного фрагмента интуиционистской (минимальной) логики. Для построения этой интерпретации А.Н. Колмогоров сначала выделяет класс интуиционистских высказываний (формул), к которым применимо правило снятия двойного отрицания, т.е. таких высказываний A, для которых в исчислении А.Н. Колмогорова доказуема (т.е., выводима) формула ¬¬A→A. Как показывает А.Н. Колмогоров, если высказывания (формулы) A, B относятся к этому типу, то формулы А→B  и ¬A тоже относятся к этому типу, т.е. класс формул данного типа замкнут относительно импликации и отрицания. Отсюда следует, что если некоторая формула Ф доказуема (выводима) в классическом исчислении высказываний², в символах

├─_H Ф,

то интуиционистский аналог (перевод) формулы Ф, обозначаемый   Ф*, который получается с помощью замены всех атомарных подформул этой формулы на их двойные отрицания, выводится в интуиционистском исчислении А.Н. Колмогорова в символах

├─_Kolm Ф*.

Идея такого перевода в неформальном виде была впервые высказана еще Л. Брауэром и после публикации статьи А.Н. Колмогорова 1925 года получила дальнейшее развитие в работах Валерия Ивановича Гливенко, Герхарда Генцена и Курта Геделя [Atten M. van, 2022]. В современной теории топосов эта идея приобрела изящную геометрическую форму, которая позволила прояснить топологические характеристики классической и интуиционистской логики [MacLane S., Moerdijk I., 1994, ch. 6].

Как известно, в интуиционистской критике классических математических результатов включается аргумент о неправомерности применения закона исключенного третьего как универсального логического принципа без учета особенностей той предметной области, к которой относятся эти рассуждения [Хинчин А.Я., 1926]. Огрубляя, можно сказать, что с интуиционистской точки зрения подходы классической логики применимы только в тех областях математики, которые имеют дело с конечными совокупностями объектов и конечными процедурами³. Но, разумеется, интуиционисты не ставили и не ставят сегодня своей целью редуцировать всю математику к такого рода конечным случаям. Многие классические математические теоремы, доказываемые с помощью классических рассуждений, которые с интуиционистской точки зрения являются неприемлемыми (в частности, из-за неправомерного, с точки зрения интуиционистов, использования закона исключенного третьего), допускают интуиционистски приемлемые переформулировки, получаемые с помощью двойного отрицания. Например, теорема о существовании некоторого математического объекта x обладающего заданным свойством P, в символах

∃xPx,

которая в классической математике доказывается приведением к противоречию гипотезы о том, что такой объект не существует,  и допускает интуиционистскую переформулировку, согласно которой неверно, что все объекты рассматриваемого класса не обладают свойством P, в символах

¬∀x¬Px.

В качестве примера можно привести известную топологическую теорему Брауэра о существовании неподвижной точки для всякого непрерывного отображения замкнутого шара в себя, которая доказывается приведением к противоречию гипотезы о том, что такой точки не существует, т.е. все точки шара при действии данного преобразования переходят в какие-то другие точки.

Таким образом, описанной А.Н. Колмогоровым в статье 1925 г. интуиционистская интерпретация   классической логики и математики дает представление об интуиционистской математике как о расширении классической математики, а не как о ее ограничении только теми рассуждениями, в которых закон исключенного третьего применяется только по отношению к конечным совокупностям [Coquand T., 2007]. Впрочем, нужно иметь в виду, что такой прямолинейный перевод классических математических утверждений и их доказательств в интуиционистски приемлемую форму невозможно использовать во всех случаях, поскольку многие понятия классической математики с интуиционистской точки зрения просто не имеют смысла и наоборот. В частности, с интуиционистской точки зрения нужно, по-видимому, считать бессмысленной аксиому выбора (за исключением тех редких случаев, когда она имеет конструктивный смысл и по сути является излишней), а с классической точки зрения нужно признать математически некорректными или по меньшей мере нерелевантными используемые Брауэром понятия свободно становящейся последовательности и творческого субъекта. Оговоримся, что поскольку конкретное содержание «интуиционистской точки зрения» и «классической точки зрения» допускает много альтернативных вариантов, подобные утверждения описывают ситуацию в целом, но не могут претендовать на математическую строгость и окончательность. 

Если принять интуиционистский тезис о том, что классическая логика корректно отражает только формы правильных рассуждений о конечных совокупностях, то можно сделать вывод, что семантика интуиционистской логики должна включать в качестве частного случая классическую логическую семантику или, точнее говоря, скорректированную с интуиционистской точки зрения версию такой семантики. Таким образом, построение интуиционистской логической семантики на основе классической должно включать в себя два момента (которые не обязаны быть независимыми): интуиционистскую переформулировку классической логической семантики и расширение сферы применения логики за счет новых предметных областей, в которых общая интуиционистская логика применима, но ее классическая разновидность, допускающая возможность использования закона исключенного третьего, не применима.

Именно такого рода проект предлагает и частично осуществляет А.Н. Колмогоров в своей статье  «Об истолковании интуиционистской логики»⁴ [Колмогоров А.Н., 1985b], утверждая, что интуиционистская логика применима не только к допускающим истинностные оценки высказываниям и их доказательствам, но и к задачам более общего вида, включая традиционные геометрические задачи на построение, в которых с помощью ограниченных средств, обычно с помощью циркуля и линейки, требуется построить геометрическую фигуру с заданными свойствами.

Прежде чем говорить более подробно об исчислении задач А.Н. Колмогорова, предложенном в его статье 1932 г., сформулируем основной тезис настоящей работы и представим план дальнейшего изложения. В отличие от статьи А.Н. Колмогорова 1925 г., которая была опубликована на русском языке и долгое время оставалась неизвестной за пределами Советского Союза, статья 1932 г., написанная на немецком языке и опубликованная в одном из ведущих европейских математических журналов своего времени, была хорошо известна Аренду Гейтингу и другим ключевым исследователям в области интуиционистской логики того времени и оказала очевидное влияние на последующее развитие этой математической и философской дисциплины [Troelstra A.S., 1990].   Тем не менее, как будет видно далее, центральная идея этой статьи — идея формального различения задач на доказательство математических утверждений (теорем) и задач более общего вида, включая геометрические задачи на построение, — выпала из поля зрения большинства исследователей и до сих пор остается нереализованной в строгом математическом смысле. Постараемся показать, что эта идея остается важной и актуальной в контексте современных логических исследований, и рассмотрим некоторые известные на сегодняшний день подходы к ее реализации, которые были предложены в последние годы, по всей видимости, независимо от прямого влияния работ А.Н. Колмогорова. Это касается в первую очередь гомотопической теории типов (ГТТ), начало которой было положено во второй половине 2000-х гг. Владимиром Воеводским и которая продолжает быстро развиваться в настоящее время [Homotopy Type Theory…, 2013].  Затем мы более подробно рассмотрим понятие неразрешимой задачи по А.Н. Колмогорову и покажем, что адекватная формализация этого понятия до сих пор остается открытой проблемой.

Исчисление задач Колмогорова и BHK-семантика интуиционистской логики

Статья А.Н. Колмогорова «Zur Deutung der intuitionistischen Logik. Mathematische Zeitschrift» [Kolmogoroff A., 1932] состоит из двух частей. В первой части А.Н. Колмогоров показывает, что интуиционистское исчисление высказываний, предложенное Арендом Гейтингом в серии статей [Heyting A., 1930], может быть интерпретировано как исчисление задач: зафиксированные А. Гейтингом формальные правила конструктивных математических рассуждений применимы не только к доказательствам утверждений, но и к решениям задач более общего вида. Во второй части статьи, которая носит более философский характер, А.Н. Колмогоров утверждает, что интерпретация интуиционистской логики как логики задач более полно соответствует теоретико-познавательным принципам математического интуиционизма, нежели использованная А. Гейтингом интерпретация этой логики как логики высказываний.

Интересно, что в этой работе А.Н. Колмогоров ограничивается ссылкой на статью [Heyting A., 1930], но не ссылается на свою собственную работу [Колмогоров А.Н., 1925], которая содержит более раннюю попытку формализации конструктивных математических рассуждений. Это можно объяснить тем, что статья А.Н. Колмогорова 1932 г. была предназначена немецкоязычному научному сообществу, а статья 1925 г. была написана и опубликована на русском языке и оставалась недоступной для большинства немецкоязычных читателей. Важное отличие интуиционистского исчисления А.Н. Колмогорова 1925 г. от исчисления А. Гейтинга 1930 г. состоит в том, что исчисление А. Гейтинга использует классическое правило ex falso quodlibet (из лжи следует что угодно),  тогда как исчисление А.Н. Колмогорова не использует этого правила. Возможно, А. Гейтингу удалось убедить А.Н. Колмогорова в преимуществах своего исчисления или же А.Н. Колмогоров не считал это различие принципиальным.

Понятие задачи А.Н. Колмогоров не определяет, но иллюстрирует с помощью примеров, ссылаясь при этом на то, что базовые понятия классической логики, включая понятие высказывания, также не могут быть определены в терминах более простых логических понятий. Для целей настоящей работы достаточно рассмотреть первые два примера А.Н. Колмогорова: «(1) Найти такие четыре целые числа x, y, z, n, для которых выполняются соотношения   xⁿ + yⁿ = zⁿ, n > 2; (2) Доказать, что [Великая] теорема Ферма [ВТФ] неверна» [Колмогоров А.Н., 1985b, с. 142–143].

Как известно, утверждение ВТФ состоит в том, что четверки чисел, удовлетворяющих условию (1), не существует. Таким образом, решение задачи (1) влечет за собой решение задачи (2); другими словами, решение задачи (2) сводится к решению задачи (1). Однако обратное с интуиционистской точки зрения, которой в 1932 г. придерживается А.Н. Колмогоров, неверно. Если из утверждения ВТФ можно вывести противоречие, то это даст интуиционистски приемлемое решение задачи (2), т.е. интуиционистское доказательство отрицания ВТФ. Однако отрицание ВТФ с интуиционистской точки зрения не равносильно утверждению о существовании четверки натуральных чисел, удовлетворяющих условиям задачи (1). Таким образом, задачи (1) и (2) с этой точки зрения не тождественны и не эквивалентны.

Как замечает Вагнер Санз в статье, посвященной работе А.Н. Колмогорова 1932 г. [Sanz W., 2021], указание на решения задач при объяснении отношения сводимости между задачами является проблематичным, поскольку оно не учитывает случай, когда одна или обе находящиеся в этом отношении задачи не имеют решений. Этот случай А.Н. Колмогоров рассматривает отдельно; мы обсудим его более подробно в следующем разделе настоящей работы. Вслед за В. Санзом, мы будем говорить «задача В сводится к задаче А», имея в виду то, что если эти задачи имеют решения, то решение задачи А позволяет получить (может быть преобразовано в) решение задачи В.

Примеры (1) и (2) иллюстрируют следующий фундаментальный момент исчисления задач А.Н. Колмогорова: доказательство утверждения (высказывания, теоремы) представляет собой задачу специального вида, однако многие задачи, например (1), имеют другую форму, а их решения не являются доказательствами. Таким образом, понятие задачи (проблемы) с точки зрения А.Н. Колмогорова является более общим, чем понятие теоремы. В качестве классических примеров задач, которые не являются теоремами, можно привести традиционные задачи на геометрические построения циркулем и линейкой из «Начал» Евклида или любого современного учебника. Заметим, что формулировки этих задач не являются логическими пропозициями, т.е. не принимают истинностных оценок.

Стандартную на сегодняшний день  теоретико-доказательную семантику интуиционистской логики принято называть  BHK-семантикой (или BHK-интерпретацией) по первым буквам имен Л. Брауэра (Brouwer), А. Гейтинга (Heyting) и А.Н. Колмогорова^5,6.  Ниже представлена ее обычная формулировка [Atten M. van, 2022]:

• доказательство коньюнкции A ˄ B дается доказательством А и доказательством В;
• доказательство дизъюнкции A ˅ B дается доказательством А или доказательством В;
• доказательство импликации A → B — это конструктивная процедура, которая позволяет преобразовать всякое доказательство А в доказательство В;
• абсурд (противоречие) ┴ не имеет доказательства;
• доказательство отрицания ¬A — это конструктивная процедура, которая преобразует любое гипотетическое доказательство А в доказательство противоречия⁷ (перевод наш. — А.Р.).

По умолчанию  переменные А, В  обозначают здесь высказывания, к которым относятся соответствующие доказательства. Таким образом, данная обобщенная интерпретация не принимает во внимание соображение А.Н. Колмогорова о том, что задачи на доказательства высказываний представляют собой задачи специального вида, а также то, что интуиционистская логика допускает более широкую область применения.

Насколько это упущение является существенным? С точки зрения А. Гейтинга и его современных последователей (Пер Мартин-Леф, Марк ван-Аттен), ответ на этот вопрос отрицательный. По мнению этих авторов, интуитивистская точка зрения на математическое доказательство обнаруживает единство проблем (задач) и теорем, высказываний и построений (конструкций) и выносит различия между этими понятиями за пределы логики. Аргумент состоит в этом, что во всех подобных случаях речь идет о некоторой интенции, которая либо реализуется (удовлетворяется) в виде доказательства теоремы или решения проблемы, либо нет. Следуя этому подходу, П. Мартин-Леф при презентации ранней версии своей интуиционистской теории типов (ТТМЛ) перечисляет следующие возможные альтернативные интерпретации формальных типов и их термов:

• как множества и их элементы;
• как высказывания и их доказательства;
• как интенции (ожидания) и их реализации;
• как задачи и методы их решений [Martin-Lof P., 1984, p. 5].

Также автор обосновывает мнение, что понятия высказывания и множества по сути тождественны⁸.

Во второй половине 2000-х гг. В.А. Воеводским и его соавторами была предложена интерпретация ТТМЛ в терминах современной теории гомотопий, что послужило толчком к созданию гомотопической теории типов (ГТТ) и развитию программы построения унивалентных оснований математики [Homotopy Type Theory…, 2013]. При такой интерпретации стало возможным определить понятие гомотопической иерархии типов, в которой формально  различаются   пропозициональные типы (т.е. типы, интерпретируемые как высказывания), множество-подобные типы, группоидные типы и следующие в порядке иерархии другие высшие типы. Таким образом,  в ГТТ приводится математический аргумент в пользу точки зрения А.Н. Колмогорова, согласно которой различие между доказательствами высказываний и решением задач более общего вида имеет формальный логический характер, и против точки зрения А. Гейтинга (которой ранее также придерживался Мартин-Леф), согласно которой это различие является чисто лингвистическим и контекстуальным. Важно подчеркнуть, что структура гомотопической иерархии типов, позволяющая формально различать доказательства высказываний и решение проблем более общего вида, не была привнесена в ГТТ внешним образом на основании тех или иных философских соображений и предпочтений. Гомотопическая стратификация типов является объективным математическим свойством синтаксиса МЛТТ, которое никак не зависит от намеренной логической интерпретации этой теории. Эта неочевидная на первый взгляд синтаксическая структура стала доступной для математического описания и логического анализа благодаря открытой В.А. Воеводским гомотопической интерпретации данной формальной теории.

Неразрешимые задачи

Как подчеркивает А.Н. Колмогоров, «мы нигде не предполагали, что каждая задача разрешима. [...] Соответственно этому ¬A означает задачу “предположив, что решение задачи A дано, получить противоречие”» [Колмогоров А.Н., 1985b, с. 143]. Случай, когда поставленная задача не имеет решения, т.е. является неразрешимой, в понимании А.Н. Колмогорова подразумевает, что сам этот факт   математически доказан, т.е. решение задачи состоит в том, чтобы «доказать, что задача A не имеет решения». В противном случае нужно говорить не о неразрешимой, а о нерешенной (открытой) задаче. Нерешенные задачи А.Н. Колмогоров оставляет за рамками своей теории⁹.

В качестве стандартных примеров неразрешимых задач можно привести задачи квадратуры круга или трисекции угла с помощью циркуля и линейки. Эти задачи не имеют решений в обычном смысле, но поскольку сегодня сам факт этого является строго математически доказанным, то эти задачи нельзя считать открытыми и допускать возможность того, что они будут решены в будущем. Поэтому в более общем смысле эти задачи все же нужно считать на сегодняшний день решенными. В подобных случаях иногда говорят об «отрицательных решениях», называя обычные решения «положительными» [Sanz W., 2021].   Используя такую терминологию, нужно иметь в виду, что если понятие об обычном «положительном» решении задачи (как и само понятие задачи) является в теории А.Н. Колмогорова примитивным, т.е. неопределяемым, то понятие об «отрицательном» решении исчерпывающе определяется в терминах положительных решений, как это было сделано выше. Поэтому говорить о двух типах решений — положительных и отрицательных — в данном контексте можно только с большими оговорками.

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

Заметим, что при такой интерпретации отрицания задача вида ¬A в любом случае представляется задачей на доказательство утверждения независимо от того, относится ли к этому классу задач сама задача A. Это обстоятельство, на наш взгляд, идет вразрез с общей стратегией А.Н. Колмогорова считать задачи на доказательство утверждений задачами специального вида и развивать общую теорию задач и их решений, не опираясь на этот специальный случай. На то, что А.Н. Колмогоров сам не был удовлетворен тем понятием интуиционистского отрицания, которое он заимствовал у А. Гейтинга, указывает критика этого понятия, представленная во второй части статьи [Колмогоров А.Н., 1985b]. Как поясняет А.Н. Колмогоров, предложенное Л. Брауэром и использованное впоследствии А. Гейтингом понятие отрицания утверждения как возможности вывода из него противоречия является по сути неконструктивным, поскольку оно не включает в себя требования о предъявлении такого вывода в явном виде. Если же включить в понятие отрицания такое конструктивное требование, то, поскольку задача построения вывода противоречия может оказаться неразрешимой (как и любая другая задача), придется отказаться от обычного предположения о том, что для всякого осмысленного утверждения (задачи) А утверждение (задача) ¬A также является осмысленной. Как замечает А.Н. Колмогоров, такой шаг ставит под угрозу весь проект построения интуиционистской логики: если ограничиться в логике только такими утверждениями, отрицание которых заведомо имеет конструктивный смысл, то в такой логике будет выполняться правило исключенного третьего и в этом случае она совпадет с классической [Колмогоров А.Н., 1985b, с. 148]¹⁰. Однако А.Н. Колмогоров усматривает здесь также возможность для развития нового логического проекта, а именно проекта построения логики высказываний (задач), отрицание которых не имеет смысла. Мотивированные этой идеей логические исчисления были предложены впоследствии G.W.C. Griss [Griss G.W.C., 1948–1949] (по всей видимости независимо от А.Н. Колмогорова).

Вывод статьи А.Н. Колмогорова 1932 г. состоит в том, что «[р]ешение задач [в математике] должно рассматриваться как ее самостоятельная цель, наряду с доказательством теоретических высказываний» [Колмогоров А.Н., 1985b, с. 148]. Чтобы прокомментировать этот вывод, заметим вслед за А.Н. Колмогоровым, что доказательство ¬A — это не единственный способ доказательства неразрешимости задачи A: ¬A влечет за собой неразрешимость A, но обратное неверно [Колмогоров А.Н., 1985b, прим. 4]. Например, неразрешимость задачи трисекции угла циркулем и линейкой не влечет за собой утверждение о том, что гипотетическое решение этой задачи содержит противоречие. Это замечание сохраняет силу и для случая, который А.Н. Колмогоров специально не выделяет: когда A является утверждением. Действительно, возможна ситуация, когда утверждение A является (доказуемо) недоказуемым, и утверждение ¬A также является (доказуемо) недоказуемым. Существование таких утверждений в формальной арифметике было доказано в 1931 г. Куртом Геделем и соответствующее утверждение известно сегодня как первая теорема о неполноте.

Вопрос о том, был ли А.Н. Колмогоров знаком с результатами К. Геделя при подготовке своей статьи 1932 г. и принимал ли их во внимание,   требует отдельного исследования; мы не располагаем свидетельствами в пользу этой гипотезы или против этой гипотезы. Однако, на наш взгляд, такая историческая гипотеза в любом случае является излишней для объяснения позиции А.Н. Колмогорова, для которого синтаксическая неполнота построенного им исчисления задач (на основе формализованной интуиционистской логики А. Гейтинга) была сама собой разумеющейся.

Действительно, допустим, что нам удалось построить формальное исчисление задач, обладающее свойством синтаксической полноты относительно стандартного интуиционистского отрицания; в таком исчислении любая задача A либо разрешима, либо отрицание этой задачи ¬A разрешимо, причем всякий раз реализуется ровно одна из этих двух возможностей¹¹. В рамках такого исчисления для любого непротиворечивого набора условий можно без всяких дополнительных усилий предполагать существование объектов и конструкций, которые удовлетворяют этим условиям. С точки зрения Д. Гильберта и развитого им аксиоматического подхода, такой способ математических рассуждений является совершенно корректным. Однако с интуиционистской (конструктивной) точки зрения, которой придерживается А.Н. Колмогоров в статье 1932 г., дело обстоит совершенно иначе. Трисекция произвольного угла циркулем и линейкой невозможна не потому, что понятие о разделенном на три равные части угле содержит противоречие, а потому, что циркуля и линейки для решения данной задачи недостаточно. Напомним еще раз замечание А.Н. Колмогорова о том, что неразрешимость данной задачи A не влечет за собой разрешимость задачи ¬A [Колмогоров А.Н., 1985b, прим. 4]. В гипотетическом исчислении задач, обладающих свойством синтаксической полноты относительно отрицания, для такого рода конструктивной неразрешимости нет места¹².

Из этих соображений понятно, почему А.Н. Колмогоров не стремился к построению синтаксически полного (относительно стандартного интуиционистского отрицания) исчисления задач. Напомним, что интуиционистское исчисление А. Гейтинга, которое использовал А.Н. Колмогоров, этим свойством не обладает. Вопрос о семантической полноте построенного исчисления А.Н. Колмогоров в статье 1932 г. в явном виде не ставил, да и не мог строго поставить, сохраняя принятый в этой работе неформальный стиль изложения. Современную попытку формализации задачной семантики и доказательство корректности и полноты исчисления относительно этой семантики А.Н. Колмогорова можно найти в работе W. Sanz [Sanz W., 2021].

Заключение

Можно с уверенностью утверждать, что построенное на основе интуиционистской логики А. Гейтинга исчисление задач А.Н. Колмогоров не считал окончательным результатом развития своей идеи о расширении сферы логики на задачи общего вида¹³.   В частности, он не был удовлетворен тем интуиционистским понятием отрицания, которым он пользовался вслед за А. Гейтингом, и которое сегодня является общепринятым. Критика этого понятия в статье А.Н. Колмогорова 1932 г. до сих пор остается актуальной и   позволяет считать вопрос о конструктивном отрицании по-прежнему открытым. Раннюю попытку решить (или, во всяком случае, обойти) эту проблему можно увидеть в работе А. Гейтинга в области интуиционистской геометрии, в которой используется примитивное понятие различимости точек вместо обычного определения различия как отрицания  тождества [Dalen D. van, 1990]. Работы [Odintsov S.P., 2008] и [Agudelo-Agudelo L.S., Sicard-Ramirez A., 2022] представляют собой примеры современных попыток введения нового конструктивного понятия отрицания  в рамках паранепротивречивой логики. Хотя в ГТТ и поддерживается различие между утверждениями и задачами более общего вида в духе А.Н. Колмогорова, используется при этом обычное для конструктивной математики понятие отрицания как сведение к противоречию.  Действительно, в рамках ГТТ нет другого способа доказать, что данная задача неразрешима (т.е. некоторая конструкция уровня множеств или выше нереализуема) кроме как доказать, что соответствующий тип пуст. Пустой тип в согласии с определением гомотопической иерархии типов интерпретируется в ГТТ как (ложное) высказывание¹⁴. Поэтому мы не можем утверждать, что на сегодняшний день в ГТТ полностью реализуются высказанные А.Н. Колмогоровым в 1932 г. логические идеи.

Критика А.Н. Колмогоровым стандартного понятия интуиционистского отрицания как сведения к противоречию указывает на замысел автора ограничить область применимости этого понятия высказываниями и дополнить исчисление задач новыми конструктивными средствами доказательства неразрешимости. Эта задача остается на сегодняшний день нерешенной. Ее решение было бы не только важным с теоретической точки зрения, но и имело бы большое прикладное значение для разработки систем представления знаний и других систем искусственного интеллекта, использующих логические подходы.

Выражение признательности

Автор благодарит Марка ван Аттена (Mark van Atten), Олега Доманова и Георгия Шабата за ценные советы и обсуждение при подготовке этой статьи.

Работа выполнена в рамках проекта РНФ «Эпистемология цифрового представления знаний: эмпирические гипотезы, формальные доказательства и человеческое понимание», грант 22-28-01420.

Список литературы

Колмогоров А.Н. О принципе tertium non datur // Математический сборник. 1925. Т. 32, вып. 4. С. 646–667.

Колмогоров А.Н. Современные споры о природе математики // Научное слово. 1929. Вып. 6. С. 41–54.

Колмогоров А.Н. К работам по интуиционистской логике // Колмогоров А.Н. Избр. труды. Кн. 1: Математика и механика / отв. ред. С.М. Никольский. М.: Наука, 1985. С. 393.

Колмогоров А.Н. К толкованию интуиционистской логики / пер. с нем. В.А. Успенского // Колмогоров А.Н. Избр. труды. Кн. 1: Математика и механика / отв. ред. С.М. Никольский. М.: Наука, 1985. С. 142–149.

Плиско В.Е. Исчисление А.Н. Колмогорова как фрагмент минимального исчисления // Успехи математических наук. 1988. Т. 43, вып. 6(264). С. 79–91.

Хинчин А.Я. Идеи интуиционизма и борьба за предмет в современной математике // Вестник коммунистической академии. 1926. Кн. 16. С. 184–192.

Agudelo-Agudelo J.S., Sicard-Ramirez A. Type Theory with Opposite Types: A Paraconsisted Type Theory // Logic Journal of IgPL. 2022. Vol. 30, iss. 5. P. 777–806. DOI: https://doi.org/10.1093/jigpal/jzab022

Atten M. van. The Development of Intuitionistic Logic // The Stanford Encyclopedia of Philosophy / ed. by E.N. Zalta. 2022. URL: https://plato.stanford.edu/entries/intuitionistic-logic-development/ (accwssed: 22.07.2022).

Coquand T. Kolmogorov’s Contribution to Intuitionistic Logic // Kolmogorov’s Heritage in Mathematics / ed. by E. Charpentier, A. Lesne, N.K. Nikolski. Berlin: Springer, 2007. P. 19–40. DOI: https://doi.org/10.1007/978-3-540-36351-4_2

Dalen M. van. Heyting and Intuitionistic Geometry // Mathematical Logic / ed. by P.P. Petkov. N.Y.: Plenuv Press, 1990. P. 19–27. DOI: https://doi.org/10.1007/978-1-4613-0609-2_2

Griss G.W.C. Sur la Négation (dans les mathématiques et la logique) // Synthese. 1948–1949. Vol. 7, iss. 1–2. P. 71–74.

Heyting A. Die formalen Regeln der intuitionistische Logik // Sitzungsberichte der Preussischen Academie der Wissenshaften. Berlin: Verlag der Akademie der Wissenschaften, 1930. S. 43–56 (I), S. 57–71 (II), S. 158–169 (III).

Homotopy Type Theory: Univalent Foundations of Mathematics. Princeton, NJ: The Univalent Foundations Program: Institute for Advanced Study, 2013. 480 p.

Kolmogoroff A. Zur Deutung der intuitionistischen Logik // Mathematische Zeitschrift. 1932. Bd. 35, ht. 1. S. 58–65. DOI: https://doi.org/10.1007/bf01186549

MacLane S., Moerdijk I. Sheaves in Geometry and Logic. N.Y.: Springer, 1994. 642 p. DOI: https://doi.org/10.1007/978-1-4612-0927-0

Martin-Lof P. Intuitionistic Type Theory. Napoli, IT: Bibliopolis, 1984. 91 p.

Odintsov S.P. Constructive Negations and Paraconsistency. Dordrecht, NL: Springer, 2008. 248 p. DOI: https://doi.org/10.1007/978-1-4020-6867-6

Sanz W. Kolmogorov and the General Theory of Problems // Festschrift for Peter Heister-Schroeder. 2021. URL: https://www.researchgate.net/publication/349517286_Kolmogorov_and_The_General_Theory_of_Problems?channel=doi&linkId=60345796a6fdcc37a846345e&showFulltext=true (accessed: 22.05.2022). DOI: https://doi.org/10.13140/RG.2.2.31753.16488

Troelstra A.S. On the Early History of Intuitionistic Logic // Mathematical Logic / ed. by P.P. Petkov. N.Y.: Plenuv Press, 1990. P. 3–17. DOI: https://doi.org/10.1007/978-1-4613-0609-2_1

 

Получена: 01.08.2022. Принята к публикации: 18.08.2022

 

Просьба ссылаться на эту статью в русскоязычных источниках следующим образом:

Родин А.В. Исчисление задач А.Н. Колмогорова и гомотопическая теория типов // Вестник Пермского университета. Философия. Психология. Социология. 2022. Вып. 3. С. 368–379. DOI: https://doi.org/10.17072/2078-7898/2022-3-368-379

1 См. также близкую по своей тематике и опубликованную в те же годы философскую работу коллеги и соавтора А.Н. Колмогорова Александра Яковлевича Хинчина «Идеи интуиционизма и борьба за предмет в современной математике» [Хинчин А.Я., 1926].

2 А.Н. Колмогоров пользуется здесь классическим исчислением высказываний, ранее предложенным Д. Гильбертом.

3 В такой словесной формулировке данное условие не является вполне четким и допускает множество альтернативных уточнений, анализ которых выходит за рамки настоящей работы.

4 Оригинальное название статьи, опубликованной на немецком языке, «Zum Deutung der Intuitionistischen Logik». Использованный В.А. Успенским русский перевод статьи А.Н. Колмогорова «Об интерпретации интуиционистской логики» вслед за принятым английским переводом этой работы смягчает исходную формулировку названия, которое говорит скорее о «настоящем смысле» интуиционистской логики, а не просто о ее возможной интерпретации. Об этом можно судить на основании авторской формулировки основного тезиса этой статьи: «[И]нтуиционистская логика [...] должна быть заменена исчислением задач, поскольку ее объекты суть в действительности не теоретические высказывания, а напротив, задачи» (выделено нами. — А.Р.) [Колмогоров А.Н., 1985b, с. 142]. Здесь и далее в основном тексте статьи указанная работа А.Н. Колмогорова цитируется по русскому переводу Успенского 1985 г.

5 Впервые эта аббревиатура была использована Троелстрой в 1997 г., причем буква К первоначально указывала на имя Г. Крейзеля, а не на А.Н. Колмогорова [Van Atten M., 2022].

6 Поскольку интуиционистское (и, говоря шире, конструктивное) направление в логике оспаривает принятые в классической логике основные логические принципы и понятия, включая стандартное различие между синтаксисом и семантикой, терминология в этой области не является на сегодняшний день вполне устойчивой. Существует точка зрения, согласно которой выражения «BHK-семантика» и «BHK-интерпретация» являются некорректными и уместнее говорить об «объяснении значения» (meaning explanation) логических констант в стиле BHK или теоретико-доказательном объяснении значения. Хотя за этими терминологическими спорами в ряде случаев стоят важные философские аргументы, мы оставляем их здесь в стороне и используем все указанные выражения как взаимозаменяемые.

7 Обратим внимание на спорный характер семантики отрицания в стандартной формулировке BHK-семантики. Что такое «гипотетическое доказательство» и как оно может быть преобразовано в «доказательство противоречия», если противоречие не допускает доказательства? Синтаксически здесь речь идет, конечно, о выводе из высказывания A пары высказываний вида B, ¬B, т.е. о выводе формального противоречия. Однако это синтаксическое указание само по себе ничего не говорит о теоретико-доказательной семантике отрицания. Это замечание предваряет наш анализ критики интуиционистского отрицания А.Н. Колмогоровым в следующем разделе настоящей работы.

8 «Если принять всерьез идею о том, что высказывание определяется способом формирования своих канонических доказательств, а множество определяется способом формирования своих канонических элементов, то становится ясным, что различение этих понятий (а также связанных с ними понятий доказательства высказывания и элемента множеств) приводит только к ненужному удвоению [терминологии]. Вместо этого мы их просто отождествляем и рассматриваем в качестве одного и того же понятия» (перевод наш. — А.Р.) [Martin-Lof P., 1984, p. 13].

9 В статье 1932 г. А.Н. Колмогоров последовательно опирается на интуиционистское понимание истинности утверждения как возможности предъявить его доказательство. Но, в отличие от Брауэра, А.Н. Колмогоров избегает отсылок к состоянию знаний познающего субъекта в данный момент реального времени и поэтому выносит нерешенные задачи за пределы области применимости своего логического исчисления. Таким образом, тот вариант математического интуиционизма, который А.Н. Колмогоров развивает в этой статье, лишен элементов субъективизма, которые есть в интуиционизме Брауэра. Ср. со статьей [Kolmogoroff A., 1932, с. 148], где А.Н. Колмогоров анализирует понятие утверждения о существовании (экзистенционального высказывания) у Брауэра и выделяет в нем «объективный элемент» и «субъективный элемент».

10 А.Н. Колмогоров не приводит в статье оснований для этого вывода. Попробуем их реконструировать. Сначала заметим, что общее утверждение об осмысленности (содержательности) формулы ¬A в предположении об осмысленности формулы А в рамках данного логического исчисления является мета-теоретическим и, таким образом, не может имплицировать валидность какого-либо формального правила внутри данного исчисления. По всей видимости, А.Н. Колмогоров имеет в виду следующий семантический аргумент: данное мета-теоретическое свойство логического исчисления имеет место только в том случае, если область применимости этого исчисления ограничена рассуждениями о конечных совокупностях. Но в таких случаях выполняется и правило исключенного третьего (в его интуиционистской формулировке). Правило исключенного третьего А.Н. Колмогоров интерпретирует как задачу, которая состоит в том, что требуется предъявить общий метод, который для любой задачи А позволяет либо решить эту задачу, либо вывести противоречие из предположения о том, что такое решение существует. Как иронически замечает А.Н. Колмогоров, «[е]сли наш читатель не считает себя всезнающим, то он, пожалуй, согласится, что [правило исключенного третьего] не может находиться в списке решенных им задач» [Kolmogoroff A., 1932, p. 146]. Однако для задач о конечных совокупностях такой общий метод есть: это прямой перебор всех случаев.

11 Еще раз подчеркнем, что мета-теоретическое свойство синтаксической полноты данного исчисления задач не указывает непосредственно на использование правила исключенного третьего в этом исчислении.

12 Конечно, невозможность трисекции угла циркулем и линейкой может быть доказана сведением к противоречию предположения о том, что такое построение осуществимо. Однако такой способ доказательства неразрешимости этой задачи не является конструктивным в том смысле этого слова, который имеет в виду А.Н. Колмогоров, говоря о неконструктивном характере стандартного интуиционистского отрицания.

13 Об этом А.Н. Колмогоров говорит совершенно определенно в комментарии  к своей статье 1932 г., сделанном десятилетия спустя при подготовке первого тома собрания его сочинений: «Предполагалось создание единого логического аппарата, имеющего дело с объектами двух типов — высказываниями и задачами» [Колмогоров А.Н., 1985a].

14 Согласно этому определению, тип является пропозициональным, если он содержит максимум один элемент. Поэтому в ГТТ существует только два пропозициональных типа (с точностью до гомотопической эквивалентности): пустой тип и тип, содержащий единственный элемент, который в геометрических контекстах иногда называют «точкой». Эти два пропозициональных типа можно интерпретировать как привычные истинностные значения, как ложь и истину соответственно. Множество-подобные типы и другие высшие типы редуцируются к пропозициональным типам посредством специальной процедуры, которую в ГТТ (по геометрическим соображениям) называют обрезанием (англ. truncation) [Homotopy Type Theory…, 2013, p. 117]. Эта процедура может быть неформально описана как внешнее отождествление всех термов данного высшего типа. В согласии с исходной теоретико-доказательной семантикой ТТМЛ об этих термах можно думать как о различных доказательствах высказывания, которое получается в результате пропозиционального обрезания данного высшего типа; в результате этой процедуры все различия между такими «доказательствами» стираются и все соответствующие термы сливаются в единственное истинностное значение. Однако, как и в других подобных случаях, такое семантическое рассуждение опирается на случай истинного высказывания, не отвечая на поставленные А.Н. Колмогоровым вопросы по поводу интуиционистского понятия отрицания. Применительно к ГТТ вопрос можно сформулировать так: как интерпретировать процедуру обрезания в том случае, когда получающийся в результате этой процедуры пропозициональный тип пуст?