Логика конструктивная

Конструктивная логика — это раздел современной математической логики (см. Логика математическая), изучающий рассуждения о конструктивных объектах (см. Конструктивный объект) и процессах (см. Конструктивный процесс). Конструктивные объекты представляют собой или отдельные, ясно отличаемые друг от друга знаки (см. Знак), или последовательности таких знаков, получаемые посредством некоторого конструктивного процесса, протекающего по чётким дискретным правилам. Примером элементарного конструктивного объекта могут служить легко отождествляемые и различаемые буквы какого-либо алфавита, а примером конструктивного процесса — построение из них слов по однозначно определённым правилам.

Конструктивная логика развивается как совокупность логических принципов, признаваемых представителями математического конструктивизма (см. Конструктивизм математический). Принципы конструктивной логики включают абстракцию потенциальной, но не актуальной бесконечности, когда невозможность полного обозрения какого-либо бесконечного образования не учитывается. Бесконечное множество, например множество всех натуральных чисел, нельзя рассматривать как единый, завершённый объект. Существование конструктивного объекта считается доказанным лишь в том случае, если указан способ потенциально осуществимого его построения — конструирования. Ограничение рассуждений конструктивными объектами и процессами (как правило, описываемыми алгоритмами) определённым образом изменяет понимание логических связок и кванторов по сравнению с их пониманием в классической логике (см. Логика). Так, дизъюнкция высказываний «A или B» считается обоснованной, если потенциально осуществим конструктивный процесс, позволяющий выбрать верный член этой дизъюнкции; аналогично оценивается обоснованность многочленных дизъюнкций. Близко к пониманию дизъюнкции истолкование квантора существования: утверждение «существует такой x, для которого справедливо условие A» считается обоснованным, если потенциально осуществим конструктивный процесс подбора конструктивного объекта x, подтверждающего условие A. Обоснование конъюнкции «A и B» состоит в обосновании обоих (то есть всех) конъюнктивных членов, а утверждение «Для всякого x справедливо условие A» считается обоснованным, если мы в состоянии для всякого объекта рассматриваемого вида доказать, что он удовлетворяет предъявленному требованию. Обоснование импликации «если A, то B» состоит в предъявлении конструктивного процесса, позволяющего по обоснованию утверждения A построить обоснование утверждения B. Отрицание утверждения A обосновывается предъявлением конструкции, приводящей к противоречию всякую попытку обоснования A.

Конструктивное истолкование логических связок и кванторов допускает и многие другие уточнения. В частности, созданы различные аксиоматические системы конструктивной логики. Поскольку конструктивная позиция идейно близка интуиционистской (см. Интуиционизм), аксиоматические системы, первоначально предназначавшиеся для реконструкции интуиционистски приемлемых рассуждений, называются (или подразумеваются) конструктивными. Например, активно изучающиеся суперинтуиционистские логики в 1960-е годы и несколько позже назывались суперконструктивными. Отличие этих логик от классической проявляется в том, что хотя конструктивно приемлемыми являются, например, законы p → ¬ ¬ p, ¬ ¬ ¬ p → ¬ p, (p → q) → (¬ q → ¬ p), в этих системах отсутствуют практически все остальные варианты форм рассуждений «от противного» — закон снятия двойного отрицания ¬ ¬ p → p, закон контрапозиции (¬ p → ¬ q) → (q → p), закон Клавия (¬ p → p) → p, закон Пирса (p → q) → p) → p, и другие.

Кроме того, в конструктивной логике связки независимы, то есть не выражаются друг через друга, нет классической взаимовыразимости кванторов всеобщности и существования. В результате оказываются, в частности, необоснованными рассуждения, приводящие к доказательству так называемых чистых теорем существования, типичным примером которых является доказательство Г. Кантора существования трансцендентных (то есть действительных, но не алгебраических) чисел: приводится к противоречию предположение о возможности расположить все действительные числа в последовательность, в то время как алгебраические числа в последовательность можно расположить. Чистые теоремы существования (имеется в виду формулировка теоремы, проистекающая из доказательства) имеют вид ¬ ¬ ∃xA (x), не переводимый в ∃xA (x), поскольку их доказательства не дают конкретного x, подтверждающего справедливость A, а лишь приводят к противоречию утверждение об отсутствии такого x. Однако ввиду специфики конструктивных объектов и процессов многими представителями конструктивизма (в отличие, например, от приверженцев интуиционизма) принимается принцип конструктивного подбора (или принцип Маркова): если имеется алгоритм, позволяющий по произвольному конструктивному объекту x осуществлять конструктивный процесс установления наличия у x свойства A, то в случае обоснования ¬ ¬ ∃xA (x) считается обоснованным и ∃xA (x).

Взаимосвязи классических и конструктивных логических систем проявляются на пропозициональном уровне в виде теоремы В. И. Гливенко:

• отрицательные утверждения в этих системах одинаковы;
• конструктивно приемлемым является двойное отрицание любого закона классической логики высказываний и наоборот.

Для справедливости теоремы Гливенко для предикатных вариантов конструктивных и классических систем необходимо добавление в качестве схемы аксиом в конструктивную систему закона ¬ ¬ (∀xA (x) ∨ ¬ ∀xA (x) и/или закона ∀x ¬ ¬ A (x) → ¬ ¬ ∀xA (x) (обратная импликация ¬ ¬ ∀xA (x) → ∀x ¬ ¬ ¬ A (x) принимается в конструктивной логике).

Отличительной чертой систем конструктивной логики и построенных на их основе теорий являются следующие свойства:

• свойство дизъюнкции (или дизъюнктивное свойство) — если выводима дизъюнкция, то выводим и некоторый её дизъюнктивный член;
• экзистенциальное свойство — если выведена формула ∃xA (x), то можно вывести и формулу A (t) при некотором конкретном эффективно разыскиваемом t, то есть из доказательства существования конструктивного объекта с требуемыми свойствами можно извлечь конструкцию его построения.

Кроме аксиоматических систем конструктивной логики, имеются различные семантические построения, отражающие конструктивные воззрения на смысл логических связок, формул и так далее. Наиболее известными являются рекурсивная реализуемость по С. К. Клини и её варианты, разработанная Н. А. Шаниным мажорантная семантика арифметических формул, созданная А. А. Марковым ступенчатая система построения логических языков с одновременным определением их семантики «снизу вверх».