Конструктивная Семантика

Совокупность способов понимания суждений в конструктивной математике. Необходимость в особой семантике вызвана различием общих принципов, лежащих в основе традиционной (классической) и конструктивной математики (далее последний термин будет в основном относиться к подходу, развитому в советской школе конструктивной математики). Основное внимание К. с. уделяет суждениям о конструктивных объектах в языках первого порядка, то есть, по существу, арифметич. суждениям (см. Арифметика формальная). Принципиальные различия с традиционной семантикой в понимании дизъюнкций (и суждений о существовании сформулированы Л. Брауэром (L. Brouwer). Конструктивное обоснование таких суждений требует решения задачи: найти число такое, что верно Ai (соответственно найти число птакое, что А(n)). Общие принципы описания задач, соответствующих более сложным формулам, были намечены А. Рейтингом (А. Неуting) и А. Н. Колмогоровым. Точная формулировка (к-рая стала возможной после появления магематич. определения алгоритма). была дана С. Клини (S. Kleene) в виде понятия реализации замкнутой арифметич. формулы (см. Рекурсивная реализуемость). Реализация верного равенства t=r есть фиксированная константа, напр, число 0, а ложное равенство не имеет реализаций. Реализация конъюнкции АaВ- это пара (а, b), где а- реализация А, b- реализация В. Реализация дизъюнкции — это пара (i, а), где i=0,1 на — реализация суждения А i. Реализация суждения — это пара формул простой структуры, причем доказуемо в подходящей формальной системе. Формула А a. наз. мажорантой для А, и А считается истинной формулой ранга а, если А a. верна. Точность аппроксимации растет с ростом а:Ab). Если отвлечься от технических деталей, то формула Астроится с помощью a-кратного вынесения кванторов, согласно эквивалентности и сворачивания цепочек кванторов с помощью алгоритма выявления конструктивной задачи. Это дает доказуемую в арифметике с трансфинитной индукцией до а эквивалентность с бескванторной формулой С a, так что оказывается мажорантой для А. Суждение А a оказывается, с точностью до технических деталей, эквивалентным утверждению о существовании вывода высоты <a для исходной формулы с использованием w-правила. В этом смысле мажорантная семантика эквивалентна ступенчатой семантике А. А. Маркова. После фиксации нек-рого класса в общерекурсивных функций (напр., класса всех функций, определимых рекурсией до а) определяются мажоранты еще более простой структуры: Если К- бескванторное исчисление для класса в, то K-истинность формулы Eu"vC(u, v )определяется как выводимость формулы С(t, v )с переменной vдля нек-рого постоянного терма t. Если в качестве Квзято стандартное исчисление равенств для функций, определимых рекурсией до ординалов, меньших a, то K-истинными оказываются формулы, выводимые в формальной интуиционистской арифметике, пополненной принципом Маркова, соотношениями, определяющими алгоритм выявления конструктивной задачи, и правилом индукции до ординалов b таких, что где e(b) — первое е-число, большее р. В частности, a=e0 для b=w, т. е. для обычной индукции. Доведение обоснования до бескванторного уровня (К-истинность) связано со стремлением остаться по возможности в рамках финитизма, т. е. бескванторного языка и соответствующих логических средств. С этим же связано стремление ограничиться небольшими a. Для большей части "работающего" конструктивного анализа (включая теорему о непрерывности эффективных операторов) достаточно конечных a. Лит.:[1] Марков А. А., в сб.: Исследования по теории алгорифмов и математической логике, М., 1976, т. 2, с.3-31; [2] Шанин Н. А., "Тр. Матем. ин-та АН СССР", 1973, т. 129, с. 203-66; [3] Клини С. К., Введение в метаматематику, пер. с англ., М., 1957. Г. Е. Минц.