Программа интуиционизма

Программа интуиционизма, или интуиционизм — это одно из трёх главных направлений (наряду с логицизмом и формализмом), традиционно выделяемых в основаниях математики и логики (см. Логика), в основе которого лежит принцип математического построения. Основное отличие интуиционизма от других направлений в том, что он ставит иную цель математике: не доказательство «истинных» теорем, а поиск «интуитивно убедительных» и «наглядно-содержательных» математических («умственных», в терминологии первоначального интуиционизма) конструкций, органично соединяющих в себе построение и его обоснование; при этом построение является единственным средством обоснования в математике. Интуиционизм отвергает использование в математике и логике идеи актуальной бесконечности и взгляд на логику как на науку, «предшествующую» математике. Главным объектом интуиционистской критики стал широко используемый в классической математике и логике закон исключённого третьего (см. Закон исключённого третьего). Согласно интуиционизму, вся математика должна опираться на интуитивное представление ряда натуральных чисел и на принцип математической индукции, истолковываемый как требование действовать последовательно, шаг за шагом; допускаются лишь конструктивные доказательства существования рассматриваемого объекта, указывающие способ его построения. Представители интуиционизма полагают, что чистая математика является мыслительной активностью, не зависящей от языка, её объект — нелингвистические математические конструкции. Язык служит лишь для сообщения математических идей, математика не сводится к языку и тем более не может быть истолкована как особый язык. Предметом исследования (математической) логики является математический язык, более или менее адекватно передающий математические построения. Логика вторична по отношению к математике, последняя не может быть обоснована с помощью логических средств.

Предшественниками интуиционизма являются немецкий математик XIX века Л. Кронекер, французские эффективисты, А. Пуанкаре и Э. Борель. Они с разных позиций отмечали признаки неблагополучия в математике, связанные с тем, что в классической математике доказательства многих теорем существования не дают построений искомых объектов, и пытались несколько ограничить математические конструкции для устранения данного недостатка. Идеи интуиционизма в явном виде были сформулированы в начале XX века голландским учёным Л. Э. Я. Брауэром, который в 1907 году показал, что корни многих нежелательных свойств классической математики уходят в классическую логику и выдвинул программу радикальной перестройки математики, противопоставив её концепции сведéния математики к логике (программа логицизма — см. Логицизм) и истолкованию математики исключительно как языка математических символов (программа формализма — см. Формализм). Идеи Брауэра были развиты Г. Вейлем (Германия) и А. Гейтингом (Нидерланды). До 1945 года интуиционизм развивался преимущественно в Голландии, хотя некоторые фундаментальные работы были созданы в России, Австрии и Польше учёными, не причислявшими себя к данному направлению. Ныне самой сильной школой интуиционизма остаётся голландская, но, помимо неё, имеются, в частности, американская и русская школы. Для общей характеризации направлений, выросших из интуиционизма, часто пользуются термином конструктивизм (см. Конструктивизм математический). Поэтому следует различать интуиционизм в узком смысле (брауэровский), русский конструктивизм и различные частично конструктивные направления, часто также называемые современным интуиционизмом.

Основания для выводов Брауэра (с несколько модернизированной точки зрения) таковы. Согласно теореме К. Гёделя о неполноте, в достаточно богатой теории имеется такая формула G, что ни она, ни её отрицание недоказуемы. При помощи классической логики легко вывести: ∃x(G ⇒ x = 0) & (⌉G ⇒ x = l). Обозначим данную формулу ∃xA(x). Ни для какого конкретного x₀ нельзя доказать A(x₀). В теории множеств ситуация ухудшается лишь незначительно. Аксиома выбора даёт возможность построить такую доказуемую формулу ∃хВ(x), что нельзя построить формулу C(x), для которой ∃l xC(x) и ∀x(C(x) ⇒ B(x)). Такая же ситуация возникает при использовании альтернативы к аксиоме выбора — аксиомы детерминированности.

Согласно анализу А. А. Маркова, классическая математика базируется на трёх абстракциях: абстракции отождествления, не позволяющей использовать свойства, различающие равные объекты; абстракции потенциальной осуществимости, позволяющей пренебречь физическими ограничениями на реализуемость очень больших конечных объектов и процессов, и абстракции актуальной бесконечности, дающей возможность мыслить бесконечные совокупности как завершённые и использовать бесконечные множества и бесконечные процессы для построения других математических объектов. Брауэр принял две первые абстракции и отверг третью. В этом с ним солидарны почти все нынешние продолжатели конструктивных традиций в математике. В некоторых разделах современного интуиционизма это допущение ослабляется, а в некоторых — усиливается. Но в любом случае принимаются во внимание принципиальные ограничения выполнимых построений: необходимость сведéния любой новой задачи к уже решённым, чтобы представить новое построение как композицию старых.

При таком подходе логика не может рассматриваться как нечто данное a priori, она должна подбираться в соответствии с классом рассматриваемых объектов и с классом допустимых методов решения задач. Так, классическая логика оказывается либо логикой конечных объектов, либо логикой всех теоретико-множественных построений с аксиомой выбора. Сама интерпретация логических формул изменяется в корне. Значения истинности представляют собой нечто второстепенное по сравнению с конкретным построением, проведённым при доказательстве теоремы. Поэтому формулы интерпретируются как задачи, логические связки — как преобразования задач, методы доказательства — как методы сведéния новых задач к уже решённым либо принятым в качестве решённых. Брауэр предложил воспользоваться для перестройки математики логикой, подобной классической, за исключением законов исключённого третьего и снятия двойного отрицания (которые в данном контексте эквивалентны) — интуиционистской логикой (см. Логика интуиционистская). Он отказался от многих объектов, созданных в теоретико-множественной математике, и ограничился теми, которые хотя бы косвенно сводятся к двум исходным сущностям: к конструктивным объектам, строящимся как конечные конструкции из конечного числа исходных ясно различимых объектов, и к последовательностям выбора, представляющим из себя методы последовательного конструирования потенциально бесконечного числа исходных объектов. Примерами последовательностей выбора являются алгоритмы, последовательности измерений физических величин и так далее. Первоначально Брауэр пытался прямо перестроить основные разделы математики, при этом он, в частности, раньше, чем это было сделано классическими средствами, установил важный результат (теорема о веерах или лемма Кёнига): дерево с конечным ветвлением и конечными путями конечно. Перестройка математики, осуществлявшаяся Брауэром, отличалась максимальной осторожностью при соблюдении принципов конструктивности. Он стремился спасти всё, что можно было спасти. Примеры гораздо более жёстких подходов продемонстрировали Р. Л. Гудстейн и Н. А. Шанин.

Наиболее интересны следующие результаты Брауэра. Операторы над последовательностями выбора должны использовать конечное число значений последовательности для получения конечной выходной информации. На основе этого он доказал непрерывность интуиционистски определимых функций действительной переменной. Брауэр показал, что на самом деле в разных областях математики использовались разные понятия функции действительной переменной, в частности, что измеримые функции не стоит для конструктивных целей трактовать как операторы над действительными числами. Сразу же после формализации интуиционистской логики многие математики начали развивать вариации интуиционизма, либо ещё сильнее ограничивая логику, либо ещё сильнее ограничивая объекты. Йохансон предложил использовать в качестве основы для интуиционизма минимальную логику, но оказалось, что в любой теории, содержащей натуральные числа, интуиционистское отрицание определимо, и переход к минимальной логике ничего нового не даёт. Д. Грис предложил рассматривать безотрицательную математику, в которой запрещены пустые понятия типа квадратного круга. Продвижение в данном направлении идёт весьма медленно из-за необычности и трудности возникающих конструкций.

Новый импульс исследованиям в области интуиционистских понятий дали интерпретация интуиционистской логики А. Н. Колмогоровым и её (логики) формализация А. Гейтингом. На этой основе и на основе точного понятия алгоритма С. К. Клини (1945) дал первую точную классическую модель неклассической математики: понятие реализуемости. В интерпретации Клини стало возможным формально выразить тезис А. Чёрча как схему аксиом.

А. А. Марков (1947) и советская школа конструктивизма развили вариант математики, последовательно проводящий идею о том, что нет ничего, кроме конструктивных объектов, а алгоритмы отождествляются с их программами. Он ввёл «принцип Маркова», явно разделивший обоснования и построения, разница между которыми с самого начала ощущалась в интуиционизме. Содержательно принцип Маркова гласит, что для обоснования уже проделанных построений можно пользоваться классической логикой (это показал Н. А. Шанин, построив алгоритм конструктивной расшифровки, разбивающий любую формулу на явное построение и классическое обоснование данного построения). Польская школа пошла по другому пути, ограничиваясь конструктивными объектами, но сохраняя классическую логику.

Реализуемость выявила, что интуиционистские теории могут расходиться с классическими. Например, если A(x) — неразрешимое свойство натуральных чисел, то конструктивно верна формула — ∀x(A(x) ∨ ⌉A(x)). Зафиксировав понятие вычислимой последовательности, мы сохраняем свободу при определении операторов высших типов. Первым это показал Клини, построив общерекурсивную реализуемость, при которой выполнена схема: ∀x (⌉A(x) ⇒ ∃yВ (x, y)) ⇒ ∀x∃y(⌉A(x) ⇒ B(x, y)), выражающая всюду определённость всех функций. Возможность выразить формулами первого порядка те высказывания, для которых в классической логике требуются конструкции высших порядков — ещё одно преимущество интуиционизма. Принцип Маркова несовместим с данной схемой во всех содержательных интуиционистских теориях, хотя оба они являются классическими тавтологиями.

Э. Бишоп (1960), переопределив вычислимые функционалы, предложил вариант интуиционизма, который характеризуется принципом: «использовать лишь алгоритмы, но явно этого не говорить». Этот вариант, в дальнейшем развитый многими учёными, в том числе П. Мартин-Лёфом, соединил многие преимущества брауэровского и марковского подходов.

Сам Брауэр после появления реализуемости по Клини сосредоточился на примерах вычислимости, не подходящих под понятие алгоритма. В частности, он предложил следующие новые типы последовательностей — творческую последовательность α(n) = 0, если в году n не доказана формула A, и 1, если она доказана; и беззаконную последовательность, обладающую следующим свойством: ∀α(A(α) ∃n∀β(∀m(m < n ⇒ α(m) = β(m)) ⇒ A(β))), то есть всё, что мы о них знаем, мы знаем из уже полученной информации.

А. С. Трулстра (1974) доказал, что композиции алгоритмов и беззаконных последовательностей образуют интуиционистскую модель, в которой можно промоделировать творческие последовательности. Беззаконные последовательности явились первым примером позитивного использования незнания в точных науках. Возможность сформулировать незнание в виде логической формулы — ещё одно достижение интуиционизма.

С конца 1970-х годов развиваются идеи приложений интуиционизма к программированию, поскольку интуиционистские доказательства могут рассматриваться как полностью обоснованные программы. Как всегда, попытка лобового применения глубоких идеальных концепций оказалась неудачной. В таких случаях нужно искать обходные пути. Ими могут стать системы, основанные на более жёстких принципах, не принимающие абстракции потенциальной осуществимости и дающие построения при ограниченных ресурсах. Таковы линейные логики Ж.-И. Жирара, ультраинтуиционистские системы А. С. Есенина-Вольпина и С. Ю. Сазонова, нильпотентные логики Н. Н. Непейводы и А. П. Бельтюкова.

Голландская школа, наоборот, рассмотрела приложения интуиционистских понятий к теории множеств, расширяющие понятие эффективной операции, и получила ряд глубоких результатов. В частности, аксиома выбора интуиционистски становится почти безвредной, так что она концептуально противоречит закону исключённого третьего, а не эффективности построений. Интуиционистские теории возникают также при категорной интерпретации логики.

Интуиционизм, остро поставив вопросы оснований математики, способствовал развитию других направлений, в частности, формулировке программы Гилберта. Он выдвинул на первый план понятие построения, что способствовало повороту математики в сторону приложений. Он показал важность идеальных объектов при построениях, что обосновало неполноценность плоских прагматических и утилитаристских концепций и возможность рациональной альтернативы традиционному рационализму, что до сих пор как следует не использовано современной философией (см. Философия) и систематикой (см. Систематика).