Содержание к диссертации
Введение
1. Обзор используемых определений и результатов 15
1.1. Общие определения 15
1.2. Операции над отношениями 16
1.3. Модальные логики 18
1.4. Шкалы Крипке 19
1.5. Произведения модальных логик 22
1.6. Временные логики 23
1.7. Некоторые свойства полиномиальных колец над полем Q . 24
2. Свойства расширений логики SLn 28
2.1. Действия моноидов и левые конгруэнции 28
2.2. Связь SLn-KOHycoB и конгруэнции на Afn 32
2.3. Конгруэнции на ЛЛ1 и идеалы кольца полиномов над Q 36
2.4. Конгруэнтные замыкания множеств пар векторов 39
2.5. Нормальные формы в SLn 44
2.6. Описание конечно аксиоматизируемых расширений SLn 45
2.7. Приведённый вид аксиом расширений SLn 48
2.8. Конечная аксиоматизируемость расширений SLn 53
2.9. Разрешимость расширений SLn 57
2.10. Разрешимость табличности конечно аксиоматизируемых расширений SL 60
2.11. Операции над конгруэнциями 62
2.12. Структура классов сглаживания 69
2.13. Поведение конгруэнции при склейке 71
2.14. Финитная аппроксимируемость расширений SLn 74
3. Свойства произведений модальных логик 76
3.1. О сохранении финитной аппроксимируемости для произведений 76
3.2. О сохранении разрешимости для произведений 79
3.3. О простой перемножаемости 82
4. Свойства расширений логики SL.tn 85
4.1. Связь SL.tn-KOHycoB и конгруэнции на Zn 85
4.2. Связь SL.t"-KonycoB и подгрупп Zn 89
4.3. Порождающие множества подгрупп Zn 92
4.4. Нормальные формы в SL.t" 94
4.5. Финитная аппроксимируемость расширений SL.tn 95
4.6. Приведённый вид аксиом расширений SL.t" 97
А. Свойства логик SL и SL.t 103
А.1. Свойства конусов логик SL и SL.t 103
А.2. Описание расширений логик SL и SL.t 106
Предметный указатель 109
Литература 112
- Некоторые свойства полиномиальных колец над полем Q
- Разрешимость табличности конечно аксиоматизируемых расширений SL
- О сохранении финитной аппроксимируемости для произведений
- Порождающие множества подгрупп Zn
Введение к работе
Первые модальные исчисления были созданы Льюисом [19], [20]. В дальнейшем теория модальностей превратилась в раздел математической логики благодаря работам Гёделя [12], Маккинси-Тарского [22], Крипке [16], [17], [18] и других. Появление многочисленных приложений модальных логик в информатике [23], теории искусственного интеллекта [5], математической лингвистике [2] и в основаниях математики [3] привело к стремительному росту этой области начиная с 1980-х годов.
Основные отличия модальных логик от классических - это наличие дополнительных (модальных) связок (необходимо) и О (возможно), а также большое разнообразие семантик. Одной из самых распространённых семантик для модальных логик является семантика возможных миров, в которой значение истинности каждой формулы зависит от «возможного мира». В частности, возможные миры в реляционной семантике Крипке рассматриваются как всевозможные варианты развития событий; при этом для каждого мира задаётся множество альтернативных ему миров и модальность интерпретируется как «истинно во всех мирах, альтернативных данному».
Современные модальные логики, как правило, являются многомодальными, т.е., содержат несколько базисных модальных связок, что позволяет выразить взаимодействие нескольких модальностей в рамках одного языка.
При содержательном рассмотрении многомодальных логик возникает задача - как можно получить многомодальную логику, описывающую взаимодействие заданных модальностей (характеризующих, например, время, пространство, знание и т. д.), при наличии модальной формализации для каждой из этих модальностей ? Для решения это задачи применяются различные способы комбинирования модальных логик, т.е., построения с помощью определённых правил новой модальной логики по нескольким заданным модальным логикам. При этом особое внимание уделяется связи свойств комбинированной модальной логики с соответствующими свойствами исходных модальных логик.
Введение
Простейший способ комбинирования модальный логик - это их соединение, которое строится как наименьшая модальная логика в объединении языков исходных модальных логик (при этом считаем, что модальности в комбинируемых логиках обозначаются по-разному), содержащая данные исходные логики. Как показано в [6], при соединении сохраняются многие свойства исходных логик, включая полноту по Крипке, финитную аппроксимируемость и разрешимость. Однако, как показала Спаан [31], алгоритмическая сложность при соединении может вырасти.
Другой распространённый вид комбинирования - это произведения, которые могут использоваться для описания <прямых произведений» различных модальных структур, например, пространства и времени, действий и времени, действий и необходимости и т.д. Произведение модальных логик определяется как логика класса всевозможных прямых произведений шкал Крипке перемножаемых логик (под прямым произведением шкал понимается шкала, носителем которой является прямое произведение носителей перемножаемых шкал, а в качестве отношений берутся отношения исходных шкал, продолженные на новые измерения как отношения равенства). Данный метод построения модальных логик был впервые рассмотрен Шехтманом [40] и в дальнейшем подробно изучен в ряде работ [7], [8], [9], [10], [30]. Произведения модальных логик применяются в информатике и в теории искусственного интеллекта ([25], [26], [27], [7], также с произведениями тесно связаны результаты о многомерных дескриптивных модальных логиках [32]).
В дополнение к обычному произведению модальных логик (называемому также семантическим) определяется синтаксическое произведение, строящееся при помощи добавления к соединению перемножаемых логик аксиом специального вида. Как показано в [8], синтаксическое и семантическое произведения двух «хорновских» модальных логик совпадают, откуда следует, что для достаточно широкого класса модальных логик их произведение можно задать аксиоматически добавлением к исходным логикам дополнительных аксиом (модальные логики, семантическое и синтаксическое произведения которых совпадают, называются «просто перемножаемыми»).
Однако, эти произведения совпадают не всегда, например, как показано в [8], семантическое и синтаксическое произведения логик Grz С L\ С Triv и S4 С L2 Q Triv не совпадают. В связи с этим для модальных логик актуален вопрос - совпадают ли их синтаксическое и семантическое произведения, т. е., можно ли аксиоматизировать их семантическое произведение с помощью аксиом их синтаксического произведения.
Перенос различных свойств модальных логик (табличности, финитной ап-
Введение проксимируемости, конечной аксиоматизируемости, разрешимости и некоторых других) от сомножителей к произведениям исследовался в ряде работ (см. [7]), например, в [8]. В частности, было показано, что конечная аксиоматизируемость, финитная аппроксимируемость и разрешимость в общем случае не переносятся, табличность переносится, для рекурсивной аксиоматизируемости показано, что она переносится для некоторых классов перемножаемых логик.
В [11] показано, что произведение двух логик из достаточно широкого класса, включающего, в частности, К4, S4, Grz, GL, неразрешимо и не является финитно аппроксимируемым. Как следует из [13], при п ^ 3 все модальные логики, находящиеся между Kx...xKhS5x...x S5, являются неразрешимыми и не могут быть конечно аксиоматизированы. Эти результаты показывают, что произведение даже простых логик может иметь очень сложную структуру, причём для высоких размерностей ситуация ухудшается.
Для разрешимых произведений модальных логик возникает вопрос об их сложности. Во многих случаях сложность при умножении логик возрастает [7], например, произведения К4 х К и К4 х S5 coNEXPTIME-трудны, S5 х S5 и S5 х К - coNEXPTIME-полны, К4.3 х S5 - EXPSPACE-трудно. Однако в работе Маркса [21] показано, что сложность произведения логики класса одномодальных шкал Крипке F с функциональной модальностью (в действительности, такими логиками являются в точности непротиворечивые расширения логики SL, речь о которой пойдёт ниже) на логику класса одно-модальных шкал Крипке /С совпадает со сложностью логики данного класса /С.
Модальные логики «завтра» (SL) и «вчера-завтра» (SL.t) (называемые также логиками с функциональными модальностями благодаря специфической структуре их шкал Крипке) были введены в 1965 году Леммоном и Скоттом (также см. [24]). Доказательства же первых результатов об этих логиках были опубликованы Сегербергом [29], а Мучник [34], [35] доказал предтабличность логик SL и SL.t (т.е., что все непротиворечивые собственные расширения этих логик есть логики конечных шкал Крипке) и получил полное описание их расширений. Но систематическое исследование логик с функциональными модальностями было начато только в работе Сегербер-га [28] и продолжено Белиссимой [1] и Крахтом [15].
Многомодальные логики с функциональными модальностями являются естественным обобщением логики «завтра» (а логика «вчера-
Введение завтра» является их частным случаем). Семейство этих логик очень велико - можно легко построить неразрешимые модальные логики такого вида и, более того, нет возможности построить их разумную классификацию [15, параграф 9.4]. Некоторые логики из этого семейства - многомерные варианты SLn логики SL - были рассмотрены Габбаем и Шехтманом [8]. В частности, в этой работе было показано, что любые семейства соединений произвольного количества логик SL финитно аппроксимируемы (и, как следствие, разрешимы) и являются просто перемножаемыми, откуда следут, что логики SLn есть логики семейства всех шкал с п коммутирующими функциональными модальностями.
Многомодальный вариант логики SL представляет интерес как фрагмент пропозициональной динамической логики детерминированных вычислений DPDL [15]. Также многомодальные логики с функциональными модальностями применяются в математической лингвистике [2], [14].
При рассмотрении многомерного варианта SLn логики SL возникли естественные вопросы:
Как для случая логики SL" выглядят аналоги результатов, полученных Мучником [34], [35] для SL ?
Обобщаются ли результаты Маркса [21] о сложности проблемы выполнимости для произведения класса одномодальных функциональных шкал Крипке Т на класс одномодальных шкал Крипке К на классы Т многомодальных функциональных шкал Крипке и многомодальные классы /С ?
Что можно сказать о переносе свойств для произведений модальных логик на логики с коммутирующими функциональными модальностями ?
Переносится ли результат Габбая и Шехтмана [8] о простой перемно-жаемости семейств соединений произвольного количества логик SL на произведения многомерных логик с функциональными модальностями на произвольные многомодальные логики ?
Насколько сходны между собой многомерные варианты SLn и SL.tn логик «завтра» SL и «вчера-завтра» SL.t ?
Цель работы
Целью данной работы является исследование расширений многомерной временной логики с коммутирующими модальностями; в частности, доказа-
Введение тельство разрешимости некоторых свойств указанных расширений, изучение свойств произведений этих расширений на другие модальные логики, а также специальное исследование многомерных расширений с модальностями «вчера-завтра».
Научная новизна
Все основные результаты диссертации являются новыми и состоят в следующем:
Доказана конечная аксиоматизируемость всех расширений SLn и предложена их стандартная аксиоматизация.
Доказана разрешимость всех расширений SLn, приведён алгоритм решения проблемы выводимости для SLn и доказана разрешимость табличное расширений SLn.
Установлено, что все расширения SLn являются финитно аппроксимируемыми.
Доказано, что при семантическом умножении полных модальных логик на расширения SLn финитная аппроксимируемость и разрешимость сохраняются; дана оценка сложности разрешающего алгоритма для семантических произведений.
Найдено достаточное условие простой перемножаемости полных модальных логик и расширений SLn и критерий простой перемножаемо-сти логик Кот и расширений SLn.
Для расширений SL.t" дано более простое (по сравнению со случаем расширений SLn) доказательство их финитной аппроксимируемости и предложена их стандартная аксиоматизация.
Апробация работы
Результаты диссертации докладывались и обсуждались в 2000-2005 г. на научно-исследовательском семинаре по математической логике под руководством академика РАН СИ. Адяна и профессора В.А. Успенского и других спецсеминарах кафедры математической логики и теории алгоритмов механико-математического факультета МГУ, на международной конференции «Computer science applications of modal logic» (Москва, 2005), на XXIV
Введение
Конференции молодых учёных (Москва, 2002), на международном семинаре «2nd Moscow-Vienna Workshop on Logic and Computation» (Москва, 2002) и были представлены на международной конференции - отношение па W.
1) Пусть х Є W. Положим R(x)^{yeW\(x,y)eR}.
2) Пусть W' CW. Отношение R\w, определяется следующим образом: R\wl^Rn(W'xW').
Отношение R называется функцией1, если \R(x)\ = 1 для всехх Є W.
Обратное к R отношение Я-1; R-1^{(x,y)\(y,x)eR}.
Определение 1.6. Пусть R\, R2 - отношения на мнооїсестве W. 1) Композиция R\ о R2 отношений R\ и R2: RlQR2^ {(х, y)\BzeW (Or, z)GRx k (z, у) Є R2)} . 'Мы отличаем функцию от отображения, под которым понимается функция вместе с областью определения и областью значений.
Некоторые свойства полиномиальных колец над полем Q
Простейший способ комбинирования модальный логик - это их соединение, которое строится как наименьшая модальная логика в объединении языков исходных модальных логик (при этом считаем, что модальности в комбинируемых логиках обозначаются по-разному), содержащая данные исходные логики. Как показано в [6], при соединении сохраняются многие свойства исходных логик, включая полноту по Крипке, финитную аппроксимируемость и разрешимость. Однако, как показала Спаан [31], алгоритмическая сложность при соединении может вырасти.
Другой распространённый вид комбинирования - это произведения, которые могут использоваться для описания прямых произведений» различных модальных структур, например, пространства и времени, действий и времени, действий и необходимости и т.д. Произведение модальных логик определяется как логика класса всевозможных прямых произведений шкал Крипке перемножаемых логик (под прямым произведением шкал понимается шкала, носителем которой является прямое произведение носителей перемножаемых шкал, а в качестве отношений берутся отношения исходных шкал, продолженные на новые измерения как отношения равенства). Данный метод построения модальных логик был впервые рассмотрен Шехтманом [40] и в дальнейшем подробно изучен в ряде работ [7], [8], [9], [10], [30]. Произведения модальных логик применяются в информатике и в теории искусственного интеллекта ([25], [26], [27], [7], также с произведениями тесно связаны результаты о многомерных дескриптивных модальных логиках [32]).
В дополнение к обычному произведению модальных логик (называемому также семантическим) определяется синтаксическое произведение, строящееся при помощи добавления к соединению перемножаемых логик аксиом специального вида. Как показано в [8], синтаксическое и семантическое произведения двух «хорновских» модальных логик совпадают, откуда следует, что для достаточно широкого класса модальных логик их произведение можно задать аксиоматически добавлением к исходным логикам дополнительных аксиом (модальные логики, семантическое и синтаксическое произведения которых совпадают, называются «просто перемножаемыми»).
Однако, эти произведения совпадают не всегда, например, как показано в [8], семантическое и синтаксическое произведения логик Grz С L\ С Triv и S4 С L2 Q Triv не совпадают. В связи с этим для модальных логик актуален вопрос - совпадают ли их синтаксическое и семантическое произведения, т. е., можно ли аксиоматизировать их семантическое произведение с помощью аксиом их синтаксического произведения.
Перенос различных свойств модальных логик (табличности, финитной ап проксимируемости, конечной аксиоматизируемости, разрешимости и некоторых других) от сомножителей к произведениям исследовался в ряде работ (см. [7]), например, в [8]. В частности, было показано, что конечная аксиоматизируемость, финитная аппроксимируемость и разрешимость в общем случае не переносятся, табличность переносится, для рекурсивной аксиоматизируемости показано, что она переносится для некоторых классов перемножаемых логик.
В [11] показано, что произведение двух логик из достаточно широкого класса, включающего, в частности, К4, S4, Grz, GL, неразрешимо и не является финитно аппроксимируемым. Как следует из [13], при п 3 все модальные логики, находящиеся между KX...XKHS5X...X S5, являются неразрешимыми и не могут быть конечно аксиоматизированы. Эти результаты показывают, что произведение даже простых логик может иметь очень сложную структуру, причём для высоких размерностей ситуация ухудшается.
Для разрешимых произведений модальных логик возникает вопрос об их сложности. Во многих случаях сложность при умножении логик возрастает [7], например, произведения К4 х К и К4 х S5 coNEXPTIME-трудны, S5 х S5 и S5 х К - coNEXPTIME-полны, К4.3 х S5 - EXPSPACE-трудно. Однако в работе Маркса [21] показано, что сложность произведения логики класса одномодальных шкал Крипке F с функциональной модальностью (в действительности, такими логиками являются в точности непротиворечивые расширения логики SL, речь о которой пойдёт ниже) на логику класса одно-модальных шкал Крипке /С совпадает со сложностью логики данного класса /С.
Модальные логики «завтра» (SL) и «вчера-завтра» (SL.t) (называемые также логиками с функциональными модальностями благодаря специфической структуре их шкал Крипке) были введены в 1965 году Леммоном и Скоттом (также см. [24]). Доказательства же первых результатов об этих логиках были опубликованы Сегербергом [29], а Мучник [34], [35] доказал предтабличность логик SL и SL.t (т.е., что все непротиворечивые собственные расширения этих логик есть логики конечных шкал Крипке) и получил полное описание их расширений. Но систематическое исследование логик с функциональными модальностями было начато только в работе Сегербер-га [28] и продолжено Белиссимой [1] и Крахтом [15].
Многомодальные логики с функциональными модальностями являются естественным обобщением логики «завтра» (а логика «вчера- завтра» является их частным случаем). Семейство этих логик очень велико - можно легко построить неразрешимые модальные логики такого вида и, более того, нет возможности построить их разумную классификацию [15, параграф 9.4]. Некоторые логики из этого семейства - многомерные варианты SLn логики SL - были рассмотрены Габбаем и Шехтманом [8]. В частности, в этой работе было показано, что любые семейства соединений произвольного количества логик SL финитно аппроксимируемы (и, как следствие, разрешимы) и являются просто перемножаемыми, откуда следут, что логики SLn есть логики семейства всех шкал с п коммутирующими функциональными модальностями.
Разрешимость табличности конечно аксиоматизируемых расширений SL
Многомодальный вариант логики SL представляет интерес как фрагмент пропозициональной динамической логики детерминированных вычислений DPDL [15]. Также многомодальные логики с функциональными модальностями применяются в математической лингвистике [2], [14].
При рассмотрении многомерного варианта SLn логики SL возникли естественные вопросы: 1) Как для случая логики SL" выглядят аналоги результатов, полученных Мучником [34], [35] для SL 2) Обобщаются ли результаты Маркса [21] о сложности проблемы выполнимости для произведения класса одномодальных функциональных шкал Крипке Т на класс одномодальных шкал Крипке К на классы Т многомодальных функциональных шкал Крипке и многомодальные классы /С 3) Что можно сказать о переносе свойств для произведений модальных логик на логики с коммутирующими функциональными модальностями 4) Переносится ли результат Габбая и Шехтмана [8] о простой перемно-жаемости семейств соединений произвольного количества логик SL на произведения многомерных логик с функциональными модальностями на произвольные многомодальные логики 5) Насколько сходны между собой многомерные варианты SLn и SL.tn логик «завтра» SL и «вчера-завтра» SL.t Цель работы Целью данной работы является исследование расширений многомерной временной логики с коммутирующими модальностями; в частности, доказа тельство разрешимости некоторых свойств указанных расширений, изучение свойств произведений этих расширений на другие модальные логики, а также специальное исследование многомерных расширений с модальностями «вчера-завтра». Научная новизна Все основные результаты диссертации являются новыми и состоят в следующем: 1) Доказана конечная аксиоматизируемость всех расширений SLn и предложена их стандартная аксиоматизация. 2) Доказана разрешимость всех расширений SLn, приведён алгоритм решения проблемы выводимости для SLn и доказана разрешимость табличное расширений SLn. 3) Установлено, что все расширения SLn являются финитно аппроксимируемыми. 4) Доказано, что при семантическом умножении полных модальных логик на расширения SLn финитная аппроксимируемость и разрешимость сохраняются; дана оценка сложности разрешающего алгоритма для семантических произведений. 5) Найдено достаточное условие простой перемножаемости полных модальных логик и расширений SLn и критерий простой перемножаемо-сти логик Кот и расширений SLn. 6) Для расширений SL.t" дано более простое (по сравнению со случаем расширений SLn) доказательство их финитной аппроксимируемости и предложена их стандартная аксиоматизация. Апробация работы Результаты диссертации докладывались и обсуждались в 2000-2005 г. на научно-исследовательском семинаре по математической логике под руководством академика РАН СИ. Адяна и профессора В.А. Успенского и других спецсеминарах кафедры математической логики и теории алгоритмов механико-математического факультета МГУ, на международной конференции «Computer science applications of modal logic» (Москва, 2005), на XXIV Конференции молодых учёных (Москва, 2002), на международном семинаре «2nd Moscow-Vienna Workshop on Logic and Computation» (Москва, 2002) и были представлены на международной конференции ASL Logic Colloquium» (Вена, 2001). По теме диссертации автором опубликованы работы [41]-[47]. Содержание работы Во введении приводится исторический обзор результатов, связанных с темой диссертации, формулируются основные цели работы и кратко описывается её содержание. Первая глава содержит вспомогательный материал. Здесь даются необходимые определения, связанные с модальными логиками, и формулируются некоторые известные результаты. Параграф 1.7 посвящен теории базисов Грёбнера для полиномиальных колец над Q. Во второй главе исследуются свойства расширений SLn. В параграфах 2.1 и 2.2 устанавливается каноническое соответствие между 8Ьп-конусами и конгруэнциями на Мп и доказываются его свойства. В параграфе 2.3 каждой конгруэции на Nn сопоставляется идеал кольца полиномов от п переменных с рациональными коэффициентами: Определение (2.11). Пусть - конгруэнция на ЛГп. Положим взаимосвязь между аксиомами логик SLn-конусов, порождающими разностями мономов идеалов вида V ( ) и порождающими элементами конгруэнции на Мп. Отсюда получается способ построения аксиом логик конусов SLn: В параграфе 2.5 доказывается теорема о нормальной форме в логике SLn. В параграфе 2.6 доказано, что конечно аксиоматизируемые расширения SLn являются логиками конечного числа SLn-KOiiycoB. В параграфе 2.7 определяется приведённый вид формул SLn:
О сохранении финитной аппроксимируемости для произведений
В параграфе 2.5 доказывается теорема о нормальной форме в логике SLn. В параграфе 2.6 доказано, что конечно аксиоматизируемые расширения SLn являются логиками конечного числа SLn-KOiiycoB.
В параграфе 2.7 определяется приведённый вид формул SLn: Определение (2.34). Будем говорить, что п-модальная формула А находится в приведённом виде, если Теорема (2.35). Каоїсдое конечно аксиоматизируемое расширение SLn аксиоматизируется формулой в приведённом виде. Среди приведённых формул выделяется подкласс вполне приведённых формул и доказывается Теорема (2.39). Каоїсдое конечно аксиоматизируемое расширение SLn аксиоматизируется формулой во вполне приведённом виде. При фиксированном порядке па мономах эта формула единственна с точностью до перестановок дизъюнктивных и конъюнктивных членов. В параграфе 2.8 с помощью леммы Кёнига доказывается конечная аксиоматизируемость всех расширений SLn. В параграфе 2.9 доказан алгоритмический вариант теоремы 2.39: Теорема (2.48). Для п-модальной формулы А мооїсно алгоритмически построить п-модальную формулу В во вполне приведённом виде, такую что Отсюда получаются следствия: Теорема (2.50). Проблема выводимости для логики SLn разрешима. Теорема (2.51). Каждое расширение SLn разрешимо. В параграфе 2.10 доказано (теорема 2.57), что по аксиоме расширения логики SLn можно алгоритмически распознать, является ли оно табличным. Дальнейшая часть второй главы посвящена доказательству теоремы 2.82: Теорема (2.82). Все расширения логики SLn финитно аппроксимируемы. В третьей главе рассматриваются свойства произведений расширений SLn и полных по Крипке многомодальных логик. В этой главе L - это непротиворечивое расширение логики SLn, Л - непротиворечивая полная по Крипке ш-модальная логика. Модальности в Л обозначаются как В параграфе 3.1 мы вводим определение перевода (n-fm)-модальной формулы в т-модальную: Определение (3.1). Распространим определения ф{А) и dl {А), 1 г п, (а, значит, и определения d (А) и D (А)) на формулы в языке L х Л добавлением следующих правил: ф (ЩА) =; Щф (A), dl {ЩА) ±=; Хг (А). Пусть А(р\, ... ,pk) - формула в языке L х Л, - конгруэнция на Мп. Полооїсим и доказываем основное свойство этого перевода Лемма (3.2). Пусть С - SL"-конус, F - т-модальная шкала Крипке, А -формула в языке L х Л. Тогда Используя это свойство, мы показываем, что для семантического произведения рассматриваемых логик финитная аппроксимируемость сохраняется: Теорема (3.3). Логика Л финитно аппроксимируема тогда и только тогда, когда логика L х Л финитно аппроксимируема. В параграфе 3.2 мы изучаем разрешимость семантического произведения данных логик. Для этого мы показываем, что произведение L х Л т-сводится (как множество формул) к Л: Лемма (3.4). Пусть L = (Ci,..., СЩ, где С\, ..., Ck - БЪп-конусы. Пусть А - формула в языке L х При помощи этой леммы мы показываем, что Теорема (3.5). Логика А разрешима тогда и только тогда, когда логика L х Л разрешима. Также мы может оценить сложность разрешающего алгоритма для произведения: Теорема (3.7). 1) По аксиоме логики L и разрешающему алгоритму для логики А можно построить разрешающий алгоритм для логики L х Л. 2) Если для логики А существует разрешающий алгоритм, время работы которого на формулах длины не более I не превосходит fi(l), а используемая память не превосходит /г(0 то для логики L х Л можно построить разрешающий алгоритм с соответствующими верхними оценками kifi(l) + gi(l), где k{ - константы, a gi - полиномы. В параграфе 3.3 сравниваются различные произведения указанных логик. Мы получаем достаточное условие простой перемножаемости: В четвёртой главе мы рассматриваем расширения логики SL.tn. Мы показываем, что решётка расширений логики SL.tn связана с подгруппами Zn подобно тому, как решётка расширений логики SLn связана с конгруэнци-ями на ЛЛ\ Используя эту связь, мы приводим более простое, чем для общего случая расширений SLn, доказательство финитной аппроксимируемости расширений логики SL.t". В параграфе 4.3 доказан следующий результат:
Порождающие множества подгрупп Zn
Зафиксируем логику L - расширение SLn. Так как множество формул логики L счётно, то L является объединением возрастающей последовательности конечно аксиоматизируемых логик Lf, без ограничения общности можно считать, что LQ = SLn. Так как логики Lj конечно аксиоматизируемы, то, по теореме 2.30, найдутся SLn-Konycbi Сц, ..., С , к{ 0, такие что
Положим ij i=; dj- Будем без ограничения общности считать, что при фиксированном і конгруэнции д, ..., ік. попарно несравнимы (действительно, большую из двух сравнимых конгруэнции можно отбросить так как, по лемме 2.10, логика соответствующего ей конуса больше). Заметим, что при этом условии, в силу леммы 2.37, множество { г? 1 J h] определяется по логике Li однозначно.
Заметим, что L0 = SL" = ЦС (Id(Nn))), т. е., kQ = 1, 0i= Id(Nn). Определение 2.40. Назовём цепочкой отобраоїсепие v отрезка [0, га] С N в множество N, такое что Число m назовём длиной I (г ) цепочки v. Рассмотрим множество Т всех цепочек и отношение R на Г такое, что (г/, v) Є R выполняется, если Напомним стандартное определение дерева: Определение. Пара (W, R) называется (направленным) графом, если R есть отношение на множестве W. Последовательность х$, ..., Xk,k 0, называется путём в графе (W, R), соединяющим Хо и Хк, если Х{ Є W при всех і и (7-1, Xj) Є R при 1 j к. Точка х Є W называется вершиной графа (W, R), если она соединяется с каоїсдой точкой в этом графе некоторым путём. Граф (W, R) называется деревом, если он имеет вершину и эта вершина соединяется со всеми точками графа единственным образом. Заметим, что вершина у дерева единственна. Высотой точки х дерева (W, R) называется длина пути из вершины этого дерева до точки х. Высотой дерева (W, R) называется максимум высот его точек. Уровнем высоты к дерева (W, R) называется множество элементов W с высотой к. Путём сквозь дерево (W, R) называется (конечная или бесконечная) последовательность Хо, х\, ... точек из W такая, что XQ - вершина (W, R), (хі,Хі+і) Є R и длина этой последовательности совпадает с высотой дерева (W,R). Доказательство. Рассмотрим цепочку VQ, такую что / (vo) — 0, г о(0) = 1, Покажем индукцией по длине цепочки г , что из неё можно за конечное число шагов спуститься по отношению R к цепочке VQ. ДеЙСТВИТеЛЬНО, ЄСЛИ I (v) = О, ТО V = VQ. Шаг индукции: пусть предположение индукции доказано для всех цепочек длины менее / (г ). Возьмём наибольшее m такое, что 0 m I (v) и """"то—l,v(m-l) т1 r Jm,v{m) Если такого m не существует, то при всех 0 і I (v) и, следовательно, (VQ, V) Є R. Иначе рассмотрим цепочку v , такую что / (г/) = m, v (i) = v(i) при і m. Тогда по выбору m имеем I (г/) I (v) и (і/, v) Є R. Учитывая, что для v предположение индукции верно, получаем, что шаг индукции выполняется. Для доказательства леммы осталось показать единственность v такого, что (г/, v) Є R. Действительно, пусть (г/, г ) Є Я и (у", v) Є R. Если I (v1) I (v"), то из (г/, v) Є R следует, что l(v")-l,v(l{v")-l) = l{v"),v(l(v")), что противоречит определению цепочки для v". Значит, l(v ) l{v")- Аналогично заключаем, что / (vr) I (г;"), значит I (г/) = / (г; 7). Из того, что при г» (г) = v(i) при і I {v ) и v"{i) = v(i) при і l(v"), заключаем, что г/ = v". Ш Лемма 2.42. Любая возрастающая последовательность о Q i Q конгруэнции на Мп стабилизируется. Доказательство. Рассмотрим конгруэнцию По теореме 1.57 и лемме 2.14(3), у идеала V ( ) есть конечный приведённый базис Грёбнера вида {xaj — xhj 1 j &}. Тогда, по лемме 2.23, конгруэнция порождена соответствующими парами (a.j,bj). Так как последовательность j возрастает, то найдётся число го, такое что a.j j0 by для каждого j. Поэтому = І0, следовательно, все конгруэнции i при і г о совпадают. Лемма 2.43. Для каждой цепочки v множество R(v) конечно. Доказательство. Покажем, что все цепочки в R(v) имеют одинаковую длину. Пусть Vі\ v" Є ПО Определению ЦепОЧКИ, 1(у )-1,у (1(і/)-1) СТрОГО СОДерЖИТСЯ В l(v )y(l(v )). Отсюда следует, что i(V ),V"(i(v )) строго содержится в i(v ),v (l(v )), чт0 противоречит несравнимости отношений л, ..., ifci Теперь утверждение леммы следует из того, что цепочек фиксированной длины существует лишь конечное число. Для доказательства конечности множества Т нам потребуется известная лемма (см., например, [33, с. 77]): Лемма 2.44 (Кёниг). Если дерево Т имеет бесконечную высоту и каждый уровень Т конечен, то найдётся путь сквозь Т. Лемма 2.45. Мпооїсество Т конечно. Доказательство. Докажем утверждение леммы от противного. Пусть множество Т бесконечно. По лемме 2.43, каждый уровень дерева (Т, R) конечен, поэтому, в силу бесконечности множества Т, дерево (Т, R) имеет бесконечную высоту и, по лемме Кёнига 2.44, найдётся путь VQ, V\, t 2, ... через дерево (Т, R).
