А.А. Марков определяет истинность для почти нормальных формул с помощью выводимости по обычным правилам для рассматриваемых логических связок плюс эффективное 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..
1).КОНСТРУКТИВНОЕ ДЕЙСТВИТЕЛЬНОЕ ЧИСЛО.
Конструктивное действительное число – понятие действительного числа, употребляемое в конструктивной математике. В более широком смысле – действительное число, конструируемое в соответствии с тем или иным кругом конструктивных средств. Близкое значение имеет термин «вычислимое действительное число», обычно употребляемый в тех случаях, когда не ставится цель изначального, нетрадиционного, нетрадиционного построения континуума, а речь идёт просто о классических действительных числах, вычислимых в том или ином смысле посредством некоторых алгоритмов.
2) КОНСТРУКТИВНЫЙ ОБЪЕКТ.
КОНСТРУКТИВНЫЙ ОБЪЕКТ — название, установившееся за математич. объектами, возникающими в результате развертывания так называемых конструктивных процессов. При описании того или иного конкретного конструктивного процесса обычно «...предполагается, что отчетливо охарактеризованы объекты, которые в данном рассмотрении фигурируют в качестве нерасчленяемых на части исходных объектов; предполагается, что задан список тех правил образования новых объектов из ранее построенных, которые в данном рассмотрении фигурируют в качестве описаний допустимых шагов конструктивных процессов; предполагается, что процессы построения осуществляются отдельными шагами, причем выбор каждого очередного
шага произволен в тех границах, которые определяются списком ранее построенных объектов и совокупностью тех правил образования, которые фактически можно применить к ранее построенным объектам». Такое описание конструктивного процесса, а тем самым и Конструктивного объекта, разумеется, не может претендовать на то, чтобы быть точным математич. определением. Однако конкретные математич. теории всегда имеют дело лишь с такими конкретными типами Конструктивного объекта, которые допускают точную характеризацию. Приведенное выше описание Конструктивного объекта служит в таких ситуациях ориентиром для выбора соответствующих точных определений.Примером точно определенного типа Конструктивного объекта могут служить слова в каком-либо фиксированном алфавите (буквы этого алфавита играют роль исходных объектов; новые слова получаются из уже имеющихся путем приписывания к последним справа букв рассматриваемого алфавита). Другими примерами типов Конструктивного объекта могут служить конечные графы, конечные абстрактные топологические комплексы, релейно-контактные схемы (выбор соответствующих исходных объектов и правил образования не представляет труда). Как Конструктивный объект могут быть также определены рациональные числа, алгебраические многочлены, алгоритмы и исчисления различных точно определенных типов, автоматы конечные, конечно определенные группы и другие им подобные математич. объекты.
Конструктивные объекты играют важную роль в тех математич. теориях, в к-рых возникает потребность в рассмотрении объектов, допускающих отчетливое индивидуальное задание средствами той или иной математич. символики. В рамках теоретико-множественной математики, неограниченно использующей абстракцию актуальной бесконечности, Конструктивный объект и произвольные множества Конструктивного объекта рассматриваются одновременно и наравне с прочими математич. Объектами, среди которых Конструктивные объекты выделяются лишь своей большей «осязаемостью». В рамках конструктивной математики Конструктивные объекты или объекты, задаваемые ими) представляют собой единственно допускаемый к рассмотрению тип математич. объектов, и рассмотрение их здесь ведется на базе отказа от применения абстракции актуальной бесконечности и на основе специальной конструктивной логики, учитывающей, в частности, специфику определения Конструктивного объекта.