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

принцип Маркова,- логико-философский принцип конструктивной математики, выдвинутый А. А. Марковым [1], [2] и в общей форме утверждающий, что если конструктивный процесс, заданный нек-рым предписанием, не является неограниченно продолжаемым, то он заканчивается. В конструктивной математике получили применение несколько конкретных, содержательно эквивалентных разновидностей этого принципа. 1) Пусть W- нормальный алгорифм, Р- слово в его алфавите. Тогда, если опровергнуто предположение о неприменимости Y к Р, то Y применим к Р;символически [img: http://localhost:8080/file/021235-68.jpg] 2) В арифметике формальной К. п. п. может быть выражен следующей арифметич. формулой [img: http://localhost:8080/file/021235-69.jpg] где T1 - примитивно рекурсивный предикат такой, что частично рекурсивная функция с гёделевым номером z определена на хтогда и только тогда, когда EyT1(z, х, у)(ср. [3]). 3) Если рекурсивно перечислимое множество непусто, то оно содержит нек-рый элемент. 4) Пусть А- алгоритмически проверяемое свойство натуральных чисел. Тогда, если опровергнуто предположение о том, что не существует числа со свойством А, то найдется натуральное число со свойством А. Соответствующая логическая схема записывается в виде [img: http://localhost:8080/file/021235-70.jpg] Иногда термин "К. п. п." специально связывается именно с этой последней формой рассуждений, поскольку искомое число "подбирается" в ходе следующего конструктивного процесса: проверяют А(0), если это верно, то берут 0 в качестве искомого числа, в противном случае переходят к проверке А (1) и т. д. Интуитивное оправдание К. п. п. в рамках применяемой в конструктивной математике системы абстракций состоит в том, что если невозможность неограниченного продолжения данного конструктивного процесса убедительно доказана, то потенциально достижимо окончание этого процесса в результате его последовательного выполнения шаг за шагом. Таким образом, при утверждении существования конструктивного объекта (напр., результата применения нормального алгорифма к слову) на основании К. п. п. не происходит выхода за рамки абстракции потенциальной осуществимости. К. п. п. безусловно допустим с точки зрения классич. логики, поскольку он является частным случаем общего закона снятия двойного отрицания и закона исключенного третьего. Применение этих логических законов сводится к К. п. п. во многих конструкциях теории рекурсивных функций, что делает эти конструкции достоянием конструктивной математики. Использование К. п. п. позволяет также получить ряд значительных результатов в конструктивном анализе, в частности теорему о непрерывности алгоритмич. операторов и о продолжимости эффективных функционалов до частично рекурсивных функционалов (см. также Конструктивное метрическое пространство). Другой сферой приложений К. п. п. является конструктивная семантика [4]. Еще задолго до формулировки К. п. п. в качестве общего принципа конструктивной математики проводились исследования по обоснованию различных форм этого принципа в рамках того или иного круга допускаемых конструктивных средств. Здесь следует указать следующий основополагающий результат П. С. Новикова, полученный в 1943 (см. [5]): пусть для формулы (х)с одной переменной в конструктивной формальной арифметике выводимо [img: http://localhost:8080/file/021235-71.jpg] для каждого пи в классической арифметике выводимо E хА (х);тогда формула [img: http://localhost:8080/file/021235-72.jpg] выводима и в конструктивной арифметике. В работе [6] было получено обоснование К. п. п. в рамках новой системы конструктивной семантики, развиваемой в последние годы А. А. Марковым. Являясь, по-видимому, наименее непосредственной из первоначальных установок конструктивной математики, К. п. п. принимается нек-рыми сторонниками последней с известными оговорками. К. п. п. отвергается также интуиционистской математикой как недостаточно убедительный интуитивно. С другой стороны, в связи с формализацией ряда разделов интуиционистской математики детально изучались вопросы о соотношениях соответствующих систем с формальными схемами, выражающими К. п. п. В частности, установлена независимость схем (2) и (4) от аксиом интуиционистского исчисления предикатов, арифметики и анализа (см. [2], [7], [8]).