Математическая энциклопедия - конструктивная семантика

совокупность способов понимания суждений в конструктивной математике. Необходимость в особой семантике вызвана различием общих принципов, лежащих в основе традиционной (классической) и конструктивной математики (далее последний термин будет в основном относиться к подходу, развитому в советской школе конструктивной математики).

Основное внимание К. с. уделяет суждениям о конструктивных объектах в языках первого порядка, то есть, по существу, арифметич. суждениям (см. Арифметика формальная). Принципиальные различия с традиционной семантикой в понимании дизъюнкций (и суждений о существовании сформулированы Л. Брауэром (L. Brouwer). Конструктивное обоснование таких суждений требует решения задачи: найти число такое, что верно Ai (соответственно найти число птакое, что А(n)). Общие принципы описания задач, соответствующих более сложным формулам, были намечены А. Рейтингом (А. Неуting) и А. Н. Колмогоровым. Точная формулировка (к-рая стала возможной после появления магематич. определения алгоритма). была дана С. Клини (S. Kleene) в виде понятия реализации замкнутой арифметич. формулы (см. Рекурсивная реализуемость). Реализация верного равенства t=r есть фиксированная константа, напр, число 0, а ложное равенство не имеет реализаций.

Реализация конъюнкции АaВэто пара (а, b), где ареализация А, bреализация В. Реализация дизъюнкции это пара (i, а), где i=0,1 на реализация суждения А i. Реализация суждения это пара {п, а), где пчисло, ареализация суждения (п). Реализация суждения это общий метод f, к-рый по всякому натуральному пвыдает реализацию f(n)суждения А(n).

Реализация суждения это общий метод f, к-рый по всякой реализации асуждения А выдает реализацию f(a)суждения В(и может быть не определен для аргументов а, не являющихся реализациями А). При этом общий метод понимается как алгоритм (частично рекурсивная функция). Используя кодирование алгоритмов числами, можно записать условие "число еесть реализация формулы Л" в виде арифметич. формулы ( еrА), не содержащей дизъюнкции и содержащей существование только тривиальным образом перед равенствами. Такие формулы наз. почти нормальными. Суждение (читаемое "А реализуема") может служить конструктивным разъяснением суждения А.

При таком понимании закон исключенного третьего х (А(х) опровергается, напр., для где Т( е, х, у )означает, что алгоритм (с кодом) езаканчивает работу над аргументом хза ушагов. Опровергается и закон двойного отрицания В(х)), напр, для Приведенное определение связывает конструктивную задачу (поиск реализации) со всяким суждением А, даже если Ане содержит Предложенный Н.

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

.