Конструктивного Подбора Принцип

Принцип Маркова,- логико-философский принцип конструктивной математики, выдвинутый А. А. Марковым [1], [2] и в общей форме утверждающий, что если конструктивный процесс, заданный нек-рым предписанием, не является неограниченно продолжаемым, то он заканчивается. В конструктивной математике получили применение несколько конкретных, содержательно эквивалентных разновидностей этого принципа. 1) Пусть W- нормальный алгорифм, Р- слово в его алфавите. Тогда, если опровергнуто предположение о неприменимости Y к Р, то Y применим к Р;символически2) В арифметике формальной К. п. п. может быть выражен следующей арифметич. формулой где T1 — примитивно рекурсивный предикат такой, что частично рекурсивная функция с гёделевым номером z определена на хтогда и только тогда, когда EyT1(z, х, у )(ср. [3]). 3) Если рекурсивно перечислимое множество непусто, то оно содержит нек-рый элемент. 4) Пусть А- алгоритмически проверяемое свойство натуральных чисел. Тогда, если опровергнуто предположение о том, что не существует числа со свойством А, то найдется натуральное число со свойством А. Соответствующая логическая схема записывается в виде Иногда термин "К. п. п." специально связывается именно с этой последней формой рассуждений, поскольку искомое число "подбирается" в ходе следующего конструктивного процесса: проверяют А(0), если это верно, то берут 0 в качестве искомого числа, в противном случае переходят к проверке А (1) и т. д. Интуитивное оправдание К. п. п. в рамках применяемой в конструктивной математике системы абстракций состоит в том, что если невозможность неограниченного продолжения данного конструктивного процесса убедительно доказана, то потенциально достижимо окончание этого процесса в результате его последовательного выполнения шаг за шагом. Таким образом, при утверждении существования конструктивного объекта (напр., результата применения нормального алгорифма к слову) на основании К. п. п. не происходит выхода за рамки абстракции потенциальной осуществимости. К. п. п. безусловно допустим с точки зрения классич. логики, поскольку он является частным случаем общего закона снятия двойного отрицания и закона исключенного третьего. Применение этих логических законов сводится к К. п. п. во многих конструкциях теории рекурсивных функций, что делает эти конструкции достоянием конструктивной математики. Использование К. п. п. позволяет также получить ряд значительных результатов в конструктивном анализе, в частности теорему о непрерывности алгоритмич. операторов и о продолжимости эффективных функционалов до частично рекурсивных функционалов (см. также Конструктивное метрическое пространство). Другой сферой приложений К. п. п. является конструктивная семантика [4]. Еще задолго до формулировки К. п. п. в качестве общего принципа конструктивной математики проводились исследования по обоснованию различных форм этого принципа в рамках того или иного круга допускаемых конструктивных средств. Здесь следует указать следующий основополагающий результат П. С. Новикова, полученный в 1943 (см. [5]): пусть для формулы (х)с одной переменной в конструктивной формальной арифметике выводимо для каждого пи в классической арифметике выводимо E хА (х);тогда формула выводима и в конструктивной арифметике. В работе [6] было получено обоснование К. п. п. в рамках новой системы конструктивной семантики, развиваемой в последние годы А. А. Марковым. Являясь, по-видимому, наименее непосредственной из первоначальных установок конструктивной математики, К. п. п. принимается нек-рыми сторонниками последней с известными оговорками. К. п. п. отвергается также интуиционистской математикой как недостаточно убедительный интуитивно. С другой стороны, в связи с формализацией ряда разделов интуиционистской математики детально изучались вопросы о соотношениях соответствующих систем с формальными схемами, выражающими К. п. п. В частности, установлена независимость схем (2) и (4) от аксиом интуиционистского исчисления предикатов, арифметики и анализа (см. [2], [7], [8]). Лит.:[1] Марков А. А., "Успехи матем. наук", 1954, т. 9, в. 3, с. 226-30; [2] его же, в кн.: Тр. 3 Всесоюзного математического съезда, т. 2, М., 1956, с. 146-47; [3] Клини С. К., Введение в метаматематику, пер. с англ., М., 1957; [4] Шанин Н. А., "Тр. матем. ин-та АН СССР", 1958, т. 52, с. 226-311; [5] Новиков П. С, "Матем. сб.", 1943, т. 12, в. 2, с. 231-61; [6] Марков А. А., "Докл. АН СССР", 1974, т. 214, № 4, с. 765-68, т. 215, № 1, с. 57-60; [7] Клини С, Весли Р., Основания интуиционистской математики с точки зрения теории рекурсивных функций, пер. с англ., М., 1978; [8] Тrое1stra A. S., в кн.: ISILC. Proof theory symposion, В., 1975, p. 370-83. Б. А. Кушнер.