автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.17, диссертация на тему:Оценки и пучки: теоремы переноса

Ч ■: Ь • .

АКАДЕМИЯ НАУК СССР ИНСТИТУТ ПРОБЛЕМ ПЕРЕДАЧИ ИНФОРМАЦИИ

Специализированный совет Д.003.29.01

На правах рукописи

ЛЮБЕЦКИЙ Василий Александрович

УДК 510.67:512.57+681.3+519.76

ОЦЕНКИ И ПУЧКИ: ТЕОРЕМЫ ПЕРЕНОСА

05.13.17 - теоретические основы информатики, 01.01.06 - математическая логика, алгебра и теория чисел

Автореферат диссертации на соискание ученой степени доктора физико-математических наук

Москва - 1991

Работа выполнена в Институте проблем передачи информации Академии наук СССР

Официальные оппоненты - доктор физико-математических наук

профессор Е.А. Палютип,

доктор физико-математических наук профессор В.Г. Каиовеи

доктор физико-математических наук профессор А.В.Чернавскин

Ведущая организация - Ленинградское отделение

Математического института АН СССР

Защита состоится

сГуи\ 1991 г в

часов на заседании Специализированного совета Д.003.29.01 при Институте проблем передачи информации АП СССР по адресу: 101447, Москва, ул. Ермоловой, 19.

С диссертацией можно ознакомиться в библиотеке Института проблем передачи информации АН СССР

Автореферат разослан

1991 г.

Ученый секретарь Специализированного совета, доктор технических наук, профессор

1 О

С.И. Степанов

1 7 ¿3

ОБЩИЙ ОБЗОР И ХАРАКТЕРИСТИКА РАБОТЫ

Тема работы относится к изучению теоретико-модельных методов; в теории доказательств, в алгебре, а также относится к теоретическим основам информатики. Предметом исследования являются две традиционные проблемы: о переходе от выводимости в классической теории к выводимости в интуиционистской теории н о построении модельного компаньона; на основе исследования этих проблем получены алгоритмы, компьютерно реализуемые в "реальное время" и связанные с задачей эффективизации (т.е. задачей извлечения явной конструкции, терма, 'программы из доказательства) и задачей обобщенного описания; эти задачи относятся к традиционным темам исследований в области theoretical computer science. Решения и алгоритмы основаны на методе, предложенном автором, - методе семантического оценивания.

В главе I излагается упомянутый метод. На его основе в главе II строится широкий класс формул в языке колец, для которых из их выводимости в классической теории множеств Цермело-Френкеля ZF следует их выводимость в

интуиционистской теории множеств ZFI', сформулированной Х.Фридманом Ш. Алгоритм перехода от исходного доказательства к соответствующему интуиционистскому доказательству компьютерно реализуется в реальное время. В главе III на основе того же метода получена явная и общая конструкция, которая для многих классов колец позволяет образовать соответствующие им модельные компаньоны. Причем алгоритм перехода от класса колец к его модельному компаньону также компьютерно реализуется в реальное время. Это и создает основу для использования этих алгоритмов в связи с упомянутыми выше темами из theoretical computer science.

Для решения континуум-проблемы П.Д. Коэн в 1963 году предложил существенно новый метод (хотя частично и основанный на идеях КГеделя) - метод вынуждения (форсинга). Затем П.Вопенка, Д.Скотт и Р.Соловей оформили его в общем виде 12]. Они ввели понятие булевозначного универсума V®, где В - любая полная булева алгебра. В середине 70-х годов

Р.Грейсон развил метод Козна дальше, определив понятие гейтинговозначного универсума V^, где £2 - любая полная гейтингова алгебра (такова, например, любая топология -решетка всех открытых множеств топологического пространства). Причем он построил V^ средствами интуиционистской теории множеств ZFI' [31. В таком виде метод Коэна вобрал многие черты теории топосов.

Долгое время метод Коэна применялся исключительно для доказательства независимости разного рода гипотез от аксиом теории множеств, т.е. для доказательства невозможности некоторых рассуждений. Затем был обнаружен подход, позволяющий использовать метод Коэна наоборот для решения некоторых (в том числе, старых) проблем, т.е. для доказательства возможности некоторых рассуждении, см., например, [4,51. В данной работе метод семантического оценивания (который также находится в рамках направления, идущего от метода Коэна) используется, в частности, для построения эффективно реализуемых алгоритмов.

На основе метода семантического оценивания в главах II к III единообразно рассматриваются следующие две, на первый взгляд, далекие друг от друга проблемы, связанные с именами П.С.Новикова и А.Макинтайра.

Пусть буквы LEM обозначают схему аксиом закона исключенного третьего <ри-нр. В 1939 г. П. С. Новиков (6] сформулировал теорию "Аг", которая описывает кольцо Z целых чисел в некотором расширении языка обычной арифметики. И показал: если "Аг"ь ЗпР(п), где здесь и далее Р бескванторная формула, то ("Ar"-LEM)h 3nP(n) и можно явно предъявить "решение" - целое число Пр, для которого ("Ar"-LEM)ь P(n0>.

Около 1930 г. А.Н.Колмогоров и КГедель получили такой перевод (р и* <р формул <р обычного исчисления предикатов PI в формулы ф~ того же исчисления, что: если Pit- <р, то (PI-LEM) ь <р . Этот перевод совершенно явный: в определенных местах формулы ip нужно добавить некоторое число раз выражение п. Они (и Г.Генцен) по существу получили такой же результат и для пеановской арифметики Аг вместо PI. Аналогичный

результат был получен Д.Майхиллом для теории типов в 1974 году, Х.Фрндманом для теории множеств ZF в 1973 году (и В.Пауэллом также для ZF в 1975 году). Принципиальное отличие всей этой цепочки результатов от результата П.С.Новикова и результатов его последователей состоит в том, что: 1) перевод Колмогорова-Геделя существенно меняет смысл исходной формулы <р, и если, например, tp - утверждение из алгебраической теории чисел, то просто неясно содержание утверждения <р~, 2) принципиальное достоинство интуиционистской теории состоит в ее эффективности (т.е. в наличии свойства экзистенциальностн, см. 17,81); но интуиционистская доказуемость формулы -пЭху(х) не влечет возможность предъявить соответствующее "решение" Xq.

Результат П.С. Новикова, как и результат Колмогорова-Геделя, был развит многими авторами. Так, геделевская функциональная интерпретация показывает: если Art- Vx3yP(x, у), то (Ar-LEM)i- Vx3yP(x,y). Спектор, Жирар и Правитц (с помощью функционалов конечных типов и нормализации доказательств) получили такой же результат с заменой теории Аг на теорию типов. Пусть далее везде буква К обозначает теоретико-множественную переменную, пробегающую класс всех колец (т.е. К=<К, +,-,-, 0,1>) и запись (plj-означает интерпретацию формулы <р языка колец в кольце К. Конечно, - уже формула в языке теории множеств. Пусть

к( •) - какая-то формула в языке теории множеств н ф АЕ-формула в языке колец, т.е. формула вида ч УхЗуР(х.у). Обозначим <; ч VK (к(Ю [0]^). Х.Фридман показал [91: если ZFh С,, то ZFI'ь где к( •) - та конкретная формула в языке теории множеств, которая описывает кольцо Z.

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

В главе II показано: если ZFh С,, то ZFI' и С,', где формула к1*), входящая в вышеуказанную формулу С. описывает (детали см. ниже) любое счетное кольцо или любой класс счетных колец (или еще некоторые несчетные кольца, или их

классы). В частности, и кольцо 2, как в результате Фридмана.

А формула С

совпадает с С 'для неразложимых или счетных колец , или в случае хорновости формулы ф) или близка по смыслу к формуле С (для произвольных колец и произвольной ф). Иными словами, мы разрешаем в формуле £ многие разные посылки •) вместо одной конкретной в результате Фридмана.

Кроме того, в главе II показано: если формула £ утверждает, что некоторая теорема ф верна в классе (например) всех тел, то формула утверждает, что эта же или близкая к ней теорема ф' верна в (гораздо более широком) классе всех строго регулярных колец (определения см. в 121.201).

В качестве следствия этих результатов получаем: по классическому доказательству существования какой-то функции y=f(x), удовлетворяющей условию [VxP(x,f(х)) 1 ^ , можно явно (алгоритмически) предъявить "решение" - программу одной конкретной вычислимой функции fp, в том же смысле удовлетворяющей предикату Р, см. 171. При этом предикат Р не обязательно разрешим: он может включать, например, термы в языке теории множеств, описывающие операции +,-,•• Конечно, вопрос о сложности такого предъявления не прост и зависит от разных ограничений.

Важно заметить, что АЕ-формула ф и даже АЕ-хорнова формула ф (где Р(х,у) - бескванторная формула) может описывать весьма нетривиальную функциональную зависимость у от х. Например, такие формулы описывают теорему Лина-Зайденберга, теорему Гильберта о нулях, теорему Артина о положительном решении 17-ой проблемы Гильберта и т.д.

В начале 50-х годов А.А.Марков выдвинул тезис: если Vx,y(P(x,y)unP<x,y)> n Vx-n3yP( х, у), то УхЗуР(х.у), -который получил название: "принцип Маркова". Принцип Маркова играет большую роль в интуиционистском (конструктивном) направлении в математике. Ему соответствует известное правило Маркова: если int h n-i3yP(x, у), то int н ЗуР(х.у), где intb обозначает интуиционистскую выводимость в подразумеваемой теории и Р(х,у) - разрешимый предикат.

Указанные выше результаты можно рассматривать как обоснование принципа (правила) Маркова или близких к нему утверждений. (Иногда в такой ситуации говорят о принадлежности формул £ классу Гливенко-Новикова.)

Задачу эффективизации мы обсуждаем на примере задачи построения движения (задачи навигации). Эту задачу, в частности, можно описать так: дана спецификация траектории (дано описание двигательной задачи) и нужно явно построить траекторию (решить эту задачу). Она исследовалась как концептуально, так и в плане построения многочисленных конкретных алгоритмов, например, в [10-14,28]. Одна из ее возможных постановок такова. По описанию Т (параметров) сцены и описанию ф s Vx3yP(x,y) требований к траектории y=f(x), т.е. по формуле Тнайти программу такой вычислимой функции fQ, что T*»VxP(x,fQ(x)). Афферентная информация преобразуется в эфферентную информацию fg,

по-видимому, с участием промежуточного "языка рассуждений". Полученные в главе II результаты позволяют уточнить постановку этой задачи и получить эффективный, в реальное время работающий алгоритм обработки информации в промежуточном языке. А именно: алгоритм, который переводит рассуждение о возможности "движения" в интуиционистское

рассуждение об этом (и, следовательно, в определенную программу движения). Здесь Р(х,у) может некоторым образом содержать логические связки и кванторы.

Перейдем к характеристике содержания главы III. Известно теоретическое и прикладное значение теорий, допускающих элиминацию кванторов (А.Тарский, около 1950 года). Но такие теории весьма редки. Обобщением понятия о теории с элиминацией кванторов является понятие о модельно полной теории (А.Робинсон, начало 50-х годов). Для такой теории Т всякая формула эквивалентными преобразованиями приводится, хотя и не к бескванторному виду, но все еще к очень простому виду. Скажем подробнее. А.Робинсон определил понятие модельного компаньона Т теории Т, и была надежда, что существует достаточно много теорий Т, имеющих модельный компаньон Т*. (Теория может иметь не более одного модельного 2- <789

компаньона.) Сначала были известны только отдельные примеры таких теорий Т. После 1969 г. значительные усилия были направлены на поиск общих конструкций для получения модельных компаньонов (например, с помощью компаньон-операций). Это делалось н на основе соответствующего развития метода вынуждення. В это же время формируется направление, которое А.Макинтаер в 1977 г. еще называет "неисследованные пути изучения", 115,с.1741. А именно, Карсон [161, Липшиц и Сарацино 117], а также Макинтаер (181, Вайспфенинг 1191 с точностью до небольших различий получили следующий результат. Пусть Ф - модельно полная теория, включающая аксиомы поля, а Т - теория класса Хф всех безатомных колец, составленных из всех глобальных сечений (пирсовских) пучков со слоями, которые являются моделями теории Ф. Утверждается, что тогда Т - модельно полная теория. Например, если Ф - теория всех алгебраически замкнутых полей, то Т - теория всех безатомных коммутативных регулярных (по Дж.Нейману 120,211) алгебраически замкнутых колец. Любой класс Хф, определенный так, как в этом результате, содержится в классе коммутативных регулярных колец. В (15,181 А.Макинтаер ставит проблему расширения этого результата на случай, когда класс Хф выходит за пределы класса коммутативных регулярных колец. А именно, пусть Ф - любая теория колец, имеющая модельный компаньон Ф , и класс Хф колец определяется по Ф точно также, как выше (повторим определение: Кф ü (К |Vp(Ф)j- ), где Кр -

произвольный слой упомянутого пучка кольца Ю. В этом случае имеет ли класс Хф модельный компаньон (который мы обозначаем Хф) и какова аксиоматика класса Хф ? По этой проблеме и близким вопросам можно найти некоторые результаты и исторического плана замечания, например, в [22-241.

В главе III (при некоторых неограннчительных условиях) дается положительный ответ на этот вопрос и приводится работающий в реальное время алгоритм, который по теории Ф (точнее по Ф ) порождает аксиоматику теории ThX^.

Задача обобщенного описания (как часть задачи или

процесса обобщения) изучалась концептуально и в связи с многочисленными конкретными постановками, например, в (25-29). Эту задачу, в частности, можно описать так: дано (подробное) описание обстановки, и мы хотим перейти от него к (в том или ином смысле) простому описанию, согласованному с исходным. Здесь ключевые слова: "простое" и "согласованное". В качестве модели такого перехода рассматривается переход от описания (теории) Т к описанию (модельному компаньону) Т . В этом случае "простое" означает: нередко теория Т допускает элиминацию кванторов и во всяком случае любая формула эквивалентными относительно Т преобразованиями приводится к очень простому виду. В этом случае "согласованное" означает, в частности: если Тд^ь <р, то Т ь <р, где Тд^ - теория, состоящая из всех АЕ-следствий теории Т, а <р - любая формула.

Более подробная постановка возникает в связи с моделированием интеллектуальных процессов. Описание Ф сцены актуализирует некоторое множество "элементарных модулей'' К, образующих внутреннюю структуру (условно говоря) поведенческой системы. А именно, актуализирует множество Хф, которое описывает (текущую, но с учетом предыдущего опыта) актуальную модель обстановки. В §5 приложения рассматриваются более подробные способы ее описания. Поведенческая система "апроксимирует модуль" Кф "модулем" Хф и рассматривает описание Т « ТйХф , как обобщенное описание афферентного описания Ф. Например, в связи с описанием параметров сцены. Эта модель задачи обобщения допускает эффективную компъютерную реализацию (как и основанная на ней более подробная интерпретация представлений о поведенческой системе, изложенная в §5 приложения).

Отметим также (например, в связи с пруверами), что для довольно широкого класса формул <р' (включающего все Ь-формулы, см. 1301) вопрос о выводимости <р' в теории Т редуцируется в реальное время к вопросу о выводимости формулы ф, соответствующей <р', в (более простой) теории Ф .

Отметим, что показанная в работе возможность на единой основе рассматривать как вопросы эффективизации

(конструктивизации) рассуждений, так и вопросы теоретико-модельной алгебры, соответствует известным положениям, см. 131]. Отметим также работы [32-34], дополняющие эту часть реферата. Наконец, упомянем несколько книг, в которых обобщены работы, стимулировавшие прикладные интересы автора 135-391.

Результаты диссертации излагались автором в пленарных докладах на 7-ой и 10-ой Всесоюзных конференциях по математической логике (Новосибирск-1984, Алма-Ата-1990), на международных конференциях (3альцбург-1983, Варна-1988, Новосибирск-1989, София-1989, Варна-1990), международном коллоквиуме (Караганда-1990) и на Российской школе по основаниям математики (Саратов-1989). Докладывались на Симпозиуме по математической логике и ее приложениям (Бразилия-1989), на Логическом коллоквиуме'89 (Берлин-1989) и Логическом коллоквиуме'90 (Хельсннки-1990). А также подробно излагались автором на научных семинарах Ю.В.Матиясевича (ЛОМИ), Л.А.Бокутя (ИМСОАН), Ю.Л.Ершова и Е. А. Пал юти на (ИМСОАН).

Основные результаты диссертации опубликованы в работах [41-65].

СОДЕРЖАНИЕ РАБОТЫ

Работа содержит 3 главы и приложение, всего 20 параграфов. В диссертации доказываются 15 теорем, нумерация которых сквозная; остальные утверждения нумеруются по параграфам. Автор рассматривает как основные, следующие три результата: метод (предложения 5,6,7в,8,10,12 из §1.6 и предложение 3-4 из §1.8), переход к интуиционистской теории (теоремы 2-4) и построение модельных компаньонов (теоремы 10-12).

В главах 1,11 все утверждения понимаются, как утверждения о выводимости соответствующих формул языка 2? в интуиционистской теории множеств 271' или как чисто финитные утверждения о наличии явно указываемой

примитивно-рекурсивной функции, которая преобразует одни выводы в другие. В отдельных случаях явно оговаривается

использование в выводе аксиомы LEM. В главе III все утверждения понимаются, как утверждения о выводимости соответствующих формул языка ZF в обычной теории множеств ZFC (хотя многие из них фактически выводимы и в теории ZFI").

Символ * означает "равно по определению" или "эквивалентно по определению".

Глава I содержит утверждения, составляющие метод семантического оценивания. В §§1-3,5 и частично в §4 напоминаются известные понятия и результаты, вводятся обозначения. В §4 известный результат

Даукера-Пейперта-Избела-Фурмана-Скотта 140) приводится к виду нужному в дальнейшем.

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

операций: ejnej * ei'e2- elue2 * ei+e2_el'e2' "ie 4 c

наибольшим элементом 1 (единица кольца) и наименьшим элементом 0 (нуль кольца). Здесь и далее буква е с индексами или без них обозначает произвольный элемент из В(К).

Кольцо К назовем нормальным, если выполняется (Ф}'^. где <Pj * Vk3eQVe (e-k=0 » eseQ).

Обозначим Э"(К) множество всех идеалов в алгебре В(К). Это множество является полной гейтинговой алгеброй относительно порядка: а^Ь <* aSb. J-оператором называется отображение J: У(К) - У(К), обладающее свойствами: asJ(a) = JJ(a) и J(anb)=J(a)nJ(b) для всех a,b€?(K). Множество всех J-операторов обозначается А(К), оно • образует полную гейтннгову алгебру относительно порядка: J ^ «

Va( J^(a)sjg(а)). Обозначим 2ИК) подалгебру в алгебре А(К), состоящую из всех стабильных в А(К) элементов, т.е. из всех таких JeA(K), что (-п)д J = J. Здесь и далее отрицание -iu определяется как (и-0), а импликация (u-v) определяется как UiueSl |unwsv) для любой полной гейтинговой алгебры П и любых ее элементов u,v. При этом 3(К) - полная булева алгебра (иногда ее называют топологическим пополнением исходной алгебры В(Ю) и В(К) вкладывается в St К) по правилу е Je,

.?- /7S9

где Jg(a) s <e>ua, Jg: 9ЧК) - Э"(К). Предложения 1 и 2 из §4 содержат полезные для дальнейшего свойства этих алгебр.

В §5 напоминается определение пирсовской локализации Кр

кольца К в точке р, где р пробегает X(К) - множество всех

простых идеалов в алгебре ВСЮ. А именно, Кр ч К/р, где р *

р-К - идеал в К. Запись {К означает VpeX(K) (pl^P)^ ,

Р Лр

где <р — любая формула в языке колец, а Е=<к^, . .., kn>eK и Jcp=<k?.....кР>. и * lkilp €Кр.

В §6 определяются два важных для нас отображения. В дальнейшем такого типа отображения мы называем оценками (общее определение оценки дано в начале §6). Первое из них является отображением вида Я(К) - ЗЧК), где Я(К) - множество всех предложений в языке колец с множеством К в качестве множества параметров. А второе является отображением вида Я(К) - 2(К). Этн отображения обозначаются соответственно ['Зд- и C'3<g- Для атомарного предложения k=t обе оценки определяются одинаково: [k=t3y и [k=t3g ч {ееВ(К) jе• k=e-1> еУ(К)£2(К). Если k,t - полиномы, то они заменяются на их значения, вычисленные в кольце К. Затем эти отображения продолжаются на все множество Я(К) обычным образом: «

№Jy п Е03у. Охр]у - Uj{k€K |ti>(k)3j> и аналогично для всех других пропозициональных связок' и квантора V; второе отображение определяется точно так же, но вместо операций в^ Э" < К > используются (в правых частях равенств) операции в 2(К). Первая из этих оценок определена в 1401.

Интуитивно каждую оценку можно рассматривать^ как

некоторую семантику, как "мир смыслов параллельный" обычному миру истинности н миру выводимости. Этот тезис будет постепенно раскрываться дальше. Пока отметим, что оценка [-3у замкнута относительно интуиционистской выводимости в теории колец, а оценка С-3g замкнута относнте.льно классической выводимости в теории колец, т.е. выполняется: во-первых, [рЗу =1 н ¡Mj =1 для всех интуиционистских или соответственно всех классических аксиом <р\ и, во-вторых, если ti)3 -1 и =1, а Ф получается из <p,\ji по одному из правил вывода, то [03 =1. Поэтому: если int ь <р, то IMj- =1;

если I- <р, то [ВД3 =1, где 1пЬн обозначает интуиционистскую выводимость, а I- обозначает классическую выводимость (в некоторой подразумеваемой теории). Суть нашего подхода в том, что семантики 1 н <р и н <р тесно связаны с предикатами (ф)^ , [фЗд- =1 и ВД!^ =1, которые в свою очередь тесно связаны между собой.

В предложении 1.§6 проверяются свойства оценки [-Цд-. В предложении 2. §6 приводится удобная для нас форма интуиционистского определения по рекурсии. Предложения 3,4§6 содержат нужные нам свойства произвольных оценок.

В предложении 5.§6 (с использованием ЬЕМ) для нормального кольца К доказаны соотношения:

<|[р<Е>3?(К) ЗР> *» Криу>(1ср), Ур€Х(К). (1)

для любой формулы <р в слабо нормальной форме (см. ниже);

и (Ур2<е> (Кр^(1(Р))) =» (|[¥>(Ю]|у г<е>) (2)

для любой АЕ-формулы р и любого ееВ(К), где р пробегает Х(К).

Формула <р называется "в слабо нормальной форме", если область действия любой входящей в нее импликации не содержит кванторов. АЕ-формулой называется формула в предваренной

форме с префиксом Ух|,...,хп3у^.....ут- Формула называется

фи-формулой, если в посылке любой ее импликации: во-первых, нет квантора V и, во-вторых, квантор 3 не входит в область действия какой-либо связки Позитивной называется формула, не содержащая связку =»; (Отрицание -1 <р везде понимается как ) Хорновой' называется формула, полученная из атомарных формул с помощью навешивания связок п,3,У и операции образования формулы где р - позитивная, а >р - хорнова

формула. Формула называется "в слабо импликативной форме", если в посылке любой ее импликации нет импликаций. Теория, состоящая из формул некоторого одного типа, называется по имени этого типа формул. Например, фн-теория - любое множество фи-формул.

В предложении 6.§6 для любого нормального кольца К доказаны соотношения:

Г^Зу - ЕДд для любой фи-формулы ф с параметрами (3) и, если Е!//]]^ га, то [й^ £а для любой АЕ-формулы 0 (4)

с параметрами и любого аеЭ"(К).

Заметим, что для любого кольца К выполняется: если <р - позитивная формула, то влечет =1, а если

0 - хорнова формула, то £0]у =1 влечет (5)

В определении 7.§6 вводится понятие почти позитивной и К-разрешимой формулы. Класс таких формул существенно расширяет класс позитивных формул. В предложении 7в.§6 доказано: для любой почти позитивной и К-разрешимой формулы <р, если то |=1. (6)

В определении 8.§6 дается следующий перевод формул <р языка колец в формулы того же языка (напомним: е.ец.е^^ - свободные переменные, пробегающие В(Ю): «» е-к=еЧ,

1<рпф)'е * <р'е п ф'е, «= Зх^, •» Ухрц, Уе0

((е0£е п ) » '^'е " Зе1,е2 ((е=е1ие21 п

Обозначим р' и и Т' * {<р' |р€Т), где Т - любая

теория. Заметим, что класс {<р' \<р) содержит известный класс

Ь-формул, определение Ь-формулы см. в 130). В предложении

8.§6 для любого кольца К доказывается:

'^е'^'к в (ее|[¥>(1с)3у) для любой формулы <р (7)

с параметрами и любого ееВ(К) н, если <р в слабо

импликативной форме, то <р'е - хорнова формула. (8)

Этот перевод оказался алгебраически содержательным.

Например, если ч> * "быть телом", то • Ук31 (к^ • 1=к).

Последняя формула определяет класс строго регулярных (по Дж.

Нейману) колец. Если <р говорит "коммутативное" или

"алгебраически замкнутое" кольцо, то <р' говорит

соответственно то же самое. В предложении 9.§6 доказано:

пусть <р - бескванторная формула в дизъюнктивной нормальной п

форме, т.е. ч> 'кц^ц п ... п Гц«^ п ...); свойство <(р' )|г эквивалентно тому, что кольцо К представимо в виде прямого произведения К 2 и в сомножнтеле К^ "выполня-

ется" 1-ый дизъюнктивный член. Последнее означает:

выполняется каждое его равенство ..... а каждое его

неравенство Гц^ц.'-- выполняется в любом ненулевом сомножителе Ь представления К^ в виде прямого произведения

KjSLxR. Если формула ф в предваренной форме, т.е. ф ч Qi>, где <р - бескванторная формула, то ф' = Qlip'). Если К -неразложимое кольцо (т.е. В(К)=<0,1)), то (<р « V''^- То же самое выполняется для любого кольца К и любой h-формулы <р. Сравните с (5).

Наконец, в предложении 10.§6 для любого кольца К доказано: если то (" >j^i всегда верно (Фз')^ если

(1)к, то

(1')'к и (9).

Здесь пары символов <i,i'> (1=2,3,4,5) обозначают следующие пары свойств: строго бириккартово ~ первичное (1=2), биригулярное ~ квазипростое (1=3), строго регулярное - тело (1=4), строго риккартово - без делителей нуля (1=5).

Напомним некоторые из этих определений: 2 * Vk3e (<k> = е-К), 2' « Vk,r (Vt(k-t-r=0) * k=0 и r=0), 3 * Vk3e (<k> = e-K), 3' * Vk3pj.....Pjj.qj.....(k=0 и 1= Pj-k-qj + .-.t

Pn'k-qn), 5 ч Vk3e (k* =e-K). Здесь a* - правый анулятор

идеала а или элемента а.

В доказательстве теоремы 1.§6 в самом простом случае показано, как работают эти оценки. А именно: пусть н (1'пр •* ф), где 1=3,4,5, а <р - фи-формула и ф - АЕ-формула. Допустим К - любое кольцо и выполняется (1пр' Тогда по (7) получим

=1. а по (9) получим Ei'3y =1 и (Ф^^- По (3) получим [I'r^Jg В силу замкнутости оценки E"i<g относительно

классической выводимости получим =» =1; это

эквивалентно тому, что [i'rwOj 5 EVGlg- Поэтому [0J<g =1 и по (4) имеем =1. По (7) получим Ф'ц- Итак, мы явно указали

интуиционистское рассуждение, которое показывает: VK ((inv') *ф')к.

В §7 в основном повторяются результаты работы [31. Дело в том, что нам нужны главные конструкции этой работы, но с определенными изменениями в них, и заранее неясно, что после таких изменений сохранятся нужные нам свойства. В §7 определяется гейтииговозначный универсум V®, где £2 - любая полная гейтингова алгебра, оценка C'ljj ZF(V^) - £2 ^отображение в алгебру £2 класса всех предложений языка ZF с

i7Sa

классом Vn в качестве класса параметров). А также определяется вложение ( • )v : V - V (интуиционистского) класса V всех множеств в класс V®. Эти определения отличаются от тех, которые даны в 13). Затем доказываются нужные нам свойства этих понятий. В дальнейшем в качестве О обычно берется алгебра ЗЧК) или алгебра 2(К).

В §8 определяется нестандартное представление кольца К, а также нестандартное представление каждого элемента к из К. Они обозначаются соответственно К' и Рь.. Нестандартное

m

представление кольца К это такой элемент К' €V , что для любой формулы çkx) в языке колец и любых параметров ЕеК выполняется:

tï)(Ic)l2 = t(P(Pk)K.3s(K). (10)

Здесь Ic=<k|,... ,kn> и Pjt=<P)c ,..., Р^ >, а Р^ - функция вида

v П ^

Pj, (t ) ъ [k^=t3g-, где ее аргумент t пробегает множество

v ЗНК)

{t |teK). При этом . Часто вместо Р^ пишут kj.

Такие элементы К' и Pt удается определить только для случая

3-кольца. Последнее означает следующее условие на кольцо К: [ky=tv32(K) s [k=t3j, Vk.teK. ST-кольцом называется кольцо К, удовлетворяющее условию:

[ky=t']|y(K) a [k=t]?, Vk.teK. Нормальное 2-кольцо назовем (*)-кольцом, а условие "быть (»)-кольцом" будем записывать »(К). Предложение 4.§8 поясняет, что представляет собой К'. А именно, определим функцию h(<ky,P|c>) s 1, VkeK. Тогда [h: Kv - К' гомоморфизм "на", его ядро равно Pq£Kv и K'/Pq s К* ю =1-

Формулу к(-) (описывающую кольцо К=<К,+,-, -,0,1>) в языке ZF назовем абсолютной, если ZFI' h VK (к(К) =» (Ck(Kv/Pq)]j^j =1)). Обычные формулы, описывающие обычные кольца Z,Q,A,M2<Z) ,Н и многие другие такого типа кольца, являются абсолютными. Просто потому, что в этих случаях Pq=<0v}, а к(К) =» ([(C(KV)3S(K) =1) для обычных формул к(-).

В главе_П основным является §1. В §§2,3 мы распространяем результаты §1 на случай кольца, не являющегося нормальным. Хотя при этом возникают, новые

содержательные случаи, формулировки становятся более грамоздскими.

Пусть х=<х|.....хп> - фиксированный список переменных и

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

Предположим, что теория Т. состоит из фи-формул, а есть АЕ-формула. Запись вида 1Т(х) |/»(х)]^ означает УЕеК (Т(£) =» Заметим что, например, любое нормальное

кольцо К со счетным носителем удовлетворяет условию *(К). В работе приводятся также примеры У-колец (в частности, любое 3-кольцо является и У-кольцом). Формула Фд в языке колец говорит: "любой центральный идемпотент равен 0 или 1".

Теорема 2.

а) Пусть 2?!' н УК [Ф^Фд.Кх) => <р(х))к. Тогда 2Т1' н УК (К есть 3-кольцо =» [ф|,Т'(х) =» р'(х)]^). Формулу Ф| можно одновременно опустить в посылке и заключении.

(Таким образом, в любом интуиционистском рассуждении "аксиома" Фд элиминируется.)

б) Пусть 2¥ н УК 1Т (х) => 0(х)1к . Тогда:

1) 2П' ь УК (*(К> * (Т ' (х) ^ ф' (х))к) и

2) гП' н УК (*(К) * [Ф3,Т^(х) * ^(х)1к).

(Таким образом, в классическом рассуждении аксиома ЬЕМ элиминируется.)

в) В пункте а перед связкой =» можно одновременно дописать: в посылке формулу 1', а в заключении формулу 1, где 2,3,4,5. В пункте б перед связкой можно одновременно дописать: в посылке формулу 1', а в заключении формулу 1, где 4= 3,4,5. В обоих пунктах (в заключениях) можно опустить (•)', если Т.Т^ Ь-теории и у>,0 1»-формулы; (•)' можно опустить у формул если они хорновы.

г) В предыдущих пунктах длина вывода в заключении линейно зависит от длины вывода в посылке.

(Пункты в,г усиливают пункты а,б, как и теоремы 3,4.)

Теорема 3. Пусть Т,Т^,(р,0 - такие же теории и формулы, как в теореме 2. Пункты а,б теоремы 2 остаются верными, если в их заключениях заменить Т' на Т, одновременно добавив (там же) условие К-разрешимости теории Т(х) (или вместо этого метаматематически предположив, что Т(х) - позитивная теория).

Теорема 4. Теоремы 2 и 3 верны, если в них вместо УК....

написать УК (к(К) ____), где к( •) - любая абсолютная

формула в языке 2?.

Эти три теоремы (и их доказательства) в сущности представляют собой один результат, изложенный в нескольких вариантах. Из него получаем следствие 1 и легкое следствие 2:

Следствие 1. Пусть гГь У+,-,-,0,1 1Т (х) * +,-.*.0.1' Тогда 2П' у У+.-.-.0.1 [* <х> + _ . о 1" <И то же самое в форме теоремы 4.) Следствие 2 (ЬЕМ). Здесь Т фи-теория. Обозначим Ху * {К |(Т)К) и Хр. х <К |(Т')К п <<«УК>. Если К^ф, то =ф' и, если ф - хорнова, то (Заметим: пусть Т" ■» Ф|; для

позитивной теории Т выполняется ,а также (К | (Т)^ п Т

есть К-разрешимая) £

Перейдем к §2. Формула называется "в слабо А-нормальной форме", если посылка любой ее импликации не содержит У и ■>. Формула называется "с тесными отрицаниями", если она содержит импликацию только в форме отрицания атомарных подформул. Кольцо К назовем "с отделимостью", если ЭйеУ

УкДеК [ (СРк*Р11Я(К) * Е<Рк.Р1>€%(К)> л С(<Рк'Рк>€#32(К)

=0)1.

Вместо <Рк,Р,.>е# будем писать Р^ИР^. Объект # называется отделимостью кольца К. Определим перевод <р е-» Цр (где <р -формула в языке колец с тесными отрицаниями) как замену всех подформул вида к*1 на формулы к#Ь.

Теорема 5а. Пусть Т - теория в слабо А-нормальной форме в языке колец и ф есть АЕ-формула с тесными отрицаниями в том же языке. Тогда в гП' выводимо: если К есть 3-кольцо с отделимостью, то I ([1Т(1с)=>0(1с) * к» З^с К> *

(|1Т(1с)ч0,{(К>]к.Зу(|;) =1)1, уКеК. Перевод (р н* <р' легко продолжается на формулы вида фи

тогда теорема 5а переходит в утверждения вида: если ZF и 1Т<х)=*/|(х)1к , то 1- [Т'(х)^#'(х)1к , которые доказываются в теореме 5б-в.

Напомним, что для любого объекта ЬеУ^ такого, что [<Ь, +,-,•,0,1>-кольцо]|д =1, определяется "внешнее" кольцо Ь следующим образом: Ь в {geVn =1) и (1^ + ^^ *

А

[<1^ 12» 1>€+1д =1 для любых 1^,12,1еЬ , и также для других

л л л л

операций. Получаем структуру Ь ч <Ь ,+ ,0,1> (где [0-нуль в Ь, 1-единица в ЬЗд =1), которая действительно является кольцом. При этом объекты Ь к Ь называются соотвественно внутренним и внешним кольцами. Один из способов задания отделимости состоит в рассмотрении колец К с "метрикой" вида Г: К - Ь , где Ь - "хорошее" внутреннее кольцо в В качестве такого I. можно брать, например,

объект - кольцо всех дедекиндовых вещественных чисел в V или объект (У Здесь У - (локально компактное и строго разрешимое) топологическое кольцо, а терм '''у обозначает операцию пополнения топологического кольца (этот

<Т( К) у

терм рассматривается в V и применяется к кольцу У ). Второй нз этих случаев рассматривается в 83.

Аналогично определяются объекты и (у")^ из У^ для любой фиксированной полной гейтинговой алгебры П. Знак ()у в дальнейшем опускается. Прежде всего возникает вопрос, что представляют собой кольца (К^) и (Уд) . В частности, в том случае, когда П * Э"(К). Ответим на него с использованием ЬЕМ.

Предложения 1.§2,12.§3. Пусть £2 - любая полная гейтнигова алгебра и X - ее стоуново пространство. Тогда

(КП)Л 3 СП<Х,Ю и (Уд)" з СП(Х,У). Здесь У - любое указанное выше топологическое кольцо (в частности, У может равняться К). А выражение Сд(Х,У) обозначает кольцо всех непрерывных функций вида Г: - У, где - открытое П-плотное (см. ниже) подмножество в X; эти функции рассматриваются с точностью до совпадения на пересечении их областей определения. Множество СКХ называется П-плотным, если ЗА5П (0=КА г\ и^А =1). В

частности, обычное кольцо С(Х,У) естественно вкладывается в Сф(Х,У). Если 12 - топология любого пространства 2, то Сд(Х,К) £ С(2,К), где £ есть (поточечный при некоторых ограничениях на 2) кольцевой изоморфизм. Таким образом, мы определили (существенное) расширение класса всех алгебр вида С<г,М.

Вернемся к отделимости. Отделимость во внутреннем кольце Ид определяется как (к#П в Кк-И^ >0], где кДеКд. Предикат к<Я говорит "к не равно I с подтверждением". Итак, отделимость в кольце К может задаваться, например, с помощью "регулятора" - отображения Г: К - (Х,К), для которого

выполняется: СР^Р^акю - Шк>=П1)]|2{К), ЕР^Р^ ®

=1, ЕРк=Р13?(К) 5 |ЦИк)=т);А5Ш для любых к, 1еК. Определим "внутреннюю" функцию

(соответствующую внешней функции Г) как Г_(, Г С к) >) * 1

для всех к из К. Тогда Г_€УУ(К) и |[Г_: К' - Крвш =1-Обозначим (к-и * (ГСк>^Г(1)) «5 (Пк)-ПШ2 <с, где кДеК и переменная с пробегает все рациональные строго положительные числа. В терминах внутренней функции это означает, что Г_( Р^) - Г.СР^. Здесь мы имеем хорошо известное в конструктивной математике е-равенство. Оно говорит, что "к равно I с е-точностью".

Пусть <р,ф - формулы с тесными отрицаниями. Естественно определяется перевод " в посылке" цр (заменой всех подформул

вида к*1 на формулы к#Ь я (<_(к) # Г_< Ь))), и перевод "в

заключении" ф е (такой же заменой всех подформул вида а также заменой всех подформул вида к=1 на формулы к-И. Естественно, кД "внешним образом" пробегают кольцо К, а "внутренним образом" пробегают кольцо К'. Далее, Т* *

Т). Перевод <р (-► <р' продолжается на формулы вида уР и

Теорема 6 аналогична теореме 5. В частности, имеет место

Теорема 6а. Пусть Т - теория с тесными отрицаниями в языке колец," а ф АЕ-формула с тесными отрицаниями в том же языке. В выводимо: если К - кольцо с регулятором Г, то ([1Т(Е).^<1с) 1к>1щ) =1' ([[Т#<Е)*Уе>0 0#с(1с,]к»Ш^ГК)

=1), и ([[Т(1с)^(К)]к.]12(-к) =1) * Пт"' (¡с)=»Ус>0

\/1сеК.

Отсюда в теореме 66-в обычным образом получаем: если формула Т =» ф выводима в то формула Т*' =» Уе>0 выводима в 2?1'.

В этой теореме, в частности, в качестве К можно взять само кольцо (Кд) и тождественный регулятор Г.

Затем определяется широкий класс формул <(•,•) в языке колец (они называются дедекиндовыми). Для дедекиндовой формулы к(-,0 и тех же Т ,ф, что и в теореме 6а, доказывается

Теорема 7. Если (к(К,П =» ГТСх) =» 0(хПк), то

гП' 1- У£2 (ЕУК.Г (к(К,П (Т8(х) * Уе>0 08с(х)]к3п =1). Здесь переменная С2 пробегает класс всех полных гейтннговых алгебр, а Т^ ч {р* |¥>€Т) и определяется аналогично

тому, как выше.

Перейдем к §3, где изучается указанное выше внутреннее кольцо Уд из У^ (везде £2 - любая полная гейтингова алгебра). Далее "внутренние" переменные пробегают множество всех

фильтров Коши в Уу (точнее, множество их баз в базе топологии а "внешне" р,ч пробегают множество (У^) .

Определим предикаты аналогичные предикатам и кМ. А

именно, (р-д) =; Заерлч (а порядка сг*), где <ге£у - базе окружений равномерного пространства У, и (р^) ь Эо-бЕу ЗаерЗЭея (оЧа)с1сг((?)), где (1 - предикат дизъюнктности двух множеств. Запись ур означает, что формула <р в языке колец с тесными отрицаниями и в ней все подформулы вида х*у заменены на формулы х#у. Запись означает, что в формуле

дополнительно все подформулы вида х=у заменены на формулы х-у. Перевод у ь* <р' естественно продолжается на формулы вида <р8 и При некоторых ограничениях доказывается: если

2ГI- У2,У (к(У) п 2-плотное подкольцо кольца У~ => (Т(х) => 0(х)12), то г?У у УП.У (П,У) =» 1Т#,(х) =» У<геЕу

ф У)'" Теорема 8 содержит интуиционистский

вариант этого утверждения, а теорема 9 - его классический вариант.

В ГЛ9В£_Ш изучается нижеуказанная проблема, [15,18]. Напомним, что класс X* колец называется модельным компаньоном класса X колец, если X аксиоматизируем и его теория модельно полна, а, кроме того, любое кольцо из X является подкольцом некоторого кольца из X и, наоборот, любое кольцо из X - кольца из X Пусть Ф - теория, имеющая модельный компаньон Ф . Здесь и далее все теории пишутся в языке колец и содержат аксиомы колец. По теории Ф образуем класс колец Хл « <К |<КП)*=Ф>, а также образуем класс колец

» г *

Хф <К ЦФ^г^^ п <Кр)*=Ф >. Первый из них определен точно также, как и в первой части реферата. А в определении второго класса используется, кроме условия нормальности Ф^ еще условие безатомности Ф2 * УеЭед (ер^е п (ед=Оие0=е «» е=0)). Если теория Ф* включает, например, аксиому "первичное кольцо" (в частности, аксиому "тело" или "поле"), то условие Ф| в определении класса Хф можно опустить, так как оно вытекает из этого условия на Ф . Спрашивается: имеет ли класс Хф модельный компаньон и каков он? Ответ: при некоторых ограничениях класс Хф хорново аксиоматизируем (эту аксиоматику обозначим Т ) и является модельным компаньоном класса Хф. Причем имеется алгоритм, который (в реальное время) по аксиомам теории Ф выписывает аксиомы теории Т .

В §1 приводятся нужные нам в дальнейшем конструкции и утверждения. Обозначим В (К > полную булеву алгебру -подалгебру в У(К), состоящую из всех стабильных в ?(К) элементов. Иными словами, теперь У1М можно понимать, как решетку всех открытых множеств стоунового пространства Х(К) булевой алгебры В (К). И поэтому В (К) - решетка всех регулярных открытых множеств компакта Х(К) (т.е. дедекиндово . пополнение алгебры В(Ш). Элементы алгебры В(К)

отождествляются с открыто-замкнутыми множествами в ?(К).

В (К)

Для нормального кольца К выполняется К'еУ , и поэтому определена оценка Е^'^к'Зщк) (связанная с булевозначным универсумом V®"*') для любой формулы <р в языке колец с параметрами ЕбК (вместо к фактически подставляется Р^). С другой стороны, определим оценку С'Зщ для всех формул <р в языке колец с параметрами из К как [1с=Ь* |[к=13д-, УкДеК и

далее обычым образом с использованием операций именно в алгебре В (К).

Предложение 4. Пусть К - нормальное кольцо. Тогда:

= ^ ЬРК-ЗВ(К) = МВ •

где неравенство выполняется для любой формулы <р в слабо Е-нормальной форме (см. ниже), а равенства выполняются для любой формулы (р. Здесь <р с любыми параметрами из К.

Формула называется "в слабо Е-нормальной форме", если посылка любой ее импликации: во-первых, не содержит квантора 3 и, во-вторых, не содержит квантора V в области действия связки и.

Заметим, что [к^Зу = <реХ(К) |кр=1р), УкДеК, и то же самое выполняется для любой позитивной бескванторной формулы ф(Е) вместо атомарной формулы (к=и.

Предложение 6. Пусть К - нормальное кольцо и (К_)»=Ф ,

* г

где Ф - модельно полная теория. Тогда для любой формулы <р( 1с) в языке колец с параметрами Ее К выполняется: Е(р(Е)]1у = (реХ(К) |Кр»=р(1ср)> и значение Ечр(Ю]ст оценки является открыто-замкнутым множеством в Х(К).

Класс колец К назовем булево правильным, если УК.ЬеХ (Ш, ■» В(К)£Ва>). Это, конечно, так, если К£Ь =» г(К)£2<и, где 2(Ю - центр произвольного кольца Я. Если X - булево правильный класс и УКеХ (Ф})£> то X называется булево простым, если VK.UK <К£Ь •» УреХ(и ((р-ЫлК £ (рпК)-К). Последнее включение, конечно, влечет равенство (р-Ь)пК = (рпК)-К. Булево абсолютным называется булево правильный и булево простой класс. Например, любой булево правильный подкласс класса всех бирегулярных колец является булево абсолютным.

Перейдем к §2. Обозначим У класс всех первичных Р1-колец А (рассматриваемых как центральные алгебры над целостными кольцами 2(А)) фиксированной степени з.

Этот класс легко аксиоматизировать явно выписываемой теорией Ту Обозначим Уд класс всех центральных простых алгебр размерности п^, где п - любое натуральное число. Здесь б=2-п. Например, МдИЙ) и Н (кватернионы) - алгебры из Уд при п=2. Выполняется: Уп^У- И класс У0 также аксиоматизируется

явно выписываемой теорией Тц, . Нас интересуют подклассы в

г0

классе Уд , описываемые как Уу * ^КбУд |2(К)>=Тд)> где Тд -

какая-то фиксированная теория, имеющая модельный компаньон Тд. Например, Тд - теория "быть формально вещественным полем" или теория "быть полем". Легко показать, что класс Уу^ аксиоматизируется некоторой явно выписываемой (по Тд)

теорией Ф. А также то, что класс Ут* (аксиоматизируемый

. о

некоторой теорией Ф ) - модельный компаньон класса Уу (а

теория Ф* - модельный компаньон теории Ф). Это проверяется в предложениях 1,4.

Обозначим Х-г =5 (К |<К )£УТ } (иными словами, Хх ч (К

Т0 Р Т0 Т0

|<Кр)мФ}) и обозначим Ху* * (К |({Кр)£Уу*) л <С1)2)К) 1иными

словами, Ху* * <К | (< Кр) *=Ф*) п (Ф2>к)>.

Теорема 10.2. Класс колец Хт-* хорново аксиоматизируем и

'0

является модельным компаньоном класса Хт- . Аксиоматика

0

класса Ху» явно выписывается по аксиоматике теории Тд.

Например, следующие классы модельно полны: {К |Ур

(кр=ш п (ч^к*- <к 1ур (Кр5И и КР5М2(К)) п 1ф2)к}- ПУСТЬ т0 - теория полей. Тогда хорново аксиоматизируемый класс Ху» -

модельный компаньон класса Ху ¡5 (К |{Кр)£У). Приводится много других примеров разного сорта модельно полных теорий и модельных компаньонов классов и теорий.

Параграф 3. Теорию Т назовем нормально автономной, если всякая ее модель вкладывается в такое нормальное кольцо Г, что <Гр)»=Т. Обозначим Х^(К) множество всех собственных . идеалов в алгебре В(К). Если яеХ^(К), то обозначим К^ * К/ ф где с| Я'К - идеал в кольце К. Обозначим <¡5 |ЧеХ^(Ю). Теорию Т назовем тотально автономной, если для любой ее модели К выполняется <К^)>=Т. Например, если Ть Ф^, где Фд « "неразложимое", то, очевидно, Т - нормально и тотально автономная теория.

Теорема 11. а) Пусть Х1 * {1С |(<Кр)(=Ф) п (Ф^), где Ф АЕ-теория. Тогда класс колец X, хорново аксиоматизируем; а

именно: КеХ^ в ((Ф'

б) Если класс Хф булево абсолютен, то он - модельно полный класс.

г) Пусть Ф£Ф*. Если Ф - нормально автономная теория, а класс колец Хф - булево абсолютный, то класс Хф - хориов модельный компаньон класса Хф. В частности, теория Ф^Ф2+(Ф )' - модельный компаньон теории Ф'.

д) Пусть Ф - нормально автономная теория, Ф - тотально автономная теория, а Хф - булево абсолютный класс колец. Тогда Хф - хориов модельный компаньон класса Хф.

Теорема 12. Пусть теория Ф модельно вложима в теорию (и это выводимо в 2ГС). Пусть Ф АЕ-теорня и Ф[ - тотально автономная теория. Тогда любое нормальное кольцо К, для которого {Кр)*=Ф, вложимо в такое кольцо Ь, что {1-р)>=Ф^.

Параграф 4. Теперь мы хотим из того, что некоторый класс Хф^ - модельный компаньон некоторого класса Хф,

получить, что теория Ф| (локально соответствующая классу Хф ) - модельный компаньон теории Ф (локально

соответствующей классу Хф). Примером такого результата является теорема 13.

В определении 1 формулируется понятие "класс Х^ -слабый модельный компаньон класса К", которое существенно слабее следующего условия: "класс Х^ - модельный компаньон класса X и УКеХУ1сХ1 (К£Ь =» (Зр^ХаПреХШ (р2р1пК) п УкеК ((Зеер1 (е•к=к)) * Зеер (е-к=к))П.

Теорема 13. Пусть выполняются следующие условия на теории Ф,Фд и класс Хд колец:

(К |<Кр)*Ф0 п <ФО'+Ф1+Ф2)К} е 2 <К I < Кр) , а X « <К |(Кр>»=Ф) и класс Хд - слабый модельный компаньон класса X. Если ФьФд и Фд ьФ^, т0 теория Фд - модельный компаньон теории Ф.

Например, отсюда получаем: класс всех строго регулярных колец не имеет слабого (обычного) модельного компаньона Хд, если Фд н Фд (соответственно, если ФдЬ "простое").

Модельная полнота часто влечет полноту; примером такого сорта результата является теорема 14.

Назовем 1-примитивной такую примитивную формулу, в которой не более одного неравенства. Теория Т "разрешает класс £ замкнутых формул", если (Ti-#>) или (Тпф) для всех <р из £.

Теорема 14. а) Пусть теория Ф разрешает класс всех 1-примитивных замкнутых формул и для любого кольца К из класса X s {К |<Кр)м1>) множество В(К) бесконечно. Тогда теория ThX разрешает все Е-замкнутые формулы.

• б) Пусть теория Ф имеет модельный компаньон Ф . Если Хф - булево абсолютный класс и теория Ф разрешает класс всех 1-примитивных замкнутых формул, то класс Хф аксиоматизируем и его теория Ф^-И^+'Ф*)' - полная, модельно полная и хорнова.

Приведем пример возможного перехода от "локальной" теории Ф к "глобальной" теории Ф'+Ф| (обычно существенно более общей, чем теория Ф).

Теорема 15. Если в теории Ф выводима формула <р, то в теории Ф'выводима формула (в языке колец) (р-1)0 n (V>) + (см. ниже).

Последняя формула определяется следующим явным переводом: классически преобразуем формулу up к предваренной форме <р-\, запишем (в языке колец) формулу выражающую

1<р->1у =0. Аналогично: запишем <р в предваренной форме и добавим п перед каждым квантором 3 (эту формулу обозначим 9-1-1), запишем формулу (в языке колец) <р+, выражающую Ev>-i-i]y =1.

0£М2жение, §§1-3 содержит краткие в историческом плане мотивировки рассматриваемых понятий и проблем.

0£М22>ение, §4 содержит формулировки основных, по мнению автора, результатов этой работы.

В приложении, §5 обсуждается задача построения траектории по спецификации и описанию соответствующей сцены. А также обсуждается задача обобщенного описания. Приводятся интерпретации (в рамках понятий и результатов, изложенных в главах 1-П1)и некоторых других основных представлений о поведенческой системе.

Спецификация траектории y=f(x) задается формулой ф ч

УхЗуР(х.у) языка колец (или языка упорядоченных колец). Например, спецификация может говорить, что траектория должна пересекать несколько указанных областей и не пересекать несколько других указанных областей некоторого пространства КП; каждая область описывается в этом пространстве системой уравнений и неравенств (с параметрами), включающей, может быть, логические связки и кванторы. Кроме того, спецификация может выражать дополнительные требования к траектории типа перпендикулярности, параллельности, прямолинейности,

монотонности ее участков; то, . что траектория выходит из определенной области и оканчивается в определенной области. Можно также выразить условие, что траектория - полином фиксированной степени. Например, спецификация может требовать: найти полином фиксированной степени, который пересекает данное алгебраическое многообразие более т раз. Все эти требования спецификация выражает относительно каких-то операций +,-, • в пространстве К.П. Существует представление о том, что эти операции не фиксированы раз и навсегда и что в качестве таких (базовых) операций для разных классов задач следует выбирать разные операции. Эти операции описываются или аксиоматически (набором Т их свойств, который может возникать в результате "наблюдений") или явными термами в языке более высокого уровня, чем язык колец. Таким образом, в первом случае спецификация принимает вид ИТ). _ , =» (0). _ .), а во втором случае она принимает

, i , »

вид {ф)^ 3, где термы Ь.г.э в языке теории множеств описывают соответственно три операции. Спецификация (задание на движение) должна сопровождаться обоснованием того, что существует хотя бы одна траектория, ей удовлетворяющая. Иными словами, сопровождаться выводом в языке высокого уровня формулы [(Т). _ . =» (0) _ .1 или формулы (0К „. Сам по себе такой вывод может быть предметом поиска в полностью автоматическом илн в интерактивном режиме. Результаты главы II позволяют в реальное время перейти от такого вывода к соответствующему интуиционистскому выводу, который (при определенных ограничениях) в свою очередь может быть преобразован, в программу вычислимой функции у=Нх) (или

коэффициенты полинома f(x)).

Набор Т свойств задается непосредственно или с помощью

нижеуказанного "механизма обобщения входной информации Ф*".

ф

Во втором случае вместо Т употребляют обозначение Т и Т в ТЬХф, где Хф - "актуальная модель обстановки", см. ниже.

Поведенческая система функционирует дискретными тактами времени 1,...,п,... Актуальная модель обстановки ХЛ

описывает обстановку (во внешнем мире) на основе текущей входной информации Фд и с учетом прошлого опыта (поведенческой системы). Возможно следующее представление: поведенческая система имеет широкий набор "элементарных модулей" К, каждому из которых текущим образом приписывается вес е^еВ(К). Эти веса меняются по определенному правилу, которое отражает изменяющийся опыт. На n-ом такте образуется "модуль" Хф * {К |Vpee^ (Фп>^ >• Переход к

локализации Кр соответствует переходу к уровню более близкому к входу-выходу поведенческой системы. Например, все Кр могут быть 4-мерными векторными пространствами, и тогда Фп может содержать все обычные элементы "физического"

описания обстановки. Модуль Хф часто весьма сложный и его

п * ♦

удобно "апроксимировать модулем" Хф ; при этом теория Т «г * п

ТЬХф играет роль "обобщенного описания внешней обстановки" п

в момент п. На этой основе в §5 приложения уточняются представления об изменении весов, о целенаправленных действиях и т.д. Эта модель компьютерно реализуема.

ЛИТЕРАТУРА

И] Friedman Н. The consistency of classical set theory relative to a set theory with intuitionistic logic, The Journal of Symbolic Logic, v. 38, no 2, 1973, p. 315-319.

[21 Йех Т. Теория множеств и метод форсинга. -М.:Мир,1973.

131 Grayson R. Heyting-valued models for intuitionistic set theory.- Lecture Notes in Mathem; v. 753. Berlin; Heidelberg; New York: Springer, 1979.-p.402-414.

[4 J Любецкнй В. А. Из существования неизмеримого множества типа ^ вытекает существование несчетного множества типа СА.- Доклады Академии Наук, 195, №3, 1970, с. 548-550.

[5J Кановей В.Г. Неразрешимые и разрешимые свойства конституант. Математический сборник, том 124 (166), №4(8), 1984, с. 505-535.

(61 Новиков П.С. О некоторых теоремах существования (1939).- В кн: Новиков П. С. Избранные труды. - М.: Наука, 1979, с. 127.

(71 Myh ill J. Some properties of intuitionistic Zermelo-Frankel set theory, Lecture Notes in Mathematics, v. 337, 1971, p. 206-231.

(81 S^edrov A. Intuitionistic set theory. In: "Harvery Friedman's Res. Found. Math.", Amsterdam, 1985, 257-284,

(91 Friedman H. Classically and intuitionistically provable recursive functions. In: Higher Set Theory, Lecture Notes in Mathematics, 669, Springer-Verlag, 1978, p. 21-27.

(101 Бернштейн И.А. О построении движений. М.: Медгиз, 1947, 255 с.

(И) Беркннблит М.Б., Чернавский А.В. Построение движения и метафора интеллекта. В сб.: Компьютеры н познание. М.: Наука, 1990, с. 22-41.

(121 Абдусаматов P.M., Беркннблит М.Б., Фельдман А.Г., Чернавский А.В. Моторика и интеллект. В сб.: Интеллектуальные процессы и их моделирование, под редакцией Велихова Е.П. и Чернавского А.В..- М.: Наука, 1987.

(13) Беркннблит М. Б., Гельфанд И.М., Фельдман А. Г. Двигательные задачи и работа параллельных программ. В сб.: Интеллектуальные процессы н их моделирование Организация движения. М.: Наука, 1991, с. 37-54.

(141 IEEE Transactions on systems, man, and cybernetics. Special issue on unmanned vehicle and intelligent robotic systems. Volume 20, №6, 1990.

(15) Макинтайр А. Модельная полнота//Справочная книга по математической логике, том 1., М.: Наука, 1982.-Гл.4.-С. 141—182. (Английское издание этой работы: Macintyre А.

Model completeness. - In book: Handbook of mathematical logic.- North-Holland publishing company, Amsterdam-New York-Oxford, 1977, chapter 4, p. 139-180.

1161 Carson A.B. The model completion of the theory of commutative regular rings.- J. Algebra, 27, 1973, p. 136-146.

1171 Lipschitz L. Saracino D. The model companion of the theory of commutative rings without nilpotent elements.-Proc. Amer. Math. Sos., 37, 1973, p. 381-387.

1181 Macintyre A. Model completeness for sheaves of structures.- Fund. Math., v. 81, 1973, p. 73-89.

(191 Weisspfenning V. Model completeness and elimination of quantifiers for subdirect products. J.. Algebra, 28, 1973, p. 146-157.

[201 Neumann J. von. Continnous geometry.- fl. Y.: Princeton, 1960.

1211 Goodearl K.R. Von Neumann regular rings.- London e.a.: Pitman, 1979.

[221 Carson A.B. Model completions, ring representations and the topology of the Pierce sheaf. Harlow: Longman, 1989, 107 p.

(231 Eklof P.C., Mez H.C., The ideal structure of existentially closed algebras., J. Symbol. Log., 50, №4, 1985, p. 1025-1043,.

1241 Eklof P.C., Mez H.C., Modules of existentially closed algebras. J. Syibol. .Log., 52, №1, 1987, p. 54-63.

1251 Давыдов В. В. Виды обобщения в обучении. М.: Педагогика, 1972, 423 с.

1261 Веденов А.А. Моделирование элементов мышления. М.: Наука, 1988, 159 с.

[271 Вайнцвайг М.Н. Алгоритм обучения распозиованию образов "Кора". В сб.: Алгоритмы обучения и распозновання образов, М.: Сов. Радио, 1973.

[281 Handbook of Theoretical Computer Science, volume

A: Algorithms and Complexity, volume B: Formal models and Semantics; The Mit Press Cambridge, Massachusetts, 1990.

(291 Вапник В.И., Червоненкнс А.Я- Теория распознования образов Статистические проблемы обучения. М.: Наука, 1974, 415 с.

1301 Палютин Е.А. Спектр и структура моделей. В кн.: Справочная книга по математической логике, том 1. М.: Наука, 1982, Дополнение, с. 320-387.

(311 Macintyre A., Krelsel G. Constructive logic versus algebralzatlon, I. The L. E. J. Brouver-Centenary Symposium (Noordwljkerhout-1981). Stud., Logic, Foundations Math. 110, North-Holland, Amsterdam - N-Y, 1982, p. 217-260.

(321 Friedman H., Seress A. Applications of mathematics to theoretical computer science. Emerg. Synth. Sci.: Proc. Found. Workshops, Santa Fe Inst., Santa Fe, N.M., 10-11, Vol. 1, 1988, p. 10-117

[331 Friedman H. Necessary uses of abstract set theory in finite mathematics. Adv. Math., 1986, 60. №1, p. 92-12.

[341 Simmons H. The semiring of topologlzing filters of a rings. Israel J. Math., 61, №3, 1988, p. 271-284.

[351 Лорьер Ж.-Л. Системы искусственного интеллекта. М.: Мир, 1991, 568 с.

1361 Логический подход к искусственному интеллекту От классической логики к логическому программированию. М.: Мир, 1990, 439 с.

(371 Ковальскн Р. Логика в решении проблем. М.: Наука, 1990, 278 с.

[381 Вагин В.П. Дедукция и обобщение в системе принятия решений. М.: Наука, 1988, 385 с.

1391 Нечеткие множества и теория возможностей. М.: Радио и связь, 1986, 406 с.

(401 Fournan М.Р., Scott D.S. Sheaves and logic.-Lecture Notes in Mathem. v. 753. Berlin; Heidelberg; New York: Springer, 1979, p.302-401. .

Работы автора по теме диссертации.

[411 Любецкий В. А. О несуществовании эффективного неизмеримого множества,- В сб.: Математические методы решения инженерных задач, вып. 4. М.: МО, 1977, с. 36-40.

[42] Любецкий В.А. Булевозначные расширения структур. В сб: Математические методы решения инженерных задач, вып. 6. М.: МО," 1979, с.67-81.

143] Любецкий В.А. Вложение пучков в гейтинговозначный универсум и теоремы переноса,- В кн: 6-ая Всесоюзная конференция по математической логике, Тбилиси, 1982, с. 98.

144] Любецкий В. А. Алгебраические аспекты нестандартного анализа. -М., 1983,- Деп. ВИНИТИ, номер 9341-83 деп.

[45] Любецкий В. А. Пучки на гейтинговон алгебре: случай колец. -М., 1984,- Деп. ВИНИТИ, номер 3971-84 деп.

[46] Любецкий В.А. Булевозначный анализ алгеброических систем.- В кн.: 9 Всесоюзный симпозиум по теории групп. М.: 1984, с. 218.

[47] Любецкий В.А. Теоремы переноса и нестандартный анализ.- В кн.: Седьмая всесоюзная конференция по математической логике. Новосибирск, 1984.

[48] Любецкий В.А. О некоторых алгебраических вопросах нестандартного анализа.- Доклады АН СССР, т. 280, №1, 1985, с. 38-41.

[49] Любецкий В.А. Некоторые применения теории, топосов к изучению алгебраических системю.- Дополнение к кн: Джонсон П.Т. Теория топосов.-М.: Наука, 1986, с.376-433.

[50] Любецкий В.А. Интерпретация морфизмов алгебр Гейтинга в гейтинговозначном универсуме: Докл. на 8-ом конгрессе по логике, август 1987//Реф. журн. ВИНИТИ.-

том 13, вып. 3, 1988, с.17.

151] Любецкий В.А. Оценки и пучки. - Препринт ИППИ АН СССР, М., 1988, 64 страницы.

[521 Любецкий В.А. О некоторых применениях гейтинговозначного анализа, I. - Сборник работ конференции по компьютерной логике, Таллинн, Институт кибернетики АН ЭССР, 1988, с. 58-75.

[531 Lyubetsky V.A. 0n some applications of Heyting-valued analysis, II.- Lecture Notes in Computer Science, Springer-Verlag, v. 417, 1988, p. 122-145.

[54] Любецкий В.А. Оценки и пучки. О некоторых вопросах

нестандартного анализа,- Успехи математических наук, т. 44, вып. 4(268), 1989, с. 99- 153. (Английский перевод в London Mathematical Society, Russian Mathematical Surveys, 1989, p. 37-112.

[551 Любецкий B.A. О вложнмостн классов моделей.-Всероссийская школа по основаниям математики и теории функций, Саратов, 1989, с. 52.

[561 Любецкий В.А. Локально аксиоматизируемые классы колец,- В кн.: Международная конференция по алгебре памяти А.И.Мальцева. Новосибирск, 1989, с. 72.

[571 Любецкий В.А. Интерпретации математических структур в гейтннговозначном универсуме.- В кн.: Синтаксические и семантические исследования

пеэкстенсиональных логик, М.: Наука, 1989, с. 101-111.

[581 Lyubetsky V.A. Locally aximatizable classes of rings. Logic Colloquium'89, Berlin, ASL, 1989, p. 101.

[591 Любецкий B.A. Внутренне и локально аксиоматизируемые классы, пучковые пополнения.- В кн.: 10-я Всесоюзная конференция по логике и методологии науки, Минск, 1990, с.17-18.

[601 Любецкий В.А. Об одной гипотезе П.С.Новикова.- В кн.: Советско-Французский коллоквиум по теории моделей, Караганда, 1990, с. 23.

(611 Любецкий В.А. А^одельиая полнота теории и оценка формул.- Алгебра и логика, Новосибирск, т. 29, 1990, с. 15-28.

[621 Lyubetsky V.A. Heyting-valued analysis: P.S.Novikov's hypotheses.- Logic Colloquin'90, Helsinki, ASL, 1990, The Journal of Symbolic Logic, v. 31, p. 277.

[631 Любецкий B.A. Гейтннговозначный анализ: гипотеза П. Новикова. В сб.: Философские основания неклассических логик (Труды научно-исследовательского семинара по логике ИФ АН СССР). М.: АН СССР, 1990, с. 105-119.

[641 Любецкий В.А. Интуиционистская теория алгебраических систем и нестандартный анализ.-Алгебра и Логика, Новосибирск, №3, 1991, с 320-332.

[65] Любецкий Й.А. Теоремы переноса. Международная

конференция по алгебре, посвященная памяти А.И.Ширшова (Логика, универсальная алгебра. Прикладная алгебра.) Новосибирск, 1991, с. 77.

Отметим также две работы по смежной теме, не вышедшие из печати на данный момент:

166) Lyubetsky V.A. Heyting-valüed analysis: P.S.Novikov's hypotheses.- Hal'cev Conference Proceedings, volume 3, part VI.a (Logic), In Transe. Amer. Math. Sos., Adv. Math., 1991, 20 pp.

(671 Любецкий В. А. Переход от выводимости в ' классической теории множеств к выводимости в интуиционистской теории множеств для языка колец.- Алгебра н логика, Новосибирск, №6, 1991, dS се.

Подп. к печати ¿6-i(jj 199Í- г. Ф.П.Л. 1,0 Тираж 110

Типография ОХО Миннефтегазпрома СССР. Зак. № П69