ЛОГИКА КОНСТРУКТИВНАЯ

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

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

Для сходных языков предлагались в некоторых случаях неэквивалентные определения понятия истинной ф-лы, что свидетельствует о существовании различных вариантов конструктивной математики. Наиболее существенные расхождения между различными вариантами существуют во взглядах на приемлемость тезиса Чёрча и принципа конструктивного подбора, выдвинутого сов. математиком А. А. Марковым (р. 1903). Этот принцип состоит в следующем: если для свойства Р натуральных чисел имеется алгоритм, выясняющий для всякого натурального числа обладает ли свойством Р, и опровергнуто предположение о том, что ни одно число свойством. Р не обладает, то имеется натуральное число со свойством Р.

В качестве обоснования совместимости этого принципа с основным требованием к доказательствам существования в конструктивной математике А. А. Марков указывает, что в описанной ситуации можно найти число , обладающее свойством Р, путем перебора натуральных чисел (начиная с нуля, в порядке возрастания) и проверки для каждого рассматриваемого числа , обладает ли оно свойством Р.

Одно из возможных определений понятия конструктивной истинности формул логико-арифм. языка основано на понятии рекурсивной реализуемости. Индукцией по числу вхождений логич. знаков в определяется отношение «натуральное число реализует По определению, напр., число реализует ф-лу, если есть номер (в некотором фиксированном упорядочении пар натуральных чисел) пары, первый член которой а есть 0 или 1, а второй член b есть число, реализующее ф-лу и реализующее ф-лу число реализует если — номер общерекурсивной ф-ции такой, что для любого к число реализует ф-лу. Принимая тезис Чёрча, арифм. ф-лу считают истинной тогда, когда существует реализующее ее число. Напр., ф-ла вида реализуема тогда и только тогда, когда существует алгоритм распознавания у числа свойства Р. Другим средством характеристики понятия конструктивно истинной ф-лы является указание алгоритма, перерабатывающего произвольную некоторого простого типа или в ф-лу более простого языка, рассматриваемую как «разъяснение», «расшифровка» исходной ф-лы. Таков алгоритм выявления конструктивной задачи, переводящий произвольную ф-лу языка (по существу, эквивалентного логико-арифм. языку), позволяющего формулировать суждения о словах и алгоритмах, в ф-лу вида , где А не содержит знаков или в вообще не содержащую этих знаков. В основу этого алгоритма положены идея, близкая к идее реализуемости, тезис Чёрча и принцип Маркова. Описаны также алгоритмы, устраняющие в ф-ле подчиненные переменные. Условием истинности ф-лы логич. языка естественно считать истинность всех ф-л некоторого логико-матем. языка, обладающих той же логич. структурой. Таково, напр., понятие реализуемости ф-л исчисления высказываний.

Дедуктивные системы Л. к. часто получают из соответствующих классических систем, отбрасывая неприемлемые аксиомы, схемы аксиом или правила вывода, чаще всего — исключенного третьего загон или закон двойного отрицания. Так получают конструктивное исчисление высказываний, конструктивное исчисление предикатов, конструктивную арифметику. Такие системы могут быть расширены, напр., присоединением аксиом истинных конструктивно, но не классически, как , где х, у — переменные для натуральных чисел, переменная для общерекурсивных ф-ций.

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

Значение Л. к. для развития конструктивной математики обусловлено тем, что с помощью ее понятий и теорем можно разъяснять конструктивное понимание матем. суждений, исследовать, насколько глубоки различия между конкретными теориями конструктивной математики и соответствующими классическими теориями, а также между различными вариантами теорий конструктивной математики.

Лит.: Шанин Н. А. О конструктивном понимании математических суждений. «Труды Математического института им. В. А. Стеклова АН СССР», 1958, т. 52; Марков А. А. О конструктивной математике. «Труды Математического института им. В. А. Стеклова АН СССР», 1962, т. 67; Шанин Н. А. О рекурсивном математическом анализе и исчислении арифметических равенств Р. Л. Гудстейна. В кн.: Гудстейн Р. Л. Рекурсивный математический анализ. Пер. с англ. М., 1970; Клини С. К. Математическая логика. Пер. с англ. М., 1973 [библиогр. с. 451-465]; Кушнер Б. А. Лекции по конструктивному математическому анализу. М., 1973 [библиогр. с. 427—440]. В. А. Лифшиц.