О модальных логиках элементарных классов шкал Крипке

Кикоть, Станислав Павлович

О модальных логиках элементарных классов шкал Крипке тема автореферата и диссертации по математике, 01.01.06 ВАК РФ

Кикоть, Станислав Павлович АВТОР

кандидата физико-математических наук УЧЕНАЯ СТЕПЕНЬ

Москва МЕСТО ЗАЩИТЫ

2010 ГОД ЗАЩИТЫ

01.01.06 КОД ВАК РФ

Диссертация по математике на тему «О модальных логиках элементарных классов шкал Крипке»

Автореферат диссертации на тему "О модальных логиках элементарных классов шкал Крипке"

Московский Государственный Университет имени М. В. Ломоносова

Механико-математический факультет

004ЬОИ1О г

На правах рукописи УДК 510.643

КИКОТЬ Станислав Павлович

О МОДАЛЬНЫХ ЛОГИКАХ ЭЛЕМЕНТАРНЫХ КЛАССОВ ШКАЛ КРИПКЕ

01.01.06— математическая логика, алгебра и теория чисел

АВТОРЕФЕРАТ

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

1 6 СЕН 2010

Москва 2010

004608107

Работа выполнена на кафедре математической логики и теории алгоритмов Механико-математического факультета Московского государственного университета имени М. В. Ломоносова.

Научный руководитель:

Официальные оппоненты:

доктор физико-математических наук, профессор В. Б. Шехтман.

доктор физико-математических наук, профессор Л. Л. Максимова

кандидат физико-математических наук, доцент М. Н. Рыбаков

Ведущая организация:

Математический институт им. В. А. Стеклова Российской академии наук.

Защита диссертации состоится 1 октября 2010 года в 16 часов 45 минут на заседании диссертационного совета Д.501.001.84 при Московском государственном университете имени М. В. Ломоносова по адресу: Российская Федерация, 119991, Москва, ГСП-1, Ленинские горы, д. 1, МГУ, Механико-математический факультет, аудитория 14-08.

С диссертацией можно ознакомиться в библиотеке Механико-математического факультета МГУ (Главное здание, 14 этаж).

Автореферат разослан 1 сентября 2010 года.

Учёный секретарь диссертационного совета Д.501.001.84 при МГУ, доктор физ.-мат. наук, профессор

Общая характеристика работы Актуальность темы

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

Начиная с конца 1950-х годов в модальной логике получила широкое распространение реляционная семантика Крипке1. Основная ее идея заключается в том, что формулы интерпретируются в реляционных структурах ("шкалах Крипке"), а формула Пф считается истинной в точке х, если ф истинна во всех точках, связанных с х по данному бинарному отношению.

Основная тема диссертации — связь между пропозициональными модальными формулами и классическими формулами первого порядка. Это — одна из традиционных тем современной модальной логики, начатая по существу еще в 1960-е гг. в работах С. Крипке и Е. Леммона. Как известно, общезначимость пропозициональной модальной формулы <р в семантике Крипке записывается в виде классической предикатной формулы второго порядка VPi... УРкф*(х, Pi,..., Р*) с кванторами общности по предикатным переменным. Однако оказывается, что во многих случаях эти кванторы элиминируются и общезначимость ц> выражается формулой 1-го порядка. В таких случаях модальная формула ф называется элементарной, а соответствующая ей формула 1-го порядка — модально определимой. Соответственно, класс шкал Крипке называется элементарным, если он задается формулой первого порядка.

Теорема Салквиста, доказанная в середине 1970-х гг., дает синтаксическое описание для широкого класса элементарных модальных формул, в который попадают аксиомы многих, но далеко не всех, известных модальных логик. Изучением элементарности и связанных с ней свойств модальных формул занимается так называемая "теория соответствия", основы которой были созданы в 1970-е гг. Р. Голдблаттом, И. Ван Бентемом и др. Эта теория занимает одно из центральных положений в модальной логике; на ней основаны исследования

'Kiipke, S. A Completeness Theorem in Modal Logic. Journal of Symbolic Logic, 24, No 1, 1959.

важнейших свойств модальных исчислений — полноты, финитной аппроксимируемости, конечной аксиоматизируемости и т. д. Нетривиальность теории соответствия подтверждается результатами JI.A. Чагровой:2 свойство элементарности для модальных формул и свойство модальной определимости для классических формул алгоритмически неразрешимы. К основным результатам теории соответствия относится и теорема Крахта,3'4 дающая синтаксическое описание классических формул первого порядка, соответствующих формулам Салквиста. На теории соответствия и, в частности, на теореме Крахта основаны некоторые алгоритмы поиска ответов на запросы к базам данных.5

Одним из трудных нерешенных вопросов в теории модальных логик остается вопрос о том, каким образом комбинировать логики с разнородными модальными операторами. Для работы с такого рода логиками в 1970е гг. было предложено интепретировать формулы в прямых произведениях реляционных структур, что послужило началом "многомерной модальной логики". Сейчас это интенсивно развивающийся раздел модальной логики; изложение основных результатов этой области содержится в книге Габбая, Куруш, Вольтера и Заха-рьящева.6 Кроме того, конструкции, похожие на произведения (предикатные шкалы Крипке с постоянной областью) возникают при изучении модальных и интуиционистских логик предикатов.7

Основные задачи многомерной модальной логики традиционны: установить аксиоматику для заданного класса структур-произведений, исследовать разрешимость и сложность получающихся логик.

Нетрудно установить,8 что прямое произведение элементарных классов шкал

2Chagrov, A. and Chagrova, L. The Truth About Algorithmic Problems in Correspondence Theory. Governatori, G., Hodkinson, I. and Venema, Y., editors Advances in Modal Logic 6. King's College Publications, 2006.

3Kracht, M. How completeness and correspondence theory got married. M. de Rijke (Ed.), Diamonds and Defaults. Synthese Library, Kluwer, 1993.

4Kracht, M. Tools and Techniques in Modal Logic. Elsevier, 1999, Studies in Logic and the Foundations of Mathematics, 142.

5Zolin, E. Query answering based on modal correspondence theory. Proceedings of the 4th "Methods for modalities" Workshop (M4M-4). 2005.

6Gabbay, D. etal. Many-dimensional modal logics: theory and applications. Elsevier, 2003, Studies in Logic and the Foundations of Mathematics, 148.

7Gabbay, D., Shehtman, V. and Skvortsov, D. Quantification in Nonclassica! Logic. Elsevier, 2009, Studies in Logic and the Foundations of Mathematics, 153.

6Gabbay, D. and Shehtman, V. Products of modal logics, part 1. Journal of the IGPL, 6, 1998.

Крипке элементарно. Поэтому изучение произведений тесно связано с исследованием произвольных элементарных классов шкал Крипке.

Однако модальные логики элементарных классов до сих пор были изучены недостаточно глубоко.

Только недавно9 была получена явная бесконечная модальная аксиоматика для произвольного элементарного класса. Однако в ряде случаев эта аксиоматика неожиданно оказывается конечной. Это обычно происходит, когда задающая класс первопорядковая формула оказывается модально определимой, поэтому задача об описании модально определимых формул первого порядка и связанных с ними элементарных модальных формул важна для модальной логики.

На протяжении 30 лет теорема Салквиста оставалась единственным в своем роде общим признаком элементарности модальных формул, и про элементарные формулы за ее пределами ничего не было известно. Ее нетривиальное обобщение, недавно найденное В, Горанко и Д. Вакареловым10,11 и, независимо, автором диссертации, является существенным продвижением в данной области. В работах Д. Вакарелова12,13 класс элементарных модальных формул синтаксически был расширен еще сильнее, но первопорядковые аналоги новых формул оказались эквивалентны старым.

Цель работы

Целью работы является изучение модальных логик различных элементарных классов шкал Крипке, в том числе

• описание новых видов элементарных модальных формул;

sHodHnson, I. Hybrid Formulas and Elementarily Generated Modal Logics. Notre Dame Journal of Formal Logic, 47, 2006, Nr. 4.

10Goranko, V. and Vakarelov, D. Sahlqvist Formulas Unleashed in Polyadic Modal Languages. Advances m Modal Logic 3. King's College Publications, 2000.

11Goranko, V. and Vakarelov, D. Elementary canonical formulae: extending Sahlqvist's theorem. Annals of Pure and Applied Logic, 141, 2006, Nr. 1-2.

12Vakarelov, D. Modal Definability in Languages with a Finite Number of Propositions! Variables and a New Extension of the Sahlqvist's Class. Balbiani, P. etal, editors Advances in Modal Lope 4. King's College Publications, 2002.

13Vakaxelov, D. Extended Sahlqvist Formulae and Solving Equations in Modal Algebras. 12-th International Congress of Logic Methodology and Philosophy of Science, August 7-13. Abstracts. Oviedo, Spain, 2003.

• описание новых видов модально определимых формул первого порядка;

• использование найденных формул для изучения квадратов модальных логик с выделенной диагональю.

Научная новизна

Основные результаты диссертации являются новыми и состоят в следующем:

1) Получено новое доказательство обобщенной теоремы Салквиста, первоначально опубликованной в работах В. Горанко и Д. Вакарелова.14'15 Это доказательство получено независимо и, в отличие от доказательства В. Горанко и Д. Вакарелова, дает явные формулы для минимальной оценки.

2) Получено явное синтаксическое описание формул первого порядка, которые являются переводами обобщенных формул Салквиста (обобщение теоремы Крахта).

3) Построен новый пример обобщенной формулы Салквиста, которая не эквивалентна никакой стандартной формуле Салквиста.

4) Получен критерий модальной определимости для экзистенциальных формул первого порядка, бескванторная часть которых представляет собой конъюнкцию атомарных.

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

6) Показано, что логики квадратов шкал Крипке с выделенной диагональю, как правило, не аксиоматизируются при помощи формул с фиксированным конечным множеством переменных.

Методы исследования

Обобщённая теорема Салквиста доказывается аналогично стандартной, с использованием метода ван Бентема подстановки минимальных оценок16 и топо-

14Goranko, V. and Vakarelov, D. Sahlqvist Formulas Unleashed in Polyadic Modal Languages. Advances in Modal Logic 3. King's College Publications, 2000.

15Goranio, V. and Vaiarelov, D, Elementary canonical formulae: extending Sahlqvist's theorem. Annals of Pure and Applied Logic, 141, 2006, Nr. 1-2.

16Blackbum, P., Kijke, M. de and Venema, Y. Modal Logic. Cambridge University Press, 2002.

логических свойств канонической шкалы17,18.

Для доказательства неэквивалентности обобщенных формул Крахта стандартным формулам Крахта используются теоретико-модельные игры.

Для доказательства модальной неопределимости диаграмных формул с циклом используется инвариантность модальных формул относительно ультрарасширений.

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

Для доказательства конечной неаксиоматизируемости логик квадратов шкал Крипке с выделенной диагональю в главе 4 используются обобщенные формулы Салквиста, которые строятся при помощи алгоритма, изложенного в главе 3.

Теоретическая и практическая ценность

Работа имеет теоретический характер. Полученные в ней результаты могут найти применение в математической логике и информатике.

Апробация работы

Результаты диссертации докладывались:

• на научно-исследовательском семинаре кафедры математической логики и теории алгоритмов механико-математического факультета МГУ под руководством академика РАН С.И. Адяна, член-корр. РАН Л.Д. Беклемишева и проф. В.А. Успенского, и других семинарах кафедры (2003-2010 гг.);

• на Международной конференции «Алгебраические и топологические методы в неклассических логиках II» (Барселона, Испания, 2005);

• на Международной конференции «Приложения модальной логики в информатике» (Москва, 2005);

• на Международной конференции «Advances in Modal Logic, 2008» (Нанси, Франция, 2008);

17Sambin, G. and Vaccaro, V. Topology and duality in modal logic. Annals of Pure and Applied Logic, 37,1988.

18Sambin, G. and Vaccaro, V. A topological proof of Sahlqvist's theorem. Journal of Symbolic Logic, 54, 1989.

• на XXXI конференции молодых ученых (МГУ, 2009);

• на Международной конференции «Advances in Modal Logic, 2010» (Москва, 2010).

Публикации

Результаты автора по теме диссертации опубликованы в 7 работах, список которых приведен в конце автореферата [1-7].

Структура и объем диссертации

Диссертация состоит из введения, четырех глав, приложения и библиографии (38 наименований). Общий объем диссертации составляет 123 страницы.

Краткое содержание диссертации

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

Фиксируем счетное множество пропозициональных переменных PV и некоторое множество индексов Н.

ОПРЕДЕЛЕНИЕ 1. Формулы языка М1~ (модальные формулы) строятся рекурсивно с помощью переменных из PV, констант «ложь» (_1_), «истина» (Т), логических связок A, V, —и двойственных друг к другу модальностей О^ и О^ для каждого £ € Е.

ОПРЕДЕЛЕНИЕ 2. Формула называется позитивной, если она не содержит связок -1 и -+ (но может содержать _L). Формула называется негативной, если она есть отрицание позитивной.

ОПРЕДЕЛЕНИЕ 3. Шкалой Крипке для языка Mis называется набор F = (IV, (Щ : £ £ Е)), где Щ С W х W для каждого £ £ S. Элементы множества W мы будем называть точками.

ОПРЕДЕЛЕНИЕ 4. Оценкой в шкале Крипке F = (W, (Rf.Çe H)) называется отображение 9 : PV. —+ 2W, которое каждой пропозициональной переменной ставит в соответствие множество точек шкалы Крипке.

ОПРЕДЕЛЕНИЕ 5. Моделью Крипке, построенной на шкале F, называется пара M = (F, 6), где в — оценка в шкале F.

ОПРЕДЕЛЕНИЕ 6. Истинность формулы в точке модели M = (F, 9) определяется стандартным образом:

• в точке х переменная р € PV истинна, если ж € 0(р);

• значения булевых связок вычисляются в точке по классическим таблицам истинности;

• в точке х истинна формула О^ф, если найдется такая точка у € Rç{x) в которой верна формула ф\

Запись F,w,9 \= ф означает, что формула ф истинна в точке w модели M — (F,9).

ОПРЕДЕЛЕНИЕ 7. Запись F,w |= ф означает, что формула ф истинна в точке w любой модели М, построенной, на шкале F.

ОПРЕДЕЛЕНИЕ 8. Формула ф общезначима на шкале F, если она истинна во всех точках любой модели М, построенной на шкале F.

Шкалу Крипке F = (W, (Щ : £ S S)) можно рассматривать как классическую модель для языка первого порядка £/н, содержащего равенство, бинарные предикатные символы Щ для каждого £ S 5, предметные переменные и кванторы.

ОПРЕДЕЛЕНИЕ 9. Первопорядковая формула А(х) языка £/2 с одной свободной переменной х (локально) соответствует модальной формуле ф языка Mis, если в любой шкале Крипке F для любой ее точки w

F,w |= ф Ч=Ф> в F (как в классической модели) верна формула

ОПРЕДЕЛЕНИЕ 10. Первопорядковая формула А(х) языка £/Е с одной свободной переменной х называется модально определимой, если она соответствует некоторой модальной формуле ф.

ОПРЕДЕЛЕНИЕ 11. Первопорядковая формула А(хь... ,хп) языка С} со свободными переменными х1,...,хп называется модально определимой, если существует такая последовательность модальных формул фх,..., фп, что в любой шкале Крипке .Р для любых ее точек

для любой оценки в для некоторого г (1 < г <п) Р, ад,-, в \=

-<=>- в ^(классически) верна формула А(тх,..., адп).

ОПРЕДЕЛЕНИЕ 12. Модальная формула называется (локально) элементарной, если она соответствует некоторой формуле первого порядка языка £/н.

ОПРЕДЕЛЕНИЕ 13. Обобщенной шкалой Крипке для языка МЦ называется набор Р = : £ е Н), А), где Щ С Ш X ]¥ для всех £ £ 5, А С и Л замкнуто относительно булевых операций и операции V —+ Д^1 (ДООПРЕДЕЛЕНИЕ 14. Пусть Р = (IV, (Щ : £ 6 Е), А) - обобщенная шкала Крипке. Оценка в : РУ —+ 2У/ называется допустимой для Р, если она принимает значения в А.

ОПРЕДЕЛЕНИЕ 15. Модальная формула общезначима, в обобщенной шкале Р, если она верна во всех точках шкалы при любой допустимой для Р оценке.

Положим для V С Щ Щ{у) = {х | Щ{х) С V}.

ОПРЕДЕЛЕНИЕ 16. Обобщенная шкала Крипке Р = (IV, Щ, А) называется

• различимой, если для любых различных х,у из найдется такое V 6 А, что х б V и у ^ У'.

• тугой, если

€ А \ ад с У} С Щ{хУ,

• компактной, если любое центрированное семейство 1Л С А имеет непустое пересечение.

• дескриптивной, если Р различима, туга и компактна.

ОПРЕДЕЛЕНИЕ 17. Модальная формула ф называется ¿-упорной, если для любой дескриптивной обобщенной шкалы Р = (ТУ, (Щ : £ <£ Е), Л) из общезначимости ф на Г, следует ее общезначимость и на соответствующей обычной шкале Крипке = (И7, (Д5: £ € 5)).

Вторая глава посвящена обобщенным формулам Салквиста и их первопо-рядковым аналогам — обобщенным формулам Крахта.

Будем считать, что множество переменных РУ разбито на счетное множество счетных группр\,р\,Рг, ■ - •> РиРъР\> • ■ •> рЬрЪрЪ • ■ ■ и т. д. Верхний индекс (называемый рангом) означает номер группы, а нижний — номер переменной в пределах группы.

ОПРЕДЕЛЕНИЕ 18. Регулярная О-формула ранга к определяется по индукции. Именно,

• любая переменная р^ ранга к является П-формулой ранга к,

• если РОБ — позитивная модальная формула, зависящая только от переменных, ранг которых меньше к и ф —регулярная Ш-формула ранга к, то РОБ — регулярная О-формула ранга к.

• если ф —регулярная О-формула ранга к, то О^ф — тоже регулярная формула ранга к.

ОПРЕДЕЛЕНИЕ 19. Обобщенной импликацией Салквиста называется формула вида 6'5Л —> где СБА построена из регулярных О-формул и негативных формул при помощи А, V, О^.

ОПРЕДЕЛЕНИЕ 20. Обобщенной формулой Салквиста называется модальная формула, построенная из обобщенных импликаций Салквиста при помощи А, а также V, применяемой к формулам без общих пропозициональных переменных.

ТЕОРЕМА 21 (Обобщенная теорема Салквиста). Каждая обобщенная формула Салквиста элементарна и ¿-упорна.

ОПРЕДЕЛЕНИЕ 22. Модальная логика А называется полной, если она совпадает с множеством формул, общезначимых на некоторой шкале Крипке.

СЛЕДСТВИЕ 23. Логика, аксиоматизируемая обобщенными формулами Салквиста, полна.

ОПРЕДЕЛЕНИЕ 24. Ь-термом называется терм в языке, алфавит которого состоит из символов П, и, Щ1, Щ, Т, _]_. Здесь Т — константы, {ж,}

— переменные, Щ Щ — одноместные функциональные символы, Л, и — бинарные функциональные символы.

ОПРЕДЕЛЕНИЕ 25. Назовем 1г-терм я полубезопасным, если верно одно из следующих условий:

1) в = {х{};

2) г = Дс(й'), где б1 полубезопасен;

3) з = г' Л в", где либо в', либо в" полубезопасен.

1-терм í называется безопасным, если он полубезопасен, и в каждом его подтерме вида терм в полубезопасен.

ОПРЕДЕЛЕНИЕ 26. Формулы с ограниченными кванторами имеют вид: (УхI х^а := Ух{{х}Щх{ —> а); (Зх; := Зх^х^Щх^ А а).

, Рассмотрим язык первого порядка содержащий предметные переменные х*, логические связки Л и V, ограниченные кванторы и атомарные формулы вида [г> е Е , где Е — безопасный терм.

Ясно, что любую такую формулу можно перевести на классический язык первого порядка, заменив предикатный символ у € Е на его перевод Е*(ь), где

{^}*(г>) := (V = х{); Т»:=Т;

(ElUE2r(v):=^(v)VE¡(vУ¡

ШЕ))» := 3у(уЩу Л Я*(«)[у/«]).

В последних трех случаях у должна быть некоторой новой переменной, не встречающейся в формуле Е*(у).

ОПРЕДЕЛЕНИЕ 27. Формула А(х0) в языке называется обобщенной формулой Крахта, если она содержит ровно одну свободную переменную хо и построена из формул вида | у £ Щ при помощи конъюнкции, дизъюнкции и ограниченных кванторов, причем для каждой подформулы вида у € Е\, входящей в Л(жо), все переменные х;, входящие в Е, квази-свободны, то есть связаны ограниченным квантором всеобщности, который не находится под действием никакого ограниченного квантора существования.

ТЕОРЕМА 28 (Обобщенная теорема Крахта).

• Каждая обобщенная формула Салквиста соответствует некоторой обобщенной формуле Крахта.

• Каждая обобщенная формула Крахта соответствует некоторой обобщенной формуле Салквиста.

Возникает естественный вопрос: будет ли семантически класс обобщенных формул Крахта шире класса стандартных формул Крахта? Ответ на этот вопрос дает следующая

ТЕОРЕМА 29. Обобщенная формула Крахта

/с = Уза >1 хУх2 >2 хУхз !>з хЗу' >1 хЗу" >2 у'Зу >з у"

выражающее "свойство куба" трехмерного произведения шкал Крипке, не эквивалентна никакой стандартной формуле Крахта.

Третья глава посвящена формулам первого порядка с одной свободной переменной, которые можно проиллюстрировать специальным чертежом — диаграммой. -

На Рис. 1 приведены простейшие примеры таких диаграмм: (условия станут более привычными, если их мысленно дополнить квантором всеобщности по х)

1) транзитивность: УуУ^хЯг/ А у Яг —» хЯх).

2) плотность: Уг(хНг Зу{хЯу А уЯг)).

3) полукоммутативность: Vу(хВ,2В.1У —► хЯхДгУ)-

3) 4)

Рис. 1: Примеры диаграмм

4) свойство Черча-Россера: УуУг{х]Ц\у Л хН2г —► Зь(уН2У Л гК^)).

5) сериальность: 3у хЯу.

6) симметричность: Уу(хЯу —> у Их).

Сначала мы рассматриваем так называемые экзистенциальные диаграммы, которые получаются из приведенных рисунков удалением сплошных стрелок.

ОПРЕДЕЛЕНИЕ 30. Экзистенциальной диаграммой называется набор С = (ТУ, ]¥ч, ТУЕ,Пь..., П.), где ТУ = Ж, О \УВ, Ж, П ТУВ = 0 и П; С IV х IV.

Положим \УЧ — {хх,..., хп}, = {у\,..., ут}. Точки множества будем называть черными, а точки множества \¥п — белыми. Каждой точке г € IV поставим в соответствие предметную переменную ьг.

Каждой экзистенциальной диаграмме С поставим в соответствие формулу Кс в языке первого порядка с в бинарными предикатами .. -, и ть Ч~ тп свободными переменными ух1,...,ухп1ьуг}...1 уУт

кС=\Г\ А

и формулу Ес в том же языке первого порядка с п свободными переменными

Ух! 1 ... 7 Ухп

Ес = ЗуУ1...ЗуУтКс.

ОПРЕДЕЛЕНИЕ 31. Экзистенциальная диаграмма С называется определимой, если первопорядковая формула Ес(уХ1,..., уХп) модально определима.

ОПРЕДЕЛЕНИЕ 32. Пусть А{уъ ..., О и В{уъ ...,уп) -две формулы языка £/ с одними и теми же свободными переменными. Мы говорим, что из формулы А следует формула В (обозначаем А \= В), если А -» В классически общезначима.

ОПРЕДЕЛЕНИЕ 33. Экзистенциальная диаграмма С называется минимальной, если для любой диаграммы С", которая получается из диаграммы С удалением какой-нибудь стрелки, из формулы Ес' не следует формула Ес.

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

ОПРЕДЕЛЕНИЕ 34. Направленным путем в экзистенциальной диаграмме С, соединяющим точку х с точкой у, называется такая последовательность а^агб• • • б^м-ъ гДе Для всех г от 1 до к с^ € V/, & € {1,...,з} и (а,, азд) 6 и, к тому же, ах = х и аш = у.

Ненаправленный путь отличается от направленного тем, что условие а;+1) € П^ заменяется на (а;, а1+х) 6 П^ и П^1.

ОПРЕДЕЛЕНИЕ 35. Экзистенциальная диаграмма называется достижимой, если для любой белой точки у найдется черная точка х, такая что существует направленный путь, соединяющий точки х и у, все точки которого, кроме х — белые.

ОПРЕДЕЛЕНИЕ 36. Экзистенциальная диаграмма называется связной, если любые две белые точки можно соединить ненаправленным путем, все точки которого белые.

ОПРЕДЕЛЕНИЕ 37. Пусть С — (Ш, Шч, Шв, Пь ..., Па) - экзистенциальная диаграмма. Мы говорим, что она содержит петлю, если для некоторых х € и £ 6 {1,..., й} (х, х) е П^. Мы говорим, что она содержит кратное ребро, если для некоторых £2 е {1,.. -, й}, & ф £> (И^ х И^) Л П П6 ф 0, или же для некоторых, возможно равных, £ъ £2 € {1,. - ■, з}, найдутся точки 1,1/6 Шв, такие что хП^у и уЩ2х. Мы говорим, что диаграмма содержит внутренний цикл, если она либо содержит петлю, либо кратное ребро, либо ненаправленный путь сц^а^ • ■. Сдад+г = <*1 (Л > 3), у которого все вершины — белые, и все вершины которого, кроме первой и последней, попарно различны.

ТЕОРЕМА 38. Если достижимая минимальная экзистенциальная диаграмма содержит внутренний цикл, то она модально неопределима.

ТЕОРЕМА 39. Если достижимая связная экзистенциальная диаграмма не содержит внутренних циклов, то она модально определима.

СЛЕДСТВИЕ 40 (Критерий определимости). Достижимая связная мини/

мальная диаграмма модально определима тогда и только тогда, когда она не содержит внутренних циклов.

СЛЕДСТВИЕ 41. Если достижимая экзистенциальная диаграмма С не содержит внутренних циклов, то задаваемая ей первопорядковая формула Ес(ьХ1,... ,уХп) представляет собой конъюнкцию определимых первопорядко-вых формул.

Далее рассматриваются диаграммы со сплошными стрелками.

ОПРЕДЕЛЕНИЕ 42. Пусть дана шкала Крипке Т = (\У,ПЬ...,К3). Два направленных пути х\, £х, хг, £2, • • • Хп и уг, ¡¿х, Уг, И2, ■ ■ ■ Ут мы считаем равными, если т = п, Х{ = у, для всех 1<г<пи& = /^ для всех 1 < г < п — 1. Пара Т = (Т, г) называется деревом с корнем г, если

• г £ Ж,

• — 0 для всех £ € Н,

• для любой точки х, отличной от корня, существует единственный путь, соединяющий тех.

ОПРЕДЕЛЕНИЕ 43. УЗ-диаграммой будем называть набор Б = (И7, Жч, Вх,..., В3, Щ,...,П31 г), где Ж — конечное множество, Ж = Ж и \Уе, Жч П = 0, В\,...,Вв — бинарные отношения на Ж,, Пх,...,— бинарные отношения на Ж и г € \УЧ, причем структура (Ж,,Въ...,В3,г) представляет собой дерево с корнем г. Элементы множеств В^ и Пу будем называть соответственно черными и белыми стрелками.

ОПРЕДЕЛЕНИЕ 44. Экзистенциальной частью УЗ-диаграммы В = (Ж Ж,,Жв,Бх,..., В„ Пх,... ,П5,7~) будем называть экзистенциальную диаграмму С = (Ж, Жч, Жв, Пх,..., П3).

Как и для экзистенциальных диаграмм, положим Ж, = {хо,хх,...,х„}, Жв = {ух,... ,Ут}, причем будем считать, что х0 — г, и каждой точке г е Ж поставим в соответствие предметную переменную уг.

Каждой УЗ-диаграмме V поставим в соответствие первопорядковую формулу Ец с одной свободной переменной уХо в сигнатуре с бинарными предикатными символами Ну,..., Лг:

а С — экзистенциальная часть Б.

ОПРЕДЕЛЕНИЕ 45. УЗ-диаграмма В = {IV, \УЧ, Ву,..., В„ Пь..., П„ г) называется минимальной (соответственно, достижимой, содержащей внутренний цикл), если ее экзистенциальная часть обладает соответствующим свойством.

ОПРЕДЕЛЕНИЕ 46. УЗ-диаграмма В = (Ш, Шч, \УВ, Ву,..., Вя, Пь..., П5, г)

называется модально определимой, если формула Ец модально определима.

ТЕОРЕМА 47. Если достижимая УЗ-диаграмма О не содержит внутренних циклов, то она модально определима.

В Приложении мы приводим критерий модальной определимости для некоторого класса УЗ-диаграмм.

В четвертой главе методы, разработанные в главах 2 и 3, применяются к модальным логикам квадратов шкал Крипке с выделенной диагональю. Основной результат главы — неаксиоматизируемость большого числа таких логик при помощи формул с конечным числом переменных.

Для работы с двумерными произведениями с выделенной диагональю используется язык М1/2- Его алфавит получается из бимодального языка добавлением пропозициональной константы 5.

Для языка М1} шкалой Крипке будем называть набор Р1 = К», А),

где Д: С № х 1У (£ <Е {/I, и}). Д С W; моделью Крипке называется пара М = (Р, б), где Р — шкала Крипке, а в — оценка в шкале

Определение истинности формулы в модели Крипке получается из Определения 6 добавлением пункта

Ев = ЧуХ1...ЧУх„(Е£^Ес),

где

• формула <5 истинна в точности в точках множества Д.

На этот язык очевидным образом переносится понятие общезначимости формулы.

ОПРЕДЕЛЕНИЕ 48. Множество формул £ аксиоматизирует логику L, если L является минимальным множеством формул, содержащим все пропозициональные тавтологии, формулы К^, Kv, где

Kt = D?(p -+q)-> -у П£9),

множество формул £, и замкнутое относительно правил вывода Modus Ponens, правила подстановки и правила обобщения:

А,А-*В А А

В ' \В/р}А ' ЩА '

ОПРЕДЕЛЕНИЕ 49. Модальная логика L аксиоматизируема формулами с конечным числом переменных, если существует такое множество модальных формул Е, что оно аксиоматизирует логику L, ив формулы £ входит лишь конечное число переменных.

ОПРЕДЕЛЕНИЕ 50. Пусть F = (W, R) - 1-шкала Крипке. Через Ff обозначим шкалу (W х W,Rh.,Rv, А), где

(а, b)Rh(c, d) <=?> aRc и b — d;

(а, b)Ro{c, d) a = с и bRd, А = {(а, а) | а e W}. Такую шкалу мы будем называть 5-квадратом шкалы F. ОПРЕДЕЛЕНИЕ 51. Пусть С — класс 1-шкал Крипке. Положим

C| = {i?|FGC}.

ОПРЕДЕЛЕНИЕ 52. Пусть L — полная по Крипке 1-модальная логика. 6-квадратом логики L (обозначается Lg) называется множество всех формул, общезначимых на классе C(L)|, где C(L) — класс всех 1-шкал Крипке, на которых общезначима логика L.'

Щ ^

Рис. 2: Шкалы £>| и

Чтобы точно сформулировать результат о неаксиоматизируемости формулами с конечным числом переменных, рассмотрим следующие шкалы Крипке (см. Рис. 2).

Формально, Щ = (В.сп) /где

= {(0, г) | 1 < г < п) и {(».¿) | 1 < ^ ^ ^ < п} и {(г, с) | 1 < г < п}, а О; = (ИМ, где

И^ = {г,1,...п}, Я£={М |1<г<п}.

ТЕОРЕМА 53. Пусть Ь — полная по Крипке 1-модальная логика, и С(Ь) содержит все шкалы вида и Отп или все их рефлексивные замыкания, или все их транзитивные замыкания, или все их рефлексивные транзитивные замыкания. Тогда Ь\ не аксиоматизируема формулами с конечным числом переменных.

СЛЕДСТВИЕ 54. Дельта-квадрат любой полной по Крипке логики Ь, такой что КС Ь С СЬ или КСЬС Сгг, не аксиоматизируем формулами с конечным числом переменных.

Благодарности

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

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

1. Кикоть, С. О квадратах модальных логик с выделенной диагональю. Математические заметки, 88(2), 2010, 261-274.

2. Kikot, S. An extension of Kracht's theorem to generalized Sahlqvist formulas. Journal of Applied Non-Classical Logic, 19/2, 2009, 227-251.

3. Kikot, S. Semantic characterization of Kracht's formulas. Advances in Modal Logic 8. College Publications, 2010,218-234.

4. Кикоть, С. О модальной определимости некоторых формул первого порядка. Рукопись депонирована в ВИНИТИ 29.04.2010, ДО234-В2010, Указатель №6, 2010, 27 стр.

5. Kikot, S. Formulas, corresponding to diagrams. International Conference "Computer science applications of modal logic". Abstracts. Independent University of Moscow, 2005, 18-19.

6. Kikot, S. A new generalization of Sahlqvist theorem. Algebraic and Topological Methods in Non-classical Logics II, Abstracts, Universität de Barcelona. Barcelona, 2005,40-41.

7. Кикоть, С. Об аксиоматике модальных логик квадратов шкал Крипке с выделенной диагональю. Тезисы докладов секции "Математика и механика" Международной конференции студентов, аспирантов и молодых ученых "Ломоносов-2009". Москва, 2009, 33-34.

Подписано в печать 30.02, 4О Формат 60x90 1/16. Усл. печ. л. {,6 Тираж /00 экз. Заказ ЗО

Отпечатано с оригинал-макета на типографском оборудовании механико-математического факультета МГУ вмени М.В.Ломоносова

Содержание диссертации автор исследовательской работы: кандидата физико-математических наук, Кикоть, Станислав Павлович

Введение

Краткое содержание диссертации

1 Предварительные сведения из модальной логики

1.1 Синтаксис.

1.2 Семантика Крипке.

1.3 Конструкции, сохраняющие истинность

1.4 Обобщенные шкалы.

1.5 Теоремы Салквиста и Крахта.

2 Обобщенные формулы Салквиста

2.1 Регулярные П-формулы.

2.2 Безопасные термы.

2.3 Обобщенные формулы Салквиста.

2.4 d-упорство

2.5 Обобщенные формулы Крахта.

2.5.1 Определения и примеры

2.5.2 Квази-безопасные выражения.

2.5.3 Доказательство обобщенной теоремы Крахта.

2.6 Неэквивалентность обобщенных формул Крахта стандартным.

3 Формулы, соответствующие диаграммам

3.1 Постановка задачи.

3.2 Экзистенциальные диаграммы.

3.3 Неопределимые экзистенциальные диаграммы

3.4 Определимые экзистенциальные диаграммы.

3.5 Достаточное условие модальной определимости для УЗ-диаграмм

4 Двумерные модальные логики с выделенной диагональю.

4.1 Формулировка теоремы

4.2 Доказательство основной теоремы.

Введение диссертация по математике, на тему "О модальных логиках элементарных классов шкал Крипке"

Актуальность темы

Модальная логика изучает модальные операторы — математические модели языковых конструкций, которые действуют как одноместные пропозициональные связки.

Сюда относятся самые разнообразные операторы, касающиеся необходимости и возможности ("необходимо, что" и "возможно, что"), доказуемости ("доказуемо, что."), знания ("Агент А знает, что."), веры ("Агент А верит, что."), пространства ("везде", "где-то", "в некоторой окрестности", "в Москве"), времени ("всегда", "всегда в будущем", "завтра"), и др. Модальная логика тесно связана с логикой первого поI рядка, а именно, классические кванторы Ух и Эж тоже можно считать модальными операторами. В настоящее время модальная логика активно развивается, благодаря разнообразным применениям — в том числе в информатике, математической лингвистике и основаниях математики.

Начиная с конца 1950-х годов в модальной логике получила широкое распространение реляционная семантика Крипке [26]. Основная ее идея заключается в том, что формулы интерпретируются в реляционных структурах ("шкалах Крипке"), а формула □ ф считается истинной в точке х, если ф истинна во всех точках, связанных с х по данному бинарному отношению.

На основе семантики Крипке были вскоре построены адекватные семантики для большого числа модальных исчислений, и была разработана соответствующая теоретико-модельная техника. Появились и общие результаты о семантике модальных логик, такие как теорема Салквиста [30] или Гольдблатта-Томасона [10]. Появились и отрицательные результаты: примеры неполных по Крипке модальных исчислений, исчислений с алгоритмически неразрешимой проблемой вывода.

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

Для работы с такого рода операторами в 1970ее гг было предложено интепре-тировать формулы в прямых произведениях реляционных структур, что послужило началом "многомерной модальной логики". Сейчас это активно развивающийся раздел модальной логики; систематическое изложение теории произведений содержится в книге [7]. Также отметим, что конструкции, похожие на произведения (предикатные шкалы Кринке с постоянной областью), возникают при изучении модальных и интуиционистских логик предикатов [9].

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

Нетрудно установить [8], что прямое произведение элементарных классов элементарно. Поэтому изучение произведений тесно связано с исследованием произвольных элементарных классов шкал Крипке, которому посвящена настоящая диссертация.

Однако модальные логики элементарных классов до сих пор были изучены недостаточно глубоко.

Из положительных результатов отметим теорему Салквиста ([30]; современное изложение см. в [2],[4]), описывающую большой класс элементарных канонических модальных формул, и теорему Крахта ([24], [25]), описывающую их классические первопорядковые эквиваленты.

Большинство современных доказательств теорем о полноте для различных модальных логик опираются на теорему Салквиста. В связи с этим существенным продвижением является обобщение теоремы Салквиста ([11], [12], [21]), которому посвящена глава 2 этой диссертации, так как оно существенно расширяет класс известных элементарных модальных формул и полных модальных логик. В работах [34], [35] класс элементарных модальных формул синтаксически был расширен еще сильнее, но первопорядковые аналоги новых формул оказались эквивалентны старым. Ведутся работы по компьютерному поиску элементарных модальных формул [5], [6].

Можно еще отметить недавнюю работу [15], приводящую явную бесконечную модальную аксиоматику для любого элементарного класса, а также работу [1], в которой показано, как существенно упростить эту аксиоматику для ряда особых случаев.

Однако, поиски общих результатов о модальных логиках элементарных классов шкал, (например, критерия конечной аксиоматизируемости), принципиально ограничены неразрешимостью классической логики первого порядка. Общие проблемы "по первопорядковой формуле определить, является ли она модально определимой", и "по модальной формуле определить, является ли она элементарной" алгоритмически неразрешимы [3].

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

В [37] модальная определимость формул первого порядка используется для конструирования алгоритмов, отвечающих на запросы к базам данных. Также в этой работе доказан частный случай Теоремы 3.16 для случая одной единственной черной точки. Интересно, что в этом доказательстве использовались операции на графах, аналогичные последовательному и параллельному соединению проводников.

В главе 4 изучается общая конструкция ¿-квадрата произвольной 1-модальной логики Ь. Именно, ¿-квадратом 1-шкалы Кригхке Р — К) называется шкала {XV х И7, 74, Нь,. А), где Я^, Я^ — стандартные вертикальные и горизонтальные отношения, а диагональ Д = {(а, а) | а £ И^}. ¿-квадратом 1-модальной логики Ь называется множество формул в языке с модальностями 0/(, и пропозициональной константой ¿, общезначимые на ¿-квадратах всех шкал многообразия логики Ь (6 верна в точности в точках диагонали).

Эта конструкция обобщает обычное произведение модальных логик по аналогии с давно известным построение логики 5-квадратов шкал Крипке с унивесальным отношением Бб^,, связанной с цилиндрическими алгебрами.

Напомним, что представимой цилиндрической алгеброй размерности п над множеством IV называется множество всех подмножеств с операциями цилиндри-фикации

Зг(т4) = {Ь | Ь =г а для некоторого а & А}, где запись Ь а означает, что кортежи Ь и а совпадают на всех своих элементах, кроме, быть может, г-ого, и выделенными элементами

4,- = {а | (11 = а^}, где щ и а^ обозначают г-ый и ^'-ый элементы кортежа. Элементы могут отсутствовать; в этом случае говорят о бездиагональных цилиндрических алгебрах.

Это понятие было введено Тарским в конце сороковых для алгебраической интерпретации логики предикатов, и представляет собой один из основных объектов исследования алгебраической логики. Цилиндрические алгебры тесно связаны с многомерными медальными логиками: например, многообразие бездиагональных пред-ставимых цилиндрических алгебр размерности п совпадает с многообразием модальных алгебр логики Эб™.

Легко видеть, что модальная алгебра декартова квадрата шкалы Р = (\¥,1Ух \¥) с отмеченной диагональю является представимой цилиндрической алгеброй размерности 2. Поэтому логика Бб^ [29] соответствует универсальному фрагменту теории представимых цилиндрических алгебр размерности 2. Используя аксиоматику для этой цилиндрической алгебры из [14], Иде Винема в [36] построил конечную аксиоматику для логик Бб^, и 85^.

Как оказалось, конечная аксиоматика для Бб^, является скорее исключением, чем правилом для квадратов. Основной результат главы 4 этой диссертации заключается в том, что, в отличие от обычных произведений, которые часто обладают конечной аксиоматикой ([38], см. также теорему 5.9 на стр. 230 в [7]), для любой модальной логики Ь, такой что К С Ь С Сгг или КС1С СЬ, ее 5-квадрат не аксиоматизируем при помощи конечного количества переменных. Используемый метод доказательства восходит к работе [16].

Весьма трудны и интересны алгоритмические вопросы, связанные с ¿-квадратами. Недавно было показано [29], что многие ¿-квадраты (среди которых логика не финитно аппроксимируемы. В самое последнее время автором совместно с А. Куруш была установлена неразрешимость логики но вопрос о разрешимости логик и Т^ пока открыт.

Цель работы

Целью данной работы является изучение модальных логик различных элементарных классов шкал Крипке.

Научная новизна

Основные результаты диссертации являются новыми и состоят в следующем:

1) Получено новое доказательство обобщенной теоремы Салквиста, первоначально опубликованной в работах [11] и [12]. Это доказательство получено независимо, не использует многоместных модальностей и, в отличие от доказательства В. Горанко и Д. Вакарелова, дает явные формулы для минимальной оценки.

2) Получено явное синтаксическое описание формул первого порядка, которые являются переводами обобщенных формул Салквиста.

4) Получен критерий модальной определимости для экзистенциальных формул первого порядка, бескванторная часть которых представляет собой конъюнкцию атомарных. Критерий заключается в отсутствии в графе, соответствующем формуле, циклов специального вида. Для определимых формул предъявлен алгоритм построения определяющего вектора модальных формул.

6) Показано, что логики квадратов шкал Крипке с выделенной диагональю, как правило, не аксиоматизируются при помощи формул с фиксированным конечным множеством переменных. Методы исследования

Обобщенная теорема Салквиста доказывается аналогично стандартной, с использованием метода ван Бентема подстановки минимальных оценок [2] и топологических свойств канонической шкалы [31], [32].

Для доказательства конечной неаксиоматизируемости логик квадратов шкал Крипкс с выделенной диагональю в главе 4 используются обобщенные формулы Салквиста, которые строятся при помощи алгоритма, изложенного в главе 3.

Теоретическая и практическая ценность

Работа носит теоретический характер. Полученные в ней результаты могут быть полезны специалистам, работающим в МГУ им. М. В. Ломоносова, Математическом институте РАН им. В. А. Стеклова, Тверском государственном университете, Петербургском отделении математического института РАН им. В. А. Стеклова, Институте математики им. С. Л. Соболева СО РАН, Институте проблем передачи информации РАН им. А. А. Харкевича.

Апробация работы I

Результаты диссертации докладывались в 2003-2010 гг.:

• на Международной конференции «Приложения модальной логики в информатике» (Москва, 2005);

• на Международной конференции «Advances in Modal Logic, 2008» (Нанси, Франция, 2008),

• на XXXI конференции молодых ученых (МГУ, 2009); Публикации

Результаты автора по теме диссертации опубликованы в 7 работах: [21], [20], [22], [18], [19], [23], [17]. Из них одна работа ([18]) опубликована в журнале из "Перечня ведущих рецензируемых научных журналов и изданий, в которых должны быть опубликованы основные научные результаты диссертаций на соискание ученой степени доктора и кандидата наук".

Краткое содержание диссертации

Фиксируем счетное множество пропозициональных переменных PV и некоторое множество индексов Е.

ОПРЕДЕЛЕНИЕ (1.1). Формулы языка Mis (модальные формулы) строятся рекурсивно с помощью переменных из PV, констант «ложь» (L), «истина» (Т), логических связок A, V, —>, -1 и двойственных друг к другу модальностей df и О^ для каждого £ G S.

ОПРЕДЕЛЕНИЕ (1.55). Формула называется позитивной, если она не содержит связок -1 и —» (но может содержать !). Формула называется негативной, если она есть отрицание позитивной.

ОПРЕДЕЛЕНИЕ (1.4). Шкалой Кринке для языка называется набор F =

IV, (Rç : £ G H)), где Rç С W х W для каждого £ G Е. Элементы множества W мы будем называть точками.

ОПРЕДЕЛЕНИЕ (1.5). Оценкой в шкале Кринке F = (W, (Rç : £ G E)) называется отображение в : PV —» 2W, которое каждой пропозициональной переменной ставит в соответствие множество точек шкалы Крипке.

ОПРЕДЕЛЕНИЕ (1.6). Моделью Крипке, построенной на шкале F, называется пара M — (F, 9), где 0 — оценка в шкале F.

ОПРЕДЕЛЕНИЕ (1.7). Истинность формулы в точке модели M = (F, в) определяется стандартным образом:

• в точке х переменная р G PV истинна, если х G в(р);

• значения булевых связок вычисляются в точке по классическим таблицам истинности;

• в точке х истинна формула О^ф, если найдется такая точка у £ в которой верна формула ф\

Запись F, w, в \= ф означает, что формула ф истинна в точке w модели М = (F, в). определение (1.14). Запись F, w f= ф означает, что формула ф истинна в точке w любой модели М, построенной на шкале F. определение (1.15). Формула ф общезначима на шкале F, если она истинна во всех точках любой модели М, построенной на шкале F.

Шкалу Крипке F = (W, (Я^ : £ € Е)) можно рассматривать как обычную модель для языка первого порядка С,содержащего равенство, бинарные предикатные символы В$ для каждого £ е Е, предметные переменные и кванторы. определение (1.18). Первопорядковая формула А{х) языка £/= с одной свободной переменной х соответствует модальной формуле ф языка М.1-=, если в любой шкале Крипке F для любой ее точки w

F, w (= ф в шкале F верна формула A(w). определение (1.19). Первопорядковая формула А(х) языка £/н с одной свободной переменной х называется модально определимой, если она соответствует некоторой модальной формуле ф. определение (1.22). Первопорядковая формула А(х\,., хп) языка £/ со свободными переменными ., хп называется модально определимой, если существует такая последовательность модальных формул ф\,., фп, что в любой шкале Крипке F для любых ее точек wi,. ,wn для любой оценки в для некоторого г (1 < г < n) F, wt, в [= фг <£=>■ в шкале F верна формула A[w\,., wn]. определение (1.20). Модальная формула называется (локально) элементарной, если она соответствует некоторой формуле первого порядка языка Cf3.

ОПРЕДЕЛЕНИЕ (1.38). Обобщенной шкалой Крипке для языка М.1^ называется набор ^ - (\¥, : ( е Е), А), где Щ С V/ х IV для всех ^ £ Б, А С 2Ц/, и А замкнуто относительно булевых операций и операции У —»

ОПРЕДЕЛЕНИЕ (1.39). Пусть ^ = (1У, (Я^ : £ £ 5), Л) — обобщенная шкала Крипке. Оценка в : РУ —> 2У/ называется допустимой для если она принимает значения в А.

Истинность формулы в обобщенной шкале определяется так же, как и в шкале Крипке.

ОПРЕДЕЛЕНИЕ (1-41). Модальная формула общезначима в обобщенной шкале Р, если она верна во всех точках шкалы при любой допустимой для Р оценке.

Положим для V С Ж /?°(У) = {х | ^(х) С V}. ОПРЕДЕЛЕНИЕ (1.42). Обобщенная шкала Крипке Р = называется

• различимой, если для любых различны х, у из IV найдется такое У £ А, что х £ V и у <£У.

• тугой, если

П^ е л I ЯеИ ^ £

• компактной, если любое центрированное семейство (т. е. семейство, пересечение любого конечного множества элементов которого не пусто) Ы С А имеет непустое пересечение.

• дескриптинной, если Р различима, туга и компактна.

ОПРЕДЕЛЕНИЕ (1.43). Модальная формула ф называется (1-упорной, если для любой дескриптивной обобщенной шкалы Р = (\У, {Щ : £ € Н),.А) из общезначимости ф на Р, следует ее общезначимость и на соответствующей обычной шкале Крипке

Вторая глава посвящена обобщенным формулам Салквиста и их первопорядко-вым аналогам — обобщенным формулам Крахта.

Будем считать, что множество переменных РУ разбито на счетное множество групп р°, Рз) Рз) • • •> р\) Рз> • • ■> Р\ > р!) Vз,. и т. д. Верхний индекс (называемый рангом) означает номер группы, а нижний — номер переменной в пределах группы.

ОПРЕДЕЛЕНИЕ (2.2). Регулярная П-формуларанга к определяется по индукции. Именно,

• любая переменная $ ранга к является П-формулой ранга к,

• если РОБ — позитивная модальная формула, зависящая только от переменных, ранг которых меньше к и ф — регулярная П-формула ранга к, то РОБ —> ф — регулярная п-формула ранга к.

• если ф —регулярная П-формула ранга к, то — тоже регулярная П-формула ранга к.

ОПРЕДЕЛЕНИЕ (2.29). Обобщенной импликацией Салквиста называется формула вида СБА —> ±, где СБА построена из регулярных П-формул и негативных формул при помощи А, V, О^.

ОПРЕДЕЛЕНИЕ (2.30). Обобщенной формулой Салквиста называется модальная формула, построенная из обобщенных импликаций Салквиста при помощи А, П^, а так же V, применяемой к формулам без общих пропозициональных переменных.

ТЕОРЕМА (2.32, Обобщенная теорема Салквиста). Каждая обобщенная формула Салквиста элементарна и ¿-упорна.

ОПРЕДЕЛЕНИЕ. Модальная логика А называется полной, если любая совместная с пей формула (т. е. такая формула ф, что ф —» 1 ^ А) выполнима на некоторой шкале Крипке, на которой А общезначима.

СЛЕДСТВИЕ. Логика, аксиоматизируемая обобщенными формулами Салквиста, полна.

ОПРЕДЕЛЕНИЕ. Ь-термом называется терм в языке, алфавит которого состоит из символов {:Ег}, П, и, Я^1, Я°, Щ, Т, !. Здесь 1, Т — константы, {х{} — переменные, Я"1, Я°, Я$ — одноместные функциональные символы, П, и — бинарные функциональные символы.

ОПРЕДЕЛЕНИЕ (2.19). Назовем Ь-терм ,ч полубезопасным, если верно одно из следующих условий:

1) з = {а*};

2) в — Я^(й'), где з' полубезопасен;

3) 4)

Рис. 1: Примеры диаграмм ТЕОРЕМА (2.52, Обобщенная теорема Крахта).

• Каждая обобщенная формула Салквиста соответствует некоторой обобщенной формуле Крахта.

• Каждая обобщенная формула Крахта соответствует некоторой обобщенной формуле Салквиста.

Естественный вопрос: а будет ли семантически класс обобщенных формул Крахта шире класса стандартных формул Крахта? Ответ на этот вопрос дает следующая

ТЕОРЕМА (2.66). Обобщенная формула Крахта с = Ух1 >1 хУх2 >2 1>з хЗу' >1 хЗу" >2 у'Зу >3 у" у <= Я3(Я2(Х1) П Яг(х2)) Л у е Я2(Яз(х!) П ЯгЫ) А А у е Яг(Я2(хг) П Я3{х2)) ), выражающее "свойство куба" трехмерного произведения шкал Крипке, не эквивалентна никакой стандартной формуле Крахта.

Третья глава посвящена формулам первого порядка с одной свободной переменной, которые можно проиллюстрировать специальным чертежом — диаграммой.

На Рис. 1 приведены простейшие примеры таких диаграмм: (условия станут более привычными,, если их мысленно дополнить квантором всеобщности по х)

1) транзитивность: УуУг(хЯу А уЯг —>• хЯл).

2) плотность: Уг{хЯг —> 3у(хЯу А уЯг)).

3) полукоммутативность: \/у(хЯ2Ягу хЯ.\ Я2у).

4) свойство Черча-Россера: ЧуУг(хЯгу А хЯ2г —> Зу(уЯ^ А гЯ\ю)).

3) 5 = в' П в", где либо з', либо в" полубезопасен.

Терм £ называется безопасным, если он полу безопасен, и в каждом его подтерме вида Щ(з) терм й нолубезопасен.

ОПРЕДЕЛЕНИЕ. Ограниченными кванторами называются конструкции х^) и (зхг >? ху), где

Ухг := \/Xi(xjЩxi —»■ а);

За^ Ху)а := Зх{(х3-Я(хг А а).

Рассмотрим язык первого порядка 7^/н, содержащий предметные переменные а^, логические связки А и V, ограниченные кванторы и по (п-Ы)-местному предикатному символу \у £ Е для каждого безопасного терма Е, содержащего п различных х^.

Ясно, что любую такую формулу можно перевести на классический язык первого порядка, заменив предикатный символ у £ Е на его перевод Е*(ь), где ж* }*(» := (и = Хг);

Т» := Т;

Ег и Е2)*{у) := Е{{у) V Е*(у);

Щ\Е)У(у) := Зу(уВ,£у Л Е*(у)[у/у])-,

Е)Г(у) := Му{уЩу Я*(т;)[у/1;]);

Яс(£))>) := А Е*(у)[у/у}).

В последних трех случаях у должна быть некоторой новой переменной, не встречающейся в формуле Е*{у).

ОПРЕДЕЛЕНИЕ (2.49, 2.50). Формула А(х0) в этом языке называется обобщенной формулой Крахта, если она содержит ровно одну свободную переменную Хо и построена из формул вида у £ Е при помощи конъюнкции, дизъюнкции и ограниченных кванторов, причем для каждой подформулы вида у £ Е , входящей в А(хо), все переменные хг, входящие в Е, квази-свободны, то есть связаны ограниченным квантором всеобщности, который не находится под действием никакого ограниченного квантора существования.

5) сериальность: 3у хЯу.

6) симметричность: Уу(хЯу —>■ уЯх).

Сперва мы рассматриваем так называемые экзистенциальные диаграммы, которые получаются из приведенных рисунков удалением сплошных стрелок.

ОПРЕДЕЛЕНИЕ (3.1). Экзистенциальной диаграммой называется набор С = {У/, \¥Ч,\¥В)Т11,.) ПД где\¥ = \¥чи\УБ,\¥чП\Ув = $иТ1гС\¥х УУ.

Положим \¥ч = ., хп}, \УВ = (т/1,., Ут}. Точки множества будем называть черными, а точки множества \УВ — белыми. Каждой тот1ке г Е Ш поставим в соответствие предметную переменную уг.

Каждой экзистенциальной диаграмме С поставим в соответствие формулу Кс в языке первого порядка с з бинарными предикатами Я],., Я3 и п + т свободными переменными уХ1,., ьХл, иУ1,., иУт

-с

А Д и формулу

Ес в том же языке первого порядка с п свободными переменными

Ес = Зуш.ЗуутКс.

ОПРЕДЕЛЕНИЕ. Экзистенциальная диаграмма С называется определимой, если первопорядковая формула Ес(иХ1,. ,уХп) модально определима.

Наша цель — получить критерий определимости для диаграмм.

ОПРЕДЕЛЕНИЕ (3.7). Пусть ., ьп) и В{ьъ .,уп)— две формулы языка £/ с одними и теми же свободными переменными. Мы говорим, что из формулы А следует формула В (обозначаем А \= В), если в любой модели Р = (И7, Яг,., Я3) для любого набора точек ., € из того, что Р \= А(г>°,. г>°) следует, что

ОПРЕДЕЛЕНИЕ (3.8). Экзистенциальная диаграмма С называется минимальной, если для любой диаграммы С, которая получается из диаграммы С удалением какой-нибудь стрелки, из формулы Ес' не следует формула Ес.

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

ОПРЕДЕЛЕНИЕ. Направленным путем в экзистенциальной диаграмме С, соединяющим точку х с точкой у, называется такая последовательность ос^а^ . £/га;/1+1, где для всех г от 1 до /г. а* е IV, & £ {1,., в} и (а*, аг+1) е П^, и, к тому же, а.\ = х и ан = у.

Ненаправленный путь отличается от направленного тем, что условие {щ, £ П^ заменяется на (о^о^!) £ П^ иП^1.

ОПРЕДЕЛЕНИЕ (3.5). Экзистенциальная диаграмма называется достижимой, если для любой белой точки у найдется черная точка х, такая что существует направленный путь, соединяющий точки х и у, все точки которого, кроме х, белые.

ОПРЕДЕЛЕНИЕ (3.11). Экзистенциальная диаграмма называется связной, если любые две белые точки можно соединить ненаправленным путем, все точки которого белые.

ОПРЕДЕЛЕНИЕ (3.13). Пусть С = {XV, П1;., Пв) - экзистенциальная диаграмма. Мы говорим, что она содержит петлю, если для некоторых х е и £ € {1,.,з} (х, х) е П^. Мы говорим, что она содержит кратное ребро, если для некоторых £ {!,•■•, ¿'Ь £1 Ф £2 х И^) ПП^ ПП^2 ф 0, или же для некоторых, возможно равных, £1,^2 £ {1,.,з}, найдутся точки х,у 6 такие что хИ^у и уП.£2х. Мы говорим, что диаграмма содержит внутренний цикл, если она либо содержит петлю, либо кратное ребро, либо ненаправленный путь а^а^г ■ • • Ь^н+х (к > 3), где все щ е И^, у которого все вершины белые, и все вершины которого, кроме первой и последней, попарно различны, а первая и последняя совпадают.

ТЕОРЕМА (3.15). Если достижимая минимальная экзистенциальная диаграмма содержит внутренний цикл, то она модально неопределима.

ТЕОРЕМА (3.16). Если достижимая связная экзистенциальная диаграмма не содержит внутренних циклов, то она модально определима.

СЛЕДСТВИЕ (Критерий определимости). Достижимая связная минимальная диаграмма модально определима тогда и только тогда, когда она не содержит внутренних циклов.

СЛЕДСТВИЕ (3.17). Если достижимая экзистенциальная диаграмма С не содержит внутренних циклов, то задаваемая ей первопорядковая формула Е°(уХ1,., иХп ) представляет собой конъюнкцию определимых первопорядковых формул.

Затем мы переходим к изучению диаграмм со сплошными стрелками.

ОПРЕДЕЛЕНИЕ. 2.33 Пусть дан набор Т = (Ж, ., Дв), где все Щ С IV х IV. Два направленных пути х^, £1, х2, • • ■ хп и у\, //1, У2, /¿2, ■ ■ ■ ут мы считаем равными, если т = п, Хг = у1 для всех 1<г<пи& = /х* для всех 1 < г < п — 1. Набор Т = (Т, г) называется деревом с корнем г, если

• г е IV,

• Щг(г) = 0 для всех ^еН,

• для любой точки х, отличной от корня, существует единственный путь, соединяющий тех.

ОПРЕДЕЛЕНИЕ (3.29). УЗ-диаграммой будем называть набор О = (IV, Вг,., В3, П1;., П3, г), где ]¥ — конечное множество, IV = У/ч и \¥в, ч П = 0, £?!,., Д, — бинарные отношения на \¥ч, П1,.,П5 — бинарные отношения на \¥ и г £ \УЧ, причем структура (1УЧ, В\,. ,В5,г) представляет собой дерево с корнем г. Элементы множеств Bj и П^ будем называть соответственно черными и белыми стрелками.

ОПРЕДЕЛЕНИЕ (3.30). Экзистенциальной частью УЗ-диаграммы В ~ \¥ч, \¥в, В\,., В8, Пх,., П8, г) будем называть экзистенциальную диаграмму С={Ш,\¥Ч,\УЪ, ПЬ.,П3).

Как и для экзистенциальных диаграмм, положим \¥ч = {хо,Х1,. ,хп}, ]¥в = {у\,., угп}, причем будем считать, что х0 = г, и каждой точке 2: £ IV поставим в соответствие предметную переменную

Каждой УЗ-диаграмме Б поставим в соответствие первопорядковую формулу Е0 с одной свободной переменной ьхо в сигнатуре с я бинарными предикатными символами Д1,., Я.а:

ОПРЕДЕЛЕНИЕ (3.32). УЗ-диаграмма £> = (Ш, \¥ч, 1УГ„ Въ ., Ва, Пь ., Па,г) называется минимальной (достижимой, содержащей внутренний цикл), если ее экзистенциальная часть обладает соответствующим свойством.

ОПРЕДЕЛЕНИЕ (3.31). УЗ-диаграмма И = Вг,., Ва, Пг,., Пя, г) называется модально определимой, если формула Ер модально определима.

ТЕОРЕМА (3.33). Если достижимая УЗ-диаграмма О не содержит внутренних циклов, то она модально определима.

В Приложении 1 мы приводим критерий модальной определимости для некоторого класса УЗ-диаграмм.

Для работы с двумерными произведениями с выделенной диагональю используется язык Его алфавит получается из бимодального языка Л41{ь,у} добавлением пропозициональной константы 3.

Шкалой Крипке (для языка Л41$) будем называть набор Е = (У/, Лу, Д), где И^ С IV х № (£ Е {/>,, г?}), Д С IV. Моделью Крипке называется пара М = (/% в), где Р — шкала Крипке, а в — оценка в шкале Е.

Определение истинности формулы в модели Крипке получается из стандартного определения добавлением пункта

• формула 8 истинна в точности в точках множества Д. где а С — экзистенциальная часть П.

На этот язык очевидным образом переносится понятие общезначимости формулы и модальной логики класса шкал.

ОПРЕДЕЛЕНИЕ (4.6). Множество формул Е аксиоматизирует логику L, если L является минимальным множеством формул, содержащим все пропозициональные тавтологии, формулы Kh, Kv, где

К£ = □ g(p q) -> (П5р ->• D^), множество формул Е, и замкнутое относительно правил вывода Modus Ponens, правила подстановки и правила обобщения:

А,А^В А А

В, [В/р]А, DiA.

ОПРЕДЕЛЕНИЕ (4.7). Логика L аксиоматизируема формулами с конечным числом переменных, если существует такое множество модальных формул Е, что оно аксиоматизирует логику L, и в формулы Е входит лишь конечное число переменных.

ОПРЕДЕЛЕНИЕ (4.1). Пусть F = (W, R) - 1-шкала Кринке. Через F| обозначим шкалу (W х W, Rh, Ry, А), где а, b)Rh(c, d) -Ф=Ф- aR,c и b = d\ а, Ь)Л„(с, d) а — с и bRd, А = {(а, а) | а е W}. Такую шкалу мы будем называть 5-квадратом шкалы F.

ОПРЕДЕЛЕНИЕ (4.2). Пусть С — класс 1-шкал Крипке. Положим

Cf = № \FtC}.

ОПРЕДЕЛЕНИЕ (4.4). Пусть L — полная по Крипке 1-модальная логика. 5-квадратом логики L (обозначается Щ) называется множество формул Log (C(ij)f), где C(L) — класс всех 1-шкал Крипке, на которых общезначима логика L.

Чтобы точно сформулировать результат о неаксиоматизируемости формулами с конечным числом переменных, рассмотрим следующие шкалы Крипке (см. Рис. 2). щ Щ

Рис. 2: Шкалы Щ и

Формально, = Н„), где {0,1,., п, 1,., гг, с},

К = {(М I 1 < г < га} и {(г, Л I 1 < ^ 7 < га} и {(г, с) | 1 < г < гг}, = где = {г, 1,. .п}, ^ = {(г,г) | 1 < г < гг}.

ТЕОРЕМА (4.9). Пусть Ь — полная по Крипке 1-модальная логика, и С(Ь) содержит все шкалы вида И''] и Отп или все их рефлексивные замыкания, или все их транзитивные замыкания, или все их рефлексивные транзитивные замыкания. Тогда не аксиоматизируема формулами с конечным числом переменных.

СЛЕДСТВИЕ (4.10). Дельта-квадраты любой полной по Крипке логики Ь, такой что К С Ь С СЬ или К С Ь С вгг, не аксиоматизируемы формулами с конечным числом переменных.

Список источников диссертации и автореферата по математике, кандидата физико-математических наук, Кикоть, Станислав Павлович, Москва

1. P. Balbiani, 1. Shapirovsky, and V. Shehtman. Every world can see a Sahlqvist world. In Governatori et al. 13], pages 69-85.

2. P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. Cambridge University Press, 2002.

3. A. Chagrov and L. Chagrova. The truth about algorithmic problems in correspondence theory. In Governatori et al. 13], pages 121-138.

4. A. Chagrov and M. Zakharyaschev. Modal Logic. Oxford University Press, 1997.

5. W. Conradie, V. Goranko, and D. Vakarelov. Algorithmic correspondence and completeness in modal logic. The core algorithm SQEMA. Logical Methods in Computer Science, 2(1), 2006.

6. D. Gabbay, A. Kurucz, F. Wolter, and M. Zakharyaschev. Many-dimensional modal logics: theory and applications. Studies in Logic and the Foundations of Mathematics, 148. Elsevier, 2003.

7. D. Gabbay and V. Shehtman. Products of modal logics, part 1. Journal of the IGPL, 6:73-296, 1998.

8. D. Gabbay, V. Shehtman, and D. Skvortsov. Quantification in Nonclassical Logic. Studies in Logic and the Foundations of Mathematics, 153. Elsevier, 2009.

9. R. Goldblatt and S. Thomason. Axiomatic classes in propositional modal logic. In Algebra and Logic, Lecture Notes in Math., Vol. 450, pages 163-173. Springer, Berlin, 1974.

10. V. Goranko and D. Vakarelov. Sahlqvist formulas unleashed in polyadic modal languages. In Advances in Modal Logic 3, pages 221-240. King's College Publications, 2000.

11. V. Goranko and D. Vakarelov. Elementary canonical formulae: extending Sahlqvist's theorem. Annals of Pure and Applied Logic, 141(1-2):180-217, 2006.

12. G. Governatori, I. Hodkinson, and Y. Venema, editors. Advances in Modal Logic 6, papers from the sixth conference on "Advances in Modal Logic," held in Noosa, Queensland, Australia, on 25-28 September 2006. King's College Publications, 2006.

13. L. Henkin, J. Monk, and A. Tarski. Cylindric algebras, part I. North-Holland, 1971.

14. I. Hodkinson. Hybrid formulas and elementarily generated modal logics. Notre Dame Journal of Formal Logic, 47(4):443-478, 2006.

15. JI. JI. Максимова, Д. П. Скворцов, и В. Б. Шехтман. Невозможность конечной аксиоматизации логики финитных задач Медведева. Доклады АН СССР, 245(5): 1051-1054, 1979.

16. С. Кикоть. Об аксиоматике модальных логик квадратов шкал Крипке с выделенной диагональю. В Тезисы докладов секции "Математика и механика" Международной конференции студентов, аспирантов и молодых ученых "Ломоносов-2009", pages 33-34, 2009.

17. С. Кикоть. О квадратах модальных логик с выделенной диагональю. Математические заметки, 88(2):261-274, 2010.

18. С. Кикоть. О модальной определимости некоторых формул первого порядка. Рукопись депонирована в ВИНИТИ 29.04.2010, №234-В2010, Указатель №6, 2010.

19. S. Kikot. Formulas, corresponding to diagrams. In International Conference "Computer science applications of modal logic". Abstracts, pages 18-19. Independent University of Moscow, 2005.

20. S. Kikot. A new generalization of Sahlqvist theorem. In Algebraic and Topological Methods in Non-classical Logics II, Abstracts, Universitat de Barcelona, pages 40-41, Barcelona, 2005.

21. S. Kikot. An extension of Kracht's theorem to generalized Sahlqvist formulas. Journal of Applied Non-Classical Logic, 19/2:227-251, 2009.

22. S. Kikot. Semantic characterization of Kracht's formulas. In Advances in Modal Logic 8, pages 218-234, 2010.

23. M. Kracht. How completeness and correspondence theory got married. In M. de Rijke (Ed.), Diamonds and Defaults, pages 175-214. Synthese Library, Kluwer, 1993.

24. M. Kracht. Tools and Techniques in Modal Logic. Studies in Logic and the Foundations of Mathematics, 142. Elsevier, 1999.

25. S. Kripke. A completeness theorem in modal logic. Journal of Symbolic Logic, 24, No 1:1-14, 1959.

26. A. Kurucz. On axiomatising products of Kripke frames. Journal of Symbolic Logic, 65:923-945, 2000.

27. A. Kurucz. On axiomatising products of Kripke frames, part II. In C. Areces and R. Goldblatt, editors, Advances in Modal Logic 7, pages 219-230. King's College Publications, 2008.

28. H. Sahlqvist. Completeness and correspondence in the first and second order semantics for modal logic. In Proceedings of the Third Scandinavian Logic Symposium, Amsterdam, North-Holland, pages 110-143, 1975.

29. G. Sambin and V. Vaccaro. Topology and duality in modal logic. Annals of Pure and Applied Logic, 37:249-296, 1988.

30. G. Sambin and V. Vaccaro. A topological proof of Sahlqvist's theorem. Journal of Symbolic Logic, 54:992-999, 1989.

31. V. Shehtman. On some two-dimensional modal logics. In 8th International Congress on Logic, Methodology, and Philosophy of Science. Abstracts, volume 1, pages 326330. Moscow, 1987.

32. D. Vakarelov. Extended Sahlqvist formulae and solving equations in modal algebras. In 12-th International Congress of Logic Methodology and Philosophy of Science, August 7-13. Abstracts, page 33. Oviedo, Spain, 2003.

33. Y. Venema. Many-dimensional modal logic. PhD thesis, University of Amsterdam,

34. E. Zolin. Query answering based on modal correspondence theory. In Proceedings of the 4th "Methods for modalities" Workshop (M4M-4), pages 21-37, 2005.

35. В. Б. Шехтман. Двумерные модальные логики. Математические заметки, 23(5):759-773, 1978.

36. JI. Л. Эсакиа. Топологические модели Крипке. Доклады АН СССР, 214(2):298-301, 1974.1991.