КОНСТРУКТИВНАЯ СЕМАНИТКА КАК СОВОКУПНОСТЬ СПОСОБОВ ПОНИМАНИЯ СУЖДЕНИЙ В КОНСТРУКТИВНОЙ МАТЕМАТИКЕ

2. КОНСТРУКТИВНАЯ СЕМАНИТКА КАК СОВОКУПНОСТЬ СПОСОБОВ ПОНИМАНИЯ СУЖДЕНИЙ В КОНСТРУКТИВНОЙ МАТЕМАТИКЕ.

Небоходимость в особой семантике вызвана различием общих принципов, лежащих в основе традиционной (классической) и конструктивной математики. Особое внимание конструктивная семантика уделяет суждениям о конструктивных объектах в языках первого порядка, то есть, по существу, арифметическим суждениям. Принципиальные различия с традиционной семантикой в понимании дизъюнкций A0ÚA1 сформулированы Л. Брауэром. Контструктивное обоснование таких сужднеий требует решения задачи: найти число i £ 1 такое, что верно Ai (соответственно найти число n такое, что А(n)). Общие принципы описания задач, соответствующих более сложным формулам юыли намечены А. Гейтингом и А.Н.. Колмогоровым. Точная формулировка (которая стала возможна после появления математического определения алгоритма) была дана С. Клини в виде понятия реализации замкнутой арифметической формулы. Реализация вернорго равенства t=r есть фиксированнная константа, например число 0, а ложное равенство не имеет реализаций. Реализация конъюнкции А&В –это пара (a,b),где a – реализация А, а b – реализация В. Реализация  дизъюнкции A0ÚA1 - это пара (i,a), где i =0,1 и a - реализация суждения A1. Реализация суждения $ х A (х)  - это пара (n,a), где n – число, a – реализация суждения А(n). Реализация суждения " х A (х) - это общий метод ¦, который по всякому натуральному n выдаёт реализацию ¦(n) суждения А(n). Реализация суждения А É В – это общий метод ¦, который по всякой реализации а суждения А выдаёт реализацию ¦(а) суждения В (и может быть не определён для аргументов а, не являющихся реализациями А). При этом общий метод понимается как алгоритм (частично рекурсивная функция). Используя кодирование алгоритмов числами, можно записать условие «число е есть реализация формулы А» в виде арифметической формулы (erA), не содержащей дизъюнкции V и содержащей существование $ только перед равенствами. Такие формулы называются почти нормальными. Суждение $ e (erA) (читаемое «А реализуемая») может служить конструктивным разъяснением суждения А. При таком понимании закон исключённого третьего " х (A (х) Ú ù А (х)) опровергается, например, для A (x) = E y T (x,x,y), где T (e,x,y) означает, что алгоритм (с кодом) е заканчивает работу над аргументом x за у шагов. Опровергается и закон двойного отрицания " х (ù ù В (х) É В (х)), например для В (х)=A (х) Ú ù А (х). Приведенное определение связывает конструктивную задачу (поиск реализации) со всяким суждением A, даже если А не содержит Ú, $. Предложенный Н.А. Шаниным алгоритм выявления конструктивной задачи не меняет формул без Ú, $ (нормальных формул) и эквивалентен реализуемости в формальной интуиционистической арифметике с бескванторной индукцией. Произвольные формулы сводятся к почти нормальным, так как основания для почти нормальных формул, содержащих Ú и нетривиальное $.

А.А. Марков определяет истинность для почти нормальных формул с помощью выводимости по обычным правилам для рассматриваемых логических связок плюс эффективное w-правило: если имеется общий метод, позволяющий для любого n устанавливать выводимость А(n) из суждения К, то " х A(х) выводимо из К.. Истинность определяется постепенно. Язык Яw , состоящий из из формул без É,"; язык Яn+1, n ³ 1, включая Яn и формулы, которые можно построить из формул языка Яn одним применением импликации и любым числом применений А, &. Истинность для Я1 – формул – это выводимость по обычным правилам для &, $, Ú. Истинность для Я2 -формул определяется через допустимость соответствующего правила. Например, истинность $ х R (х) É $ y T (y) означает наличие алгоритма j такого, что R (n) É T (j (n )) для любого числа n. Для Яn+1 – формул при n>1 истинность конъюкций и " -формул определяется обычным образом через истинность компонента, а истинность импликации А É В означает выводимость В из А  по некоторым правилам Sn, о которых уже доказано, что они сохраняют истинность Яn – формул. Системы Sn содержат w-правило, а в качестве аксиом – все истинные Яn – формулы. Понятие выводимости в Sn вводится обобщенным индуктивным определением, а для доказательства метатеорем применяется соответствующий принцип индукции. Индукцией по S2 – выводу доказывается допустимость правила " É ù ù $  х R - А É $ х R . Оно включается в S3  и даёт принцип Маркова ù ù $ х R É $ х R.. Системы Sn+3 , n ³ 1, состоят из обычных правил для рассматриваемых связок, включая w-правило. Оказывается, что почти нормальная формула А истинна по Маркову тогда и только тогда, когда примитивно рекурсивное дерево Tа поиска вывода формулы А без сечения (но с w-правилом и принципом Маркова) является выводом в смысле индуктивного определения. Это эквивалентно (в рамках классической математики) классической истинности А.

В мажоритальной семантике Н.А. Шанина для каждой почти нормальной формулы А определяется трансвинитная иерархия {А ^a} формул простой структуры, причём А ^aÉ А доказуемо в подходящей формальной системе. Формула А ^a называется мажоритарной для А,и А считается истинной формулой ранга a, если А ^aверна. Точность аппроксимации растёт с ростом a : a < b É( А ^aÉ А ^b). Если отвлечься от технических деталей, то формула А строится с помощью a - кратного вынесения кванторов, согласно эквивалентности

ù ù (ВÚù ù $ u" vC (u, v))« $ u" vù ù (BÚù ù $ u" vC(u, v) Ú C(u, v)),

и сворачивания цепочек кванторов с помощью алгоритма выявления конструктивной задачи. Это даёт доказуемую в арифметике с транксфинитной индукцией до a эквивалентность

А« $ u" vù ù (ù ù $ w С a Ú Da)

с бесквантовой формулой С a, так что

А ^a = $ u" v $ w С a (u, v, w)

оказывается мажорантой для А. Суждение оказывается с точностью до технических деталей, эквивалентным утверждению о существовании вывода высоты <a исходной формулы с использованием w-правила. В этом смысле мажоритарная семантика эквивалентна ступенчатой семантике А.А. Маркова. После фиксации некоторого класса q общекурсивных функций (например, класса всех функций, определимых пекурсией до a ) определяются мажоранты ещё более простой структуры:

$ u" v С a (u, v, j( v)) для jÎq .

Если К – бесквантовое исчисление для класса q, то К- истинность $ u " v C (u, v) определяется как выводимость формулы С (t, v) c переменной v для некоторого постоянного терма t. Если в качестве К взято стандартное исчисление равенств для функций, определимых рекурсией до ординалов, меньших a, то К- истинными оказываются формулы, выводимые в формальной интуиционной арифметике, пополненной принципом Маркова, соотношениями, определяющими алгоритм выявления конструктивной задачи, и правилом индукции до ординалов b таких, что e (b) – первое e - число, большее b. В частности, a=e0 для b=w, т.е. для обычной индукции.

Доведение обоснования до бескванторного уровня (К- истинность) связано со стремлением остаться по возможности в рамках финитизма, т.е. бескванторного языка и соответствующих логических средств. С этим же связано стремление ограничиться небольшими a.. Для большей части «работающего» конструктивного анализа (включая теорему о непрерывности эффективных операторов) достаточно конечных a..