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

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, даже если А не содержит Ú, $. Предложенный Н.А. Шаниным алгоритм выявления конструктивной задачи не меняет формул без Ú, $ (нормальных формул) и эквивалентен реализуемости в формальной интуиционистической арифметике с бескванторной индукцией. Произвольные формулы сводятся к почти нормальным, так как основания для почти нормальных формул, содержащих Ú и нетривиальное $.

А.А. Марков определяет истинность для почти нормальных формул с помощью выводимости по обычным правилам для рассматриваемых логических связок плюс эффективное w-правило: если имеется общий метод, позволяющий для любого n устанавливать выводимость А(n) из суждения К, то " х A(х) выводимо из К Истинность определяется постепенно. Язык Яw , состоящий из из формул без É,"; язык Яn+1, n ³ 1, включая Яn и формулы, которые можно построить из формул языка Яn одним применением импликации и любым числом применений А, &. Истинность для Я1 – формул – это выводимость по обычным правилам для &, $, Ú. Истинность для Я2 -формул определяется через допустимость соответствующего правила. Например, истинность $ х R (х) É $ y T (y) означает наличие алгоритма j такого, что R (n) É T (j (n )) для любого числа n. Для Яn+1 – формул при n>1 истинность конъюкций и " -формул определяется обычным образом через истинность компонента, а истинность импликации А É В означает выводимость В из А по некоторым правилам Sn, о которых уже доказано, что они сохраняют истинность Яn – формул. Системы Sn содержат w-правило, а в качестве аксиом – все истинные Яn – формулы. Понятие выводимости в Sn вводится обобщенным индуктивным определением, а для доказательства метатеорем применяется соответствующий принцип индукции. Индукцией по S2 – выводу доказывается допустимость правила " É ù ù $ х R - А É $ х R . Оно включается в S3 и даёт принцип Маркова ù ù $ х R É $ х R Системы Sn+3 , n ³ 1, состоят из обычных правил для рассматриваемых связок, включая w-правило. Оказывается, что почти нормальная формула А истинна по Маркову тогда и только тогда, когда примитивно рекурсивное дерево Tа поиска вывода формулы А без сечения (но с w-правилом и принципом Маркова) является выводом в смысле индуктивного определения. Это эквивалентно (в рамках классической математики) классической истинности А.

В мажоритальной семантике Н.А. Шанина для каждой почти нормальной формулы А определяется трансвинитная иерархия {А a} формул простой структуры, причём А a É А доказуемо в подходящей формальной системе. Формула А a называется мажоритарной для А,и А считается истинной формулой ранга a, если А a верна. Точность аппроксимации растёт с ростом a : a < b É( А a É А b). Если отвлечься от технических деталей, то формула А строится с помощью a - кратного вынесения кванторов, согласно эквивалентности