К необходимости рассмотрения алгоритмов приводит конструктивная трактовка экзистенциональных утверждений. Утверждение о существовании конструктивного объекта с данным свойством, то есть утверждение вида $ х А (х), в соответствии с представлениями о конструктивных объектах как результат конструктивных процессов считается в конструктивной математике установленным в том случае, когда указан потенциально выполнимый конструктивный объект, заканчивающийся построением искомого объекта. Соответственно установление параметрического утверждения существования " х $ у А (х, у) («для всякого х существует у такой, что А (х, у)» ) предполагает указание «общего» конструктивного процесса, начинающегося с произвольного конструктивного объекта х данного исходного типа и заканчивающегося построением искомого у. Другими словами, " х $ у А(х, у) выражает существование алгоритма, находящего у, исходя из х.. Из такой трактовки существования вытекает и конструктивное понимание дизъюнкции: суждение « А или В» считается установленным, только если предъявлен конструктивный процесс, заканчивающийся указанием его верного члена. Дальнейшее разъяснение смысла суждений более сложной структуры и выработки правил обращения с ними, соответствующих исходным конструктивным установкам, составляет задачу конструктивной семантики и конструктивной логики. Приведенная конструктивная трактовка утверждений существования и дизъюнкции существенно отличается от традиционной: в теоретико-множественной математике, например, суждение $ х А (х) может быть доказано приведением к нелепости его отрицания. Такое доказательство обыкновенно не содержит никакого способа построения искомого конструктивного объекта. Конструктивная математика считает, что подобное рассуждение доказывает не $ х А (х), а его «двойное отрицание», то есть ùù$ х А (х). Последнее суждение рассматривается в конструктивной математике как, вообще говоря, более слабое, чем $ х А(х). Таким образом, конструктивная математика не принимает закона снятия двойного отрицания, а, следовательно, и закона исключенного третьего (на отсутствие оснований для принятия последнего указывает и конструктивная трактовка дизъюнкции).
Первоначальные математические структуры – натуральные, целые и рациональные числа – непосредственно могут трактоваться как слова некоторых простых типов в фиксированном алфавите, при этом соответствующие отношения равенства и порядка легко сводятся к графическому совпадению и различию слов. Введение более сложных структур – действительных чисел, функций над ними и т. д. –осуществляется в конструктивной математике на основе понятия алгоритма, играющего в ней примерно такую же роль, какую играет в традиционной математике понятие функции. Считая интуитивные представления об алгоритмах слишком расплывчатыми для таких построений, конструктивная математика делает здесь принципиальный шаг, стандартизируя используемые алгоритмы посредством принятия одного из современных точных определений этого понятия вместе с соответствующей гипотезой типа Чёрча тезиса, принципа нормализации и т.д., утверждающей совпадение оперативных возможностей, доставляемых алгоритмами в интуитивном и точном смысле слова. Фактически наибольшее применение в конструктивной математике получили нормальные алгорифмы Маркова. К необходимости уточнения понятия алгоритма приводит также и конструктивная трактовка существования. Например, отрицание суждения " х $ у A (х,у) есть утверждение о невозможности некоторого алгоритма, между тем интуитивные представления, достаточные для опознания в качестве алгоритма того или иного конкретного предписания, в принципе не позволяют получать сколько-нибудь нетривиальные теоремы невозможности. На основе изложенных принципов и опираясь на современную теорию алгоритмов, конструктивная математика строит ряд математических дисциплин, в том числе и конструктивный математический анализ, включая сюда элементы функционального анализа, дефференциальные уравнения, теорию функций комплексного переменного и т.д.. Получаемые таким образом теоретические модели, основанные на более скромной чем обычносистеме абстракций, хотя и уступают традиционным в прозрачности и элегантности, тем не менее, по-видимому, способны обслужить тот же круг приложений.
Имея общий критический источник с интуиционимтической математикой Л.Брауэра и заимствовав из неё ряд конмтрукций и идей, контруктивная математика обнаруживает определённое сходство с последней. Вместе с тем, здесь имеются и принципиальные отличия как общефилософского, так и конкретно математического характера. Прежде всего констуктивная математика не разделяет интуиционизму убеждение е первоначальном характере математической интуиции, считая, что сама эта интуиция формаируется под влиянием практической деятельности человека. Соответственно абстрагирование в конструктивной математике идет не от умственных построений как в интуиционизме. А от простейших реально наблюдаемых, конструктивных процессов. В математическом плане конструктивная математика не принимает выходящую за рамки конструктивных процессов и объектов концепцию свободно становящейся последовательности и основанную на ней интуиционистскую теорию континуума как среды свободного становления. С другой стороны, интуиционистическая математика не принимает правила конструктивного подбора и не считает необходимым элиминировать интуитивные алгоритмы при помощи соответственных точных определений. Следует заметить, что в последние годы наметилась определённая тенденция к сближению конструктивного и интуитивного подходов; в некоторых конструктивных исследованиях, в особенности относящихся к семантике, используются индуктивные определения и соответствующие им индуктивные доказательства, напоминающие построения Л. Брауэра при доказательстве им так называемой бар-теоремы, занимающей одно из центральных мест в интуиционистской математике.
2. КОНСТРУКТИВНАЯ СЕМАНИТКА КАК СОВОКУПНОСТЬ СПОСОБОВ ПОНИМАНИЯ СУЖДЕНИЙ В КОНСТРУКТИВНОЙ МАТЕМАТИКЕ.
Небоходимость в особой семантике вызвана различием общих принципов, лежащих в основе традиционной (классической) и конструктивной математики. Особое внимание конструктивная семантика уделяет суждениям о конструктивных объектах в языках первого порядка, то есть, по существу, арифметическим суждениям. Принципиальные различия с традиционной семантикой в понимании дизъюнкций A0ÚA1сформулированы Л. Брауэром. Контструктивное обоснование таких сужднеий требует решения задачи: найти число i £ 1такое, что верно Ai (соответственно найти число n такое, что А(n)). Общие принципы описания задач, соответствующих более сложным формулам юыли намечены А. Гейтингом и А.Н.. Колмогоровым. Точная формулировка (которая стала возможна после появления математического определения алгоритма) была дана С. Клини в виде понятия реализации замкнутой арифметической формулы. Реализация вернорго равенства t=rесть фиксированнная константа, например число 0, а ложное равенство не имеет реализаций. Реализация конъюнкции А&В –это пара (a,b),где a – реализация А, а b – реализация В. Реализация дизъюнкции A0ÚA1 - это пара (i,a), где i =0,1 и a - реализация суждения A1. Реализация суждения $ х A (х) - это пара (n,a), где n – число, a – реализация суждения А(n). Реализация суждения " х A (х) - этообщий метод ¦, который по всякому натуральному n выдаёт реализацию ¦(n) суждения А(n). Реализация суждения А É В – это общий метод ¦, который по всякой реализации а суждения А выдаёт реализацию ¦(а) суждения В (и может быть не определён для аргументов а, не являющихся реализациями А). При этом общий метод понимается как алгоритм (частично рекурсивная функция). Используя кодирование алгоритмов числами, можно записать условие «число еесть реализация формулы А» в виде арифметической формулы (erA), не содержащей дизъюнкции Vи содержащей существование $только перед равенствами. Такие формулы называются почти нормальными. Суждение $e (erA) (читаемое «А реализуемая») может служить конструктивным разъяснением суждения А. При таком понимании закон исключённого третьего " х (A (х) Úù А (х)) опровергается, например, для A (x) = E y T (x,x,y),где T (e,x,y) означает, что алгоритм (с кодом) е заканчивает работу над аргументом x за у шагов. Опровергается и закон двойного отрицания " х (ùù В (х)É В (х)), например для В (х)=A (х) Úù А (х). Приведенное определение связывает конструктивную задачу (поиск реализации) со всяким суждением A, даже если А не содержит Ú, $. Предложенный Н.А. Шаниным алгоритм выявления конструктивной задачи не меняет формул без Ú, $(нормальных формул) и эквивалентен реализуемости в формальной интуиционистической арифметике с бескванторной индукцией. Произвольные формулы сводятся к почти нормальным, так как основания для почти нормальных формул, содержащих Ú и нетривиальное $.