Представленная работа посвящена теории конструктивных булевых алгебр, и в ней исследуются проблемы нахождения критерия сильной конструктивизируемости булевых алгебр, & также проблемы построения конструктивных линейных порядков и булевых алгебр с некоторыми заданными алгебраическими и алгоритмическими свойствами. •. •'.'¦' «М?*>>'—» •'•: Л-* ;
Понятие сильно конструктивной модели было введено в 1968 году Ю. Л. Ершовым в его курсе лекций в Казахском университете в г. Алма-Ате, которые были опубликованы в посвященных А. И. Мальцеву трудах [5]. С этого понятия начинается ряд исследований, посвященных естественной проблеме нахождения критерия совпадения конструктивности и сильной конструктивности, а также необходимых и достаточных условий сильной конструктивизируемости. В случае булевых алгебр такие исследования были проведены в работах Н. Г. Хисамиева, С. С. Гончарова, С. П. Одинцова [8, 1, 12]. Н. Г. Хисамиевым был открыт один из первых признаков сильной конструктивности атомных булевых алгебр, состоящей в рекурсивности множества атомов [8]. Как было замечено в [6], этот признак является следствием сильной конструктивности конструктивных моделей модельно полных разрешимых теорий. В работе [4] С. С. Гончарова доказано, что от этого условия нельзя отказаться.
В работах [1, 4, 3] были введены промежуточные между сильной конструктивностью и конструктивностью понятия гг-конструктивности, а также было установлено различие этих понятий уже на классе булевых алгебр. В монографиях С. С. Гончарова [1, 2] нашли отражение базисные критерии и основные результаты этого направления. В частности, была найдена конструкция, сводящая в некоторых случаях проблемы построения критериев сильной конструктивизируемости булевых алгебр высших элементарных характеристик к критериям конструктивизируемости булевых алгебр так называемого нижнего слоя, т. е. элементарных характеристик (0, оо, 1), (1,1,0) и (1,0,1) в терминах ограниченных теорий [3].
Дальнейшее развитие исследований в этом направлении оказалось связанным с оригинальной идеей Л. Фейнера [15, 16], предложившего специальные оценки для булевых алгебр с заданными алгоритмическими свойствами и также общую идею построения рекурсивных булевых алгебр, опровергающих эти оценки, и, таким образом, заданные алгоритмические свойства, при любом изоморфизме. Как указывает сам Л. Фейнер, его работа и постановка проблемы была инициирована А. Неро-удом, и некоторая помощь была оказана В. Ханфом. Указанный выше результат С. С. Гончарова [4] — его пример атомной конструктивной, но не сильно конструк-тивизируемой булевой алгебры, — опирается на метод Фейнера и существенно его модернизирует, так что в дальнейшем мы называем его метод «методом Фейнера-Гончарова». Но стоит отметить, что сам метод Л. Фейнера так и остался мало-используемым в разделах современной теории конструктивных моделей — известен результат Дж. Реммела [17] о существовании конструктивной булевой алгебры с разрешимым множеством атомов, но с неразрешимым в любой конструктивизации идеалом Фреше, и также известна интересная работа Дж. Тёрбера [18], о которой будет подробнее сказано ниже.
Ряд положительных решений о возможности сильной конструктивизируемости булевых алгебр нижнего слоя, в частности, с элементарными характеристиками (1,1,0) и (1,0,1), был получен С. П. Одинцовым [12, 13]:
1. Конструктивная булева алгебра элементарной характеристики (1,1,0) с разрешимым множеством атомов и безатомных элементов будет сильно конструктивизируема.
2. Конструктивная булева алгебра элементарной характеристики (1,0,1) с разрешимым множеством атомов, безатомных и атомных элементов будет сильно конструктивизируема.
С.П. Одинцовым были анонсированы без доказательства [13] утверждения о возможности обобщения указанных выше результатов на высокие характеристики.
Автором диссертации В. Н. Власовым совместно с С. С. Гончаровым [21] был получен результат о сильной конструктивизируемости булевых алгебр элементарной характеристики (1,1,0) с разрешимым множеством атомов и с некоторым естественным условием (разложимости данной алгебры в эффективную прямую сумму конструктивных булевых алгебр с первой характеристикой 0), эквивалентному в данном случае разрешимости идеала Ершова-Тарскогоэто исследование и новый вариант доказательства предложены в первой главе. С. С. Гончаровым: было получено [2] и окончательное решение проблемы характеризации для случая характеристики (1,1,0) — конструктивная булева алгебра сильно конструктивизируема если, и только если, множество атомов в данной конструктивизации разрешимо, которое существенно опирается на теорему Гончарова-Власова [21].
Краткий обзор
Сделаем краткий обзор представляемой работы. Диссертация состоит из введения, трех глав, и заключения. Во введении также присутстует сводка основных обозначений и определений. Каждая глава состоит из нескольких параграфов. Основные результаты изложены в первых двух главах, третья глава носит более методологический характер.
Заключение
.
Подведем общий итог. В первой и во второй главах работы представлены теоремы, позволяющие уточнить или даже решить проблему сильной конструктивизируемости в конкретных случаях для булевых алгебр заданных элементарных характеристик. Так, совместный результат, изложенный в параграфе 1.1, в совокупности с другими результатами С. С. Гончарова [2], дает полную характеризацию для случая (1,1,0). В случае элементарной характеристики (п + 1,1,0), модификацией ранее использованного метода и при ослаблении условий, получен достаточный критерий сильной конструктивизируемости: (4п + 2)-конструктивизируемость и разложимость в эффективную прямую сумму БА с меньшей первой характеристикой Ершова-Тарского (что в соответствует разрешимости идеала /га+1). Вопрос более точных критериев сильной конструктивизируемости для высоких характеристик (п + 1,1,0), и вопрос применимости методов, использованных для решения проблемы (1,1,0) для высоких характеристик — пока остается открытым.
Во второй главе были достигнуты две цели. Во-первых, использованием модифицированного метода Фейнера-Гончарова были построены контр-примеры, позволяющие сделать вывод, что разрешимость только множества атомов в конструктивной булевой алгебре характеристики (1,0,1) не является достаточным условием сильной конструктивизируемости, и что также (4гг —1)-конструктивизируемость не является достаточным условием сильной конструктивизируемости в случае характеристики (п1, 0,1). Во-вторых был существенно модифицирован сам метод Фейнера-Гончарова для решения как узко-специфичных проблем конструирования линейных порядков БА нижнего слоя, так и для возможного более широкого обобщения в будущем. По-прежнему остается открытым вопрос достаточного критерия, и как уже указывалось, пока наиболее минимальные условия сформулированы С. П. Одинцовым [12, 13]: «Конструктивная булева алгебра элементарной характеристики (1, 0,1) с разрешимым множеством атомов, безатомных и атомных элементов будет сильно конструктивизируема». Для более высоких характеристик этого случая, кроме того пока проблематичен и аналог этого критерия.
Третья глава посвящена проблеме собственно метода Фейнера-Гончарова. В § 3.1 был построен некоторый «предельный» пример в ряду исследований предыдущей главы по сильной конструктивизируемости. Хотя в качестве уточнения критерия он имеет мало ценности, пример интересен в методологическом плане. На анализе его построения видны непреодолимые внутренние барьеры метода для исследовании в данном направлении для БА характеристики (1,0,1). «Тонкости» распознавания в арифметической иерархии (а именно алгоритм Тарского-Куратовского и используется для стандартного способа получения Фейнеровых оценок некоторых необходимых свойств сильной конструктивности в Б А) не хватает, чтобы распознать будет ли Ав разрешимым, или он будет лежать в и при этом распознавать нетривиальные тины изоморфизма выделяемых элементов.
Дальнейшие идеи были направлены прежде всего на более глубокое понимание метода Фейнера-Гончарова, его систематизацию, его возможности для использования в более широком классе задач. Таким образом, две теоремы из § 3.2 и были посвящены как систематизации метода (теорема 6 и примеры в конце параграфа), так и некоторому применению общей систематизационной теоремы для более частного класса задач. Так, теорема 7 дает пример нахождения для произвольной формулы К[х) теории слабого второго порядка, задающей идеал на Б А, такой конструктивной БА, что в любой её конструктивизации предикат К (х) не разрешим. И приведен пример использования последней теоремы — построение конструктивной Б А, у которой в любой конструктивизации идеал Ершова-Тарского не разрешим.
В качестве далеко идущей цели — хотелось бы сформулировать более естественные и общие условия для обобщающей теоремы б и использовать полученный метод как универсальный инструмент для построения различного рода алгоритмических контр-примеров как на булевых алгебрах, так и на других алгебраических объектах.
И в конце проделанного труда мне бы хотелось выразить теплые слова признательности математикам, оказавшим значительное влияние как на постановку проблем в самом начале пути, так и на дальнейшее развитие результатов в поздние годы.
Это, прежде всего, благодарность моему научному руководителю Сергею Саво-стьяновичу ГОНЧАРОВУ, —- благодаря помощи, настойчивости и терпению которого на продолжении нескольких лет, собственно и состоялся этот труд, равно как и развитие большого математического направления по исследованию конструктивных булевых алгебр, в чьем общем русле были проведены все исследования.
Также автор выражает искреннюю признательность молодому коллективу семинаров «Конструктивные модели» под руководством С. С. Гончарова за полезные замечания при обсуждениях работы.
