Метод канонических формул и его применение в модальной логике

Модальная логика — одна из наиболее динамично развивающихся ветвей математической логики, нашедшая многочисленные приложения в основаниях математики, философии, информатике, лингвистике, искусственном интеллекте и других областях. Начавшись, казалось бы, с не очень-то обоснованных систем Льюиса [115, 116], которые вряд ли бы заметили в серьезных математических кругах, своим нынешним положением она обязана, прежде всего, двум открытиям.

Во-первых, прочитав льюисовский оператор? (некой абстрактной) необходимости как «доказуемо», Орлов [30]1 и Гедель [99] дали классическую интерпретацию интуиционистской пропозициональной логики Int посредством погружения ее в модальную систему «доказуемости», которая к тому же оказалась эквивалентной льюисовской S4. Это открытие, с одной стороны, стимулировало установление связи модальной и интуиционистской логик с топологией и алгеброй в виде построения Стоуном [147], а также Маккинси и Тарским [122, 123] топологической и алгебраической семантик для S4 и Int. А с другой стороны, оно продемонстрировало возможность использования модальной логики в основаниях математики для анализа феномена доказуемости в формальных системах, которая была успешно реализована в конце 70-х — начале 80-х Соловьем [143], Артемовым [1], Булосом [66] и др. Сегодня — это одно из самых плодотворных и впечатляющих приложений модальной логики. «Если исследования в области модальной логики или семантические понятия, развитые для ее изучения, и нуждались когда-либо в научном обосновании, теорема Соловья и ее доказательство их предоставляют,» —.

ХК сожалению, эта работа Орлова, опубликованная за 5 лет до заметки Геделя [99], оставалась незамеченной вплоть до 80-х годов. писал Булос [68].

Вторым крупным открытием, привлекшим широкое внимание к модальной логике, явилось найденное Йонссоном и Тарским [106] представление топологических булевых и других «модальных» алгебр в виде реляционных структур или шкал, как они теперь называются, и использование этих структур для построения семантики «возможных миров» в работах Кангера [107], Хинтикки [104] и Крипке [111], формализовавшей старинную идею Лейбница о необходимости как истинности во всех возможных мирах. Это открытие дало импульс построению «трех столпов ., на которых покоится все здание модальной логики —. всепроникающей теории полноты,. теории соответствия или определимости и. теории двойственности между шкалами Крипке и модальными алгебрами» (ван Бентем [154]).

С другой стороны, возможность интерпретирования шкал как временных потоков, процессов вычислений или, скажем, процессов развития знаний познающих субъектов привела к разнообразным применениям модальной логики в теоретическом и практическом программировании, искусственном интеллекте, философии, лингвистике и ряде других областей. «Этот подход имел огромное влияние не только на логику необходимости и возможности, но также и на другие области. В частности, его идеи были использованы с целью разработки формализмов для описания многих других видов структур и процессов в информатике, давших предмету (модальной логике — М.З.) приложения, которые, вероятно, удивили бы как самих его создателей, так и их клеветников» , — пишут Барвайс и Мосс [59].

Одним из результатов вызванного этими открытиями ускоренного развития модальной логики вглубь и вширь явилось создание колоссального числа всевозможных систем как естественного, так и искусственного происхождения.2 Это, в свою очередь, не могло не привести к разнообразным обобщениям. На рубеже 60-х и 70-х годов завершилось формирование абстрактного понятия (или, скорее, понятий) модальной логики.

2Интересно, что одна из самых знаменитых систем модальной логики — логика доказуемости Геделя-Леба СЬ — была введена сначала Сегербергом [138] как «искусственная» система под именем К4Л?. и была явно поставлена задача разработки соответствующей общей теории. «Последние работы по модальной логике,» — писал Файн [90], — «содержат два больших пробела: нам недостает общих результатов и результатов отрицательного характера. Обычно показывается, что та или иная логика обладает таким-то и таким-то свойством, однако очень мало известно о протяженности и границах этого свойства. Таким образом, имеются многочисленные результаты о полноте, разрешимости, финитной аппроксимируемости, компактности и т. д., но очень мало общих или отрицательных результатов.» Систематические исследования близкого к модальным логикам класса расширений интуиционистского исчисления высказываний были инициированы еще раньше А. В. Кузнецовым, Т. Хосои и X. Оно.

Предмет и задачи модальной логики стали меняться. Ряд конкретных модальных систем дали начало более специальным дисциплинам, таким как логика доказуемости, временная, деонтическая, динамическая, квантовая, эпистемическая и т. п. логики. Общая же (или, по аналогии с алгеброй, универсальная) модальная логика сконцентрировалась на изучении больших семейств модальных систем. Ее главной целью стала разработка методов, пригодных для работы с логиками en masse. Создание теории двойственности между реляционной и алгебраической семантиками Ионссоном и Тар-ским [106], Леммоном [114], Эсакиа [51] и Гольдблатом [100], установление связи между модальными (и суперинтуиционистскими) логиками и многообразиями модальных (и псевдобулевых) алгебр Кузнецовым [17], Максимовой и Рыбаковым [28] и Блоком [62], а также между пропозициональным модальным языком и языком логики предикатов первого или более высокого порядка Файном [91] и ван Бентемом [153] снабдили модальную логику теми математическими орудиями, которые были необходимы для выделения ее в самостоятельную и полноценную ветвь математической логики.

Современная модальная логика в таком широком понимании базируется в основном на теоретико-модельном (или теоретико-шкальном) и алгебраическом подходах. (Теория доказательств развита лишь для нескольких отдельных систем, и совсем не понятно, возможны ли здесь далеко идущие обобщения.) Связь между синтаксическими представлениями логик и их семантикой осуществляется общей теорией полноты, берущей начало с работ Була [70], Файна [90], Салквиста [136], Гольдблата и Томасо-на [101]. Теоремы полноты обычно являются первым шагом в изучении разнообразных свойств логик, особенно если эти свойства имеют алгебраические или семантические эквиваленты. Классические примеры — исследование Максимовой [26] интерполяционного свойства нормальных модальных логик, содержащих S4, или результаты о разрешимости, основанные на полноте относительно «хороших» (скажем, конечных) шкал. Теория полноты предоставляет также средства для аксиоматизации логик, задаваемых классами шкал, и дает критерии аксиоматизируемости таких классов.

Стандартные семейства модальных логик обычно образуют решеточные структуры относительно теоретико-множественного включения. Это наблюдение дает начало исследованиям строения решеток логик, поднимающим вопросы об их коатомах (т.е. максимальных непротиворечивых логиках данного семейства), наличии бесконечно возрастающих цепей (т.е. существовании логик, не имеющих конечной аксиоматизации) и т. д. С алгебраической точки зрения решетка логик соответствует решетке подмногообразий некоторого фиксированного многообразия модальных алгебр, что открывает возможность использования методов и результатов хорошо разработанной области универсальной алгебры. Удивительные связи между «геометрическими» свойствами модальных формул, полнотой, аксиоматизируемостью и неразложимыми элементами решетки модальных логик были обнаружены Янковым [54, 55], Блоком [63, 64] и Раутенбергом [133].

Еще одним важным направлением современных исследований, возникающим только тогда, когда мы имеем дело с классами логик, является решение алгоритмической проблемы распознавания свойств (конечно аксиоматизируемых) логик. Существование неразрешимых исчислений (построенных Томасоном [150] и Шехтманом [46]), казалось бы, по аналогии с теоремой Райса-Успенского должно вести к неразрешимости нетривиальных свойств логик. Однако эта аналогия здесь не срабатывает. В решетке нормальных расширений S4 разрешимыми оказываются, например, табличность и интерполяционное свойство Крейга, как было доказано Максимовой [24, 26]. Но большинство интересных свойств все же неразрешимы. Техника получения такого рода отрицательных результатов разработана Томасоном [151] и Чагровым [40, 76].

Томасон [151] доказал неразрешимость полноты по Крипке сначала в классе всех полимодальных логик, а затем перенес этот результат на унимодальные логики путем погружения первых во вторые. Теория погружения и переноса вообще становится довольно мощным техническим средством в модальной логике, позволяя в ряде случаев сводить исследование новых типов логик к уже хорошо изученным. Пожалуй, наиболее известным примером такого рода сведения является погружение Орлова-Геделя интуиционистской логики и ее расширений в расширения Б4, применявшееся Дамметом и Леммоном [83], Максимовой и Рыбаковым [28], Блоком [62] и Эсакиа [53], а также его обобщения на некоторые модальные логики с интуиционистской базой, построенные Фишер Серви [93] и Шехтманом [48]. Другой впечатляющий пример — недавние результаты Крахта и Вольтера [110] о сохранении свойств унимодальных логик при их независимом объединении в полимодальные.

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

Как уже отмечалось выше, уровень наших знаний о модальных логиках в значительной мере определяется имеющейся информацией об устройстве их шкал (или алгебр). Изучая некоторую решетку логик С и желая иметь в каком-то смысле универсальное средство для работы с ними, мы заинтересованы в нахождении единого описания (т.е. в одном и том же языке и с использованием одних и тех же понятий) «геометрии и топологии» их шкал. Если С — решетка расширений некой логики Ь0, а чаще всего это именно так, то перед нами встает фундаментальная проблема харак-теризации класса всех тех шкал для Ьо, в которых общезначима (или опровергается) произвольно заданная модальная формула.

Целью диссертационной работы является: • решение проблемы характеризации для модальных формул в классе транзитивных шкал с действительными мирами, т. е. для решетки Ех1-К4 квазинормальных расширений базисной системы К4;

• разработка (на основе построенного в результате теоретико-модельного языка) методов доказательства разрешимости, финитной аппроксимируемости, сильной полноты, элементарности и других важных свойств логик из Ех<-К4;

• исследование подрешетки логик, которые характеризуются классами шкал, замкнутыми относительно взятия (конфинальных) подшкал;

• развитие теории погружений суперинтуиционистских логик в расширения Б4, а также модальных логик на интуиционистской базе в классические полимодальные логики, и применение полученных теорем сохранения для изучения свойств этих логик.

Следует отметить, что проблема характеризации в столь общей формулировке явно никогда не ставилась и не решалась. Причина, по всей видимости, заключалась в отсутствии подходящего универсального языка для описания «геометрических и топологических» свойств шкал. Традиционный первопорядковый подход достиг своего апогея в теореме Салквиста [136], давшей алгоритм построения формул первого порядка с равенством и предикатом достижимости, характеризующих строение шкал Крипке для большого, но все-таки ограниченного класса модальных формул. Многие важные пропозициональные модальные и интуиционистские формулы (например, аксиомы Лёба, Гжегорчика, Скотта) вообще не имеют первопорядковых эквивалентов на шкалах, не говоря уже о том, что ввиду существования неполных по Крипке логик (см. [89, 45]) требуется описывать обобщенные шкалы, а не только шкалы Крипке. Одним из наиболее важных результатов данной работы является разработка универсального теоретико-модельного языка, достаточного для характеризации (обобщенных) транзитивных шкал, опровергающих данную формулу в данной точке, а также создание его синтаксического аналога — языка канонических формул (см. параграфы 2.1 — 2.3).

Грубо говоря, каждая модальная каноническая формула S, L) строится по конечной корневой шкале J = (W, R) и некоторому множеству D ее антицепей, называемых закрытыми областями, так чтобы шкала <3 опровергала Э, L) в том и только том случае, когда существует подредукция3 (или частичный р-морфизм) / из © на 3 которая является конфиналъной в том смысле, что каждая точка, достижимая (по R) из области определения dorn/ подредукции /, либо «видит» dorn/, либо сама принадлежит dorn/, — символически dom/t С dom/J, — и удовлетворяет условию закрытых областей.

CDC) ->3х G dom/t-dom/ 3t> е ® /(st) = *>t т. е. никакая точка из dom/f—dorn/ не может «видеть» только прообразы всех точек из какой-либо закрытой области, их последователей и ничего больше).

Канонические формулы содержат явную информацию об устройстве своих опровергающих шкал — а стало быть, и об устройстве шкал аксиоматизируемых этими формулами логик — в теоретико-модельных терминах подшкал, редукций, условия конфинальности и (CDC) (ср., к примеру, стандартное и «каноническое» представления известной логики Маккинси.

S4.1 = S4 ф ПОр ОПр = S4 е а ((оо), 0, ±), где (оо) — двухэлементный сгусток). А с другой стороны, в параграфе 2.3 доказана теорема аксиоматической полноты, согласно которой каждая модальная формула может быть эффективно представлена в виде дедуктивно эквивалентного ей (т.е. аксиоматизирующего то же самое расширение К4) конечного множества канонических формул.

Аналогичный результат установлен и для интуиционистского случаяинтуиционистские канонические формулы обозначаются посредством ?>,!). Канонические представления многих стандартных модальных и суперинтуиционистских логик можно найти в таблицах на стр. 94 и 97. Таким образом,.

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

Частными случаями канонических формул являются хорошо известные интуиционистские характеристические формулы Янкова [54, 55] и модальные шкальные формулы (frame formulas) Файна [88]- они дедуктивно эквивалентны формулам вида /З^,®-", L) и «(З, ?)», L), соответственно, где ?>" — множество всех антицепей в Другой частный случай — подшкальные (subframe) формулы Файна [92], аксиоматизирующие в точности те нормальные расширения К4, которые характеризуются классами шкал, замкнутыми относительно образования подшкал. Однако множества формул Янкова и Файна аксиоматически полными не являются.

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

Традиционный метод доказательства разрешимости в неклассической логике (см. [103]) — это установление финитной аппроксимируемости (т.е. полноты относительно множества конечных шкал) и конечной аксиоматизируемости. Мы начинаем исследовать эти свойства в параграфе 3.1, где доказано, что финитно аппроксимируемы все нормальные модальные логики, канонические аксиомы которых не содержат закрытых областей (т.е. имеют вид а (£, 0,±-)).

Это достаточное условие охватывает почти все стандартные модальные логики (см. таблицу на стр. 94), все расширения S4.3 (ср. [70, 86]), уже упоминавшиеся подшкальные логики Файна [92], все нормальные расширения 84 булевыми комбинациями модальностей (см. пример 3.1.17) и множество других интересных логик. Класс СБТ нормальных модальных логик с каноническими аксиомами вида «(5, 0, -1) вообще оказывается замечательным во многих отношениях. В параграфах 3.1 и 3.2 показано, что СБТ — полная подрешетка решетки ЫЕх<-К4 нормальных расширений К4, а класс БТ подшкальных логик — полная подрешетка СЭТ] построена континуальная антицепь подшкальных логик, что дает отрицательный ответ на известный вопрос о числе и разрешимости логик из БТ (см. [21, 92, 108]) — дана теоретико-модельная характеризация СБТ'. логика принадлежит СБТ тогда и только тогда, когда она характеризуется классом шкал, замкнутым относительно образования конфинальных подшкалвычислена верхняя (по порядку не уменьшаемая в общем случае) оценка — 22 г (¥-»)+1 — размера минимальной шкалы, отделяющей формулу (р ^ Ь от логики Ь? СБТ (здесь 1((р) — число подформул (р) — доказан критерий элементарности, каноничности и сильной полноты по Крип-ке логик из С8Т.А.

Эти результаты переносятся (с помощью доказываемых в работе теорем сохранения, которые мы обсудим чуть позже) на интуиционистский случай, где семейства СБТ и БТ допускают не только теоретико-модельную, но и чисто синтаксическую характери-зацию. А именно, показано, что суперинтуиционистская логика аксиоматизируема импликатив-ными формулами (или формулами, не содержащими дизъюнкции) тогда и только тогда, когда она характеризуется классом шкал, замкнутым относительно взятия подшкал (соответственно, конфинальных подшкал);

4Продолжая исследования в этом направлении, Вольтер [160] обобщил некоторые из упомянутых здесь результатов на класс минимальных временных расширений логик из СБТ. установлено, что число суперинтуиционистских логик с импликативными аксиомами континуально (см. [21]) — доказано, что все суперинтуиционистские логики с аксиомами без вхождений дизъюнкции каноничны, а стало быть, и сильно полны по Крипке.5.

В параграфе 3.4 мы выходим за пределы решетки CST и обнаруживаем множество на удивление простых (благодаря языку канонических формул) примеров логик, не являющихся финитно аппроксимируемыми. Из новых результатов здесь можно отметить следующие: построен пример финитно не аппроксимируемого расщепления (splitting) решеток NExtK4 и NExtK4.3, что дает отрицательный ответ на давно стоявший вопрос (финитно не аппроксимируемые объединения расщеплений были построены Янковым [54] и Крахтом [109]) — дан пример финитно не аппроксимируемой салквистовой логики, содержащей S4 (до этого подобный пример был известен только над Ксм. [105]).

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

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

5 Этот результат был независимо получен Шимурой [142], который также использовал метод канонических формул. доказана финитная аппроксимируемость всех нормальных расширений К 4 принципами редукции модальностей6- доказана финитная аппроксимируемость всех нормальных расширений Э4 конечным числом формул от одной переменной.

Можно ли обобщить первый из этих результатов на класс всех нормальных логик пока не известно. А вот второй результат оказывается принципиально не улучшаемым. Над К4 даже константные формулы могут аксиоматизировать финитно не аппроксимируемые логики, а над 84 имеется построенная Шехтманом [49] финитно не аппроксимируемая логика с бесконечным числом аксиом от одной переменной. В параграфе 3.6 показано, что имеется бесконечно возрастающая цепь логик из NExtS4 с аксиомами от одной переменной, что число таких логик — континуум, а стало быть, среди них существуют и неразрешимые.

Использование метода канонических формул позволяет достигнуть значительного прогресса в развитии методов доказательства разрешимости при отсутствии свойства финитной аппроксимируемости и даже полноты по Крипке. В модальной логике существовал лишь один (несинтаксический) способ получения такого рода результатов — основанный на теореме Рабина о дереве метод редукций, предложенный Габбаем [95] и примененный им для нескольких конкретных систем. В интуиционистском случае Соболеву [33] удалось воспользоваться некоторыми результатами теории автоматов для (довольно сложного) доказательства разрешимости конечно аксиоматизируемых тесных суперинтуиционистских логик конечной ширины. В основе методов, предложенных в данной работе, лежат теоремы о полноте относительно классов достаточно «хороших и прозрачных», хотя и бесконечных шкал, проверка общезначимости канонических формул в которых может быть выполнена за конечное время. Этим способом в параграфе 3.3.

6Принцип редукции модальностей — это формула вида Мр —> Ир, где М и N — цепочки (возможно пустые)? и О. доказана разрешимость всех конечно аксиоматизируемых квазинормальных расширений К 4 каноническими формулами без закрытых областей (эти логики, вообще говоря, не являются полными по Крипке), а в параграфе 3.7 установлена разрешимость всех конечно аксиоматизируемых нормальных модальных логик, содержащих К4.3, что является существенным усилением известной теоремы Була-Файна [70, 86]. 7.

Хотя модальные и суперинтуиционистские логики рассматриваются в работе параллельно, «настоящие» доказательства и построения проводятся лишь для модального случая. На суперинтуиционистские логики результаты, как правило, переносятся с помощью теории погружений, систематические исследования в которой были начаты Максимовой и Рыбаковым [28], Блоком [62] и Эсакиа [52, 53]. Метод канонических формул позволяет представить эту теорию в очень наглядной и компактной форме (см., например, теорему 2.6.6, описывающую множество нормальных модальных напарников из ЫЕх184 данной суперинтуиционистской логики), фактически превращая ее в мощный конвейер по переносу результатов с модального случая на интуиционистский и обратно. В параграфе 2.6 получено описание устройства шкал для наименьшего модального напарника данной суперинтуиционистской логикинайден алгоритм, строящий по конечной аксиоматизации логики из NExtS4 аксиоматизацию ее суперинтуиционистского фрагментаисследовано сохранение наиболее важных свойств логик при переходе от модальной логики к ее суперинтуиционистскому фрагменту и от суперинтуиционистской логики к ее наименьшему и наибольшему модальным напарникам;

7Развивая предложенную в диссертации технику, Вольтер [159] недавно обобщил этот результат на линейные временные логики. Упомянутый выше результат Соболева также легко получается этой техникой. в частности, доказано сохранение разрешимости при всех этих переходах, сохранение полноты по Крипке (а также сильной полноты и каноничности) при переходе к наименьшему напарнику, что дало решение высказанной в 1959 году гипотезе ДамметаЛеммона [83], несохранение независимой аксиоматизируемости при переходе к суперинтуиционистскому фрагментуэти и другие интересные результаты собраны в таблице 2.8 на стр. 114.

В отличие от нормального случая, где логика Гжегорчика Grz оказывается наибольшим напарником интуиционистской логики и где имеет место теорема Блока Эсакиа об изоморфизме, существуют, как показал Чагров [38], собственные квазинормальные расширения Grz, имеющие Int своим фрагментом. В параграфе 2.7 изучаются квазинормальные модальные логики, в которые Int погружается переводом Орлова-Геделя. В частности, с помощью метода канонических формул получено описание всех квазинормальных напарников Int из ExtS4- доказано, что среди них имеется наибольший, и изучены его основные свойства (так, он разрешим, финитно не аппроксимируем, обладает дизъюнктивным свойством и полон по Холдену) — показано, что в квазинормальном случае теорема Блока-Эсакиа места не имеет.

Значительное внимание в последнее время стали привлекать модальные логики не на классической, а на интуиционистской (или, более общо, суперинтуиционистской) базе. Такие логики возникают из разных источников и имеют разные области приложений. Среди них — философия (см. [132, 85, 157]), основания математики (см. [18, ИЗ]), информатика (см. [131, 146, 156]). Модальности добавляются к интуиционистской логике в рамках изучения «новых интуиционистских связок» ([2, 96, 56]) и для моделирования монадического фрагмента интуиционистской логики предикатов ([71, 128, 130]). Однако в отличие от классической модальной логики, интуиционистские модальные системы изучались до сих пор «по-штучно» с использованием их индивидуальных особенностей.

Причина, очевидно, заключалась в том, что интуиционистские логики даже с одним модальным оператором гораздо ближе к бимодальным, чем к унимодальным классическим логикам, и только несколько последних лет принесли достаточно общие результаты в полимодальной логике (см., например, [110, 158]).

В главе 4 данной работы закладывается фундамент общей теории интуиционистских модальных логик, вообще говоря, с несколькими модальными операторами. В центре разрабатываемого подхода лежит обобщение рассмотренной выше теории погружений на интуиционистский модальный случай и использование ее для переноса результатов с суперинтуиционистских и унимодальных классических логик на интуиционистские модальные логики. Более конкретно, в параграфе 4.1 развивается теория двойственности между интуиционистскими модальными алгебрами и шкалами, в параграфе 4.2 разрабатывается теория погруженийв частности, доказывается аналог теоремы Блока-Эсакиа, согласно которому решетка интуиционистских модальных логик изоморфна некоторому главному фильтру решетки классических полимодальных логик, а также несколько теорем сохранения и, наконец, в параграфе 4.3 устанавливается несколько общих результатов о финитной аппроксимируемости и разрешимости интуиционистских модальных логик.

Таковы основные результаты этой диссертации. Они опубликованы в работах [3], [5] - [11], [14] - [15], [61], [73] - [79], [148], [162] - [172]- большая их часть вошла в монографию [79].

По результатам диссертации делались доклады на Всесоюзных и Всероссийских конференциях по математической логике (Тбилиси, 1982, пленарный докладНовосибирск, 1984; Москва, 1986; Ленинград, 1988; Алма-Ата, 1990; Казань, 1992), на международной конференции FCT'87 (Казань, 1987), на X Всесоюзной конференции по логике, методологии и философии науки (Минск, 1990), на международной конференции по алгебре (Новосибирск, 1989), на логических коллоквиумах Европейской Ассоциации символической логики (Берлин, 1989; Вежпрем, 1992; Киль, 1993; Клермон-Ферран, 1994), на логической конференции в Болгарии (София, 1990), на 4-ой Азиатской логической конференции (Токио, 1990), на международной конференции в центре Банаха (Варшава, 1991, приглашённый доклад), на конференциях по математической логике в Японии (Ниигата, 1994; Сендай 1996; Каназава, 1996; Киото, 1997, все — приглашённые доклады), на Международном конгрессе по логике, методологии и философии науки (Флоренция, 1995), на международной конференции FOLLI (Чиба, 1996, приглашённый доклад), на конференции Ассоциации символической логики (Сан Диего, Калифорния, 1997). Приглашенные лекции были прочитаны в университетах Хиросимы (1990), Амстердама (1992, 1993, краткий курс о канонических формулах, 1997), Берлина (1992, 1994, 1995, 1997), Токио (1994), Милана (1996, краткий курс «Метод канонических формул»), Каназавы (1996), Нагойи (1997), Лейпцига (1997) и Аахена (1997). Результаты докладывались на научных семинарах Московского, Новосибирского, Иркутского и Киевского университетов.

1. с.н. артемов. Модальные логики доказуемости для расширений арифметики // Семиотика и информатика. 1978;1979. Т. 12. С. 43−46.

2. A.B. бессонов. Новые операции в интуиционистском исчислении // Математические заметки. 1977. Т. 22. С. 503−506.

3. Ф. вольтер, М. В. Захарьящев. Об отношении между интуиционистскими и классическими модальными логиками // Алгебра и логика. 1997. Т. 36. С. 121−155.

4. B.JI. гудовщиков, в.в. Рыбаков. Дизъюнктивное свойство в модальных логиках // Тезисы докладов и сообщений 8-й Всесоюзной конференции «Логика и методология науки». Вильнюс, 1982. С. 35−36.

5. М.В. захарьящев, С.В. попов. О сложности контрмоделей Крипке в интуиционистском исчислении высказаваний // 2-й Советско-финский коллоквиум по логике. М., ИФ АН СССР, 1979. С. 32−36.

6. М.В. захарьящев, С. В. Попов. О мощности контрмоделей интуиционистского исчисления. Препринт Ин. прикл. матем. им. М. В. Келдыша АН СССР. N 85. 1980 г.

7. М.В. захарьящев, A.B. Чагров. Неразрешимость дизъюнктивного свойства суперинтуиционистских исчислений. Препринт Ин. прикл. матем. им. М. В. Келдыша АН СССР. N 57. 1989 г.

8. М.В. захарьящев, A.B. Чагров. Неразрешимость свойства полноты по Холдену модальных исчислений. Препринт Ин. прикл. матем. им. М. В. Келдыша АН СССР. N 82. 1990 г.

9. Г. кейслер, Ч. Ч. Чэн. Теория моделей. М., Мир, 1977.

10. A.B. КУЗНЕЦОВ. Некоторые свойства структуры многообразий псевдобулевых алгебр // XI Всесоюзный алгебраический коллоквиум: резюме сообщений и докладов. Кишинёв, 1971. С. 255−256.

11. A.B. КУЗНЕЦОВ. Доказуемостно-интуиционистское пропозициональное исчисление // Доклады АН СССР. 1985. Т. 283. С. 27−30.

12. A.B. кузнецов, В. Я. Герчиу. О суперинтуиционистских логиках и финитной аппроксимируемости // Доклады АН СССР. 1970. Т. 195. С. 1029−1032.

13. A.B. Кузнецов, А.Ю. МуравицкиЙ. Доказуемость как модальность. // Актуальные проблемы логики и методологии науки. Киев, Наукова Думка, 1980, с. 193−230.

14. Л.Л. максимова. Теорема Крейга в суперинтуиционистских логиках и амальгамируемые многообразия псевдобулевых алгебр // Алгебра и логика. 1977. Т. 16. С. 643−681.

15. Л. Л. Максимова, В. В. Рыбаков. О решётке нормальных модальных логик // Алгебра и логика. 1974. Т. 13. С. 188−216.

16. П. С. Новиков. Конструктивная математическая логика с точки зрения классической. М., Наука, 1977.

17. И.Е. ОРЛОВ. Исчисление совместности высказываний // Математический сборник. 1928. Т. 35. С. 263−286.

18. Е. расёва, р. СикорскиЙ. Математика метаматематики. М., Наука, 1972.

19. В.В. РЫБАКОВ. Модальные логики с LM-аксиомами // Алгебра и логика. 1978. Т. 17. С. 455−468.

20. С.К. СОБОЛЕВ. О конечномерных суперинтуиционистских логиках // Известия АН СССР. Сер. матем. 1977. Т. 41. С. 963−986.

21. С.К. СОБОЛЕВ. О финитной аппроксимируемости суперинтуиционистских логик // Математический сборник. 1977. Т. 102. С. 289−301.

22. Р. фейс. Модальная логика. М., Наука, 1974.

23. A.B. ЧАГРОВ. О полиномиальной финитной аппроксимируемости модальных и суперинтуиционистских логик // Математическая логика, математическая лингвистика и теория алгоритмов. Калинин, КГУ, 1983, с. 75−83.

24. A.B. ЧАГРОВ. О сложности пропозициональных логик // Сложностные проблемы математической логики. Калинин, КГУ, 1985, с. 80−90.

25. A.B. ЧАГРОВ Многообразия логических матриц // Алгебра и логика. 1985. Т. 24. С. 426−489.

26. A.B. ЧАГРОВ. Нижняя оценка мощности аппроксимирующих шкал Крипке // Логические методы построения эффективных алгоритмов. Калинин, КГУ, 1986, с. 96−125.

27. A.B. ЧАГРОВ. Неразрешимые свойства расширений логики доказуемости // Алгебра и логика. 1990. Т. 29. С. 350−367, 613−623.

28. A.B. ЧАГРОВ. Неразрешимые свойства суперинтуиционистских логик // Математические вопросы кибернетики. Вып. 5: Сборник статей / Под ред. C.B. Яблонского. М., Физматлит, 1994, с. 62−108.

29. Л. А. Чагрова. О первопорядковой определимости интуиционистских формул с ограничениями на вхождения связок // Логические методы построения эффективных алгоритмов. Калинин, КГУ, 1986, с. 135−136.

30. В.б. шехтман. О неполных логиках высказываний // Доклады АН СССР. 1977. Т. 235. С. 542−545.

31. В.Б. шехтман. Неразрешимое суперинтуиционистское исчисление // Доклады АН СССР. 1978. Т. 240. С. 549−553.

32. В.Б. шехтман. Лестницы Ригера-Нишимуры // Доклады АН СССР. 1978. Т. 241. С. 1288−1291.

33. В.Б. шехтман. Семантика Крипке для пропозициональных логик с интуиционистской базой // Модальные и временные логики. ИФ АН СССР. 1979. С. 108−112.

34. В.б. шехтман. Топологические модели пропозициональных логик // Семиотика и информатика. 1980. Вып. 15. С. 74−98.

35. В.б. шехтман. Неразрешимые исчисления высказываний // Неклассические логики и их применение. Вопросы кибернетики. М., Наука, 1982, с. 74−115.

36. Л.Л. эсакиа. О топологических моделях Крипке // Доклады Академии Наук СССР. 1974. Т. 214. С. 298−301.

37. JI.JI. эсакиа. О многообразии алгебр Гржегорчика // Исследования по неклассическим логикам и теории множеств. М., Наука, 1979, с. 257−287.

38. Л.Л. эсакиа. К теории модальных и суперинтуиционистских систем // Логический вывод. М., Наука, 1979, с. 147−172.

39. В.А. ЯНКОВ. Построение последовательности сильно независимых суперинтуиционистских исчислений // Доклады АН СССР. 1968. Т. 181. С. 33−34.

40. В.А. ЯНКОВ. Конъюнктивно неразложимые формулы в пропозициональных исчислениях // Известия АН СССР. Сер. матем. 1969. Т. 33. С. 18−38.

41. А.Д. ЯШИН. Логика Сметанича Т^ и два определения новой интуиционистской связки II Математические заметки. 1994. Т. 56. С. 135−142.

42. J.G. ANDERSON. Superconstructive prepositional calculi with extra axiom schemes containing one variable / / Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik. 1972. Bd. 18. S. 113−130,.

43. S.N. Artemov. Operational modal logic. Technical Report 95−29, MSI, Cornell University, 1995.

44. J. barwise, L. moss. Vicious circles. CSLI Publications, Stanford, 1996.

45. F. bellissima. An effective representation for finitely generated free interior algebras 11 Algebra Universalis. 1985. V. 20. P. 302−317.

46. G. bezhanishvili, M. zakharyaschev. Logics over MIPC // In T. Shimura, editor, Sequent Calculus and Kripke Semantics, pp.86−95, RIMS, Kyoto University, No. 1021, 1997.

47. W.J. BLOK. Varieties of interior algebras. PhD thesis, University of Amsterdam, 1976.

48. W.J. Blok. On the degree of incompleteness in modal logics and the covering relation in the lattice of modal logics. Technical Report 78−07, Department of Mathematics, University of Amsterdam, 1978.

49. W.J. BLOK. The lattice of modal logics: an algebraic investigation // Journal of Symbolic Logic. 1980. V. 45. P. 221−236.

50. W.J. blok, P. kohler. Algebraic semantics for quasi-classical modal logics // Journal of Symbolic Logic. 1983. V. 48. P. 941−964.

51. G. Boolos. The unprovability of consistency: an essay in modal logic. Cambridge University Press, 1979.

52. G. boolos. On systems of modal logic with provability interpretations. // Theoria. 1980. V. 46. P. 7−18.

53. G. boolos. The logic of provability. Cambridge University Press, 1993.

54. M. Bozic, K. Dosen. Models for normal intuitionistic logics // Studia Logica. 1984. V. 43. P. 217−245.

55. R.A. bull. That all normal extensions of S4.3 have the finite model property // Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik. 1966. V. 12. P. 341−344.

56. R.A. BULL. MI PC as the formalization of an intuitionistic concept of modality // Journal of Symbolic Logic. 1966. V. 31. P. 609−616.

57. R.A. Bull, K. Segerberg. Basic modal logic // Handbook of Philosophical Logic, vol. II (edited by D. Gabbay and F. Guenthner), Reidel, Dordrecht, 1984, pp. 1−88.

58. A. Chagrov, M. zakharyaschev. On Hallden-completeness of intermediate and modal logics // Bulletin of the Section of Logic. 1990. V. 19. No. 1. P. 21−24.

59. A. CHAGROV, M. ZAKHARYASCHEV. The disjunction property of intermediate propositional logics // Studia Logica. 1991. V. 50. No. 2. P. 189−216.

60. A. CHAGROV, M. ZAKHARYASCHEV. Modal companions of intermediate propositional logics // Studia Logica. 1992. V. 51. No. 1. P. 49−82.

61. A. CHAGROV, M. ZAKHARYASCHEV. The undecidability of the disjunction property of propositional logics and other related problems // Journal of Symbolic Logic. 1993. V. 58. No. 3. P. 967−1002.

62. A. Chagrov, M. zakharyaschev. On the independent axiomatizability of modal and intermediate logics // Journal of Logic and Computation. 1995. V. 5. No. 3. P. 287−302.

63. A. CHAGROV, M. ZAKHARYASCHEV. Sahlqvist formulas are not so elementary even above S4. // Logic Colloquium '92 (edited by Laslo Csirmaz, Dov M. Gabbay and Maarten de Rijke). CSLI, Stanford, California, 1995, pp. 61−73.

64. A. CHAGROV, M. ZAKHARYASCHEV. Modal Logic. Clarendon Press, Oxford, 1997, 605 p.

65. L.A. CHAGROVA. An undecidable problem in correspondence theory // Journal of Symbolic Logic. 1991. V. 56. P. 1261−1272.

66. W. Craig. On axiomatizability within a system // Journal of Symbolic Logic. 1953. V. 18. P. 30−32.

67. K. Doets. Completeness and definability. PhD thesis, Universiteit van Amsterdam, 1987.

68. M.A.E. Dummett, E.J. Lemmon. Modal logics between S4 and S5 // Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik. 1959. V. 5. P. 250−264.

69. L.L. Esakia, V.Yu. Meskhi. Five critical systems // Theoria. 1977. V. 40. P. 52−60.

70. W.B. ewald. Intuitionistic tense and modal logic // Journal of Symbolic Logic, 1986. V. 51. P. 166−179.

71. K. Fine. The logics containing S4.3 // Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik. 1971. V. 17. P. 371−376.

72. K. fine. Logics containing S4 without the finite model property // Proceedings of Conference in Mathematical Logic, London 1970. Lecture Notes in Mathematics, vol. 255. Springer-Verlag, Berlin, 1972, pages 88−102.

73. K. Fine. An ascending chain of S4 logics // Theoria. 1974. V. 40. P. 110−116.

74. K. Fine. An incomplete logic containing S4 // Theoria. 1974. V. 40. P. 23−29.

75. K. Fine. Logics containing K4. Part /// Journal of Symbolic Logic. 1974. V. 39. P. 31−42.

76. K. FINE. Some connections between elementary and modal logic // Proceedings of the Third Scandinavian Logic Symposium. North-Holland, Amsterdam, 1975, pages 15−31.

77. K. Fine. Logics containing K4. Part //// Journal of Symbolic Logic. 1985. V. 50. P. 619−651.

78. G. fischer Servi. On modal logics with an intuitionistic base // Studia Logica. 1977. V. 36. P. 141−149.

79. G. FISCHER SERVI. Semantics for a class of intuitionistic modal calculi // In: (M. L. Dalla Chiara, editor) Italian Studies in the Philosophy of Science. Reidel, Dordrecht, 1980, pages 59−72.

80. D.M. GABBAY. On decidable, finitely axiomatizable modal and tense logics without the finite model property. I, II // Israel Journal of Mathematics. 1971. Y. 10. P. 478−495, 496−503.

81. D.M. GABBAY. On some new intuitionistic propositional connectives. 1/1 Studia Logica. 1977. V. 36. P. 127−139.

82. D.M. Gabbay. Semantical investigations in Heyting’s intuitionistic logic, Reidel, Dordrecht, 1981.

83. D.M. gabbay, D.H.J. de Jongh. A sequence of decidable finitely axiomatizable intermediate logics with the disjunction property // Journal of Symbolic Logic. 1974. V. 39. P. 67−78.

84. K. GODEL. Eine Interpretation des intuitionistischen Aussagenkalkuls // Ergebnisse eines mathematischen Kolloquiums. 1933. V. 4. P. 39−40.

85. R.I. goldblatt. Metamathematics of modal logic. Part I // Reports on Mathematical Logic. 1976. V. 6. P. 41−78.

86. R.I. goldblatt, S.K. Thomason. Axiomatic classes in propositional modal logic. // (J. Crossley, ed.) Algebraic Logic, Lecture Notes in Mathematics. Springer, Berlin. 1974. V. 450. P. 163−173.

87. A. grzegorczyk. Some relational systems and the associated topological spaces // Fundamenta Mathematicae. 1967. V. 60. P. 223−231.

88. R. HARROP. On the existence of finite models and decision procedures for propositional calculi // Proc. Cambridge Philos. Soc. 1958. V. 54. P. 1−13.

89. J. HlNTlKKA. Quantifiers in deontic logic // Societas Scientiarum Fennica, Commentationes humanarum litterarum. 1957. V. 23. P. 1−23.

90. G.E. Hughes, M.J. Cresswell. A companion to modal logic. Methuen, London, 1984.

91. В. jonsson, А. tarski. Boolean algebras with operators // American Journal of Mathematics. 1951. V. 73. No. 4. P. 891−939.

92. S. KANGER. The Morning Star paradox // Theoria. 1957. V. 23. P. 1−11.

93. A.V. kuznetsov, A.YU. Muravitskij. On superintuitionistic logics as fragments of proof logic extensions // Studia Logica. 1986. V. 45. P. 77−99.

94. E.J. lemmon. Algebraic semantics for modal logic. I, II // Journal of Symbolic Logic. 1966. V. 31. P. 46−65, 191−218.

95. C.I. Lewis. A survey of symbolic logic. University of California Press, Berkeley, 1918.

96. C.I. lewis, C.H. langford. Symbolic logic. Appleton-Century-Crofts, New York, 1932.

97. D.C. MAKINSON. On some completeness theorems in modal logic // Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik. 1966. V. 12. P. 379 384.

98. D.C. MAKINSON. Some embedding theorems for modal logic / / Notre Dame Journal of Formal Logic 1971. V. 12. P. 252−254.

99. L. MAKSIMOVA. On maximal intermediate logics with the disjunction property. // Studia Logica. 1986. V. 45. P. 69−75.

100. J. MCKAY. The decidability of certain intermediate logics // Journal of Symbolic Logic. 1968. V. 33. No. 2. P. 258−264.

101. R. McKENZIE. Equational bases and non-modular lattice varieties // Transactions of the American Mathematical Society. 1972. V. 174. P. 1−43.

102. J.C.C. McKlNSEY. A solution of the decision problem, for the Lewis systems S2 and S4, with an application to topology // Journal of Symbolic Logic. 1941. V. 6. P. 117−134.

103. J.C.C. McKlNSEY, A. TARSKI. The algebra of topology // Annals of Mathematics. 1944. V. 45. P. 141−191.

104. J.C.C. McKlNSEY, A. TARSKI. On closed elements in closure algebras // Annals of Mathematics. 1946. V. 47. P. 122−162.

105. J.C.C. McKlNSEY, A. TARSKI. Some theorems about the sentential calculi of Lewis and Heyting // Journal of Symbolic Logic. 1948. Y. 13. P. 1−15.

106. I. NlSHlMURA. On formulas of one variable in intuitionistic propositional calculus // Journal of Symbolic Logic. 1960. V. 25. P. 327−331.

107. H. Ono. Some results on the intermediate logics // Publications of the Research Institute for Mathematical Science, Kyoto University. 1972. V. 8. P. 117−130.

108. H. Ono. On some intuitionistic modal logics // Publications of the Research Institute for Mathematical Science, Kyoto University. 1977. V. 13. P. 55−67.

109. H. Ono, A. Nakamura. On the size of refutation Kripke models for some linear modal and tense logics // Studia Logica. 1980. V. 39. P. 325−333.

110. H. Ono, N. Suzuki. Relations between intuitionistic modal logics and intermediate predicate logics // Reports on Mathematical Logic. 1988. V. 22. P. 65−87.

111. G.D. Plotkin, C.P. Stirling. A framework for intuitionistic modal logic. In: (J.Y. Halpern, editor) Reasoning about knowledge, pages 399−406, 1986.

112. A. prior. Time and modality. Clarendon Press, Oxford, 1957.

113. W. rautenberg. Klassische und nichtklassische Aussagenlogik. Vieweg, Braunschweig-Wiesbaden, 1979.

114. P.h. rodenburg. Intuitionistic correspondence theory. PhD thesis, University of Amsterdam, 1986.

115. V.V. rybakov. Criteria for admissibility of inference rules. Modal and intermediate logics with the branching property // Studia Logica. 1994. V. 53. P. 203−226.

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

117. S.J. SCROGGS. Extensions of the Lewis system S5 // Journal of Symbolic Logic. 1951. V. 16. P. 112−120.

118. K. SEGERBERG. An essay in classical modal logic. Filosofiska Studier 13. Uppsala, 1971.

119. K. SEGERBERG. That all extensions of S4.3 are normal // Proceedings of the Third Scandinavian Logic Symposium. North-Holland, Amsterdam, 1975, pages 194−196.

120. V.Yu. SHAVRUKOV. Subalgebras of diagonalizable algebras of theories containing arithmetic // Dissertationes Mathematicae (Rozprawy Matematyczne, Polska Akademia Nauk, Instytut Matematyczny). Warszawa, 323, 1993.

121. R. solovay. Provability interpretations of modal logic // Israel Journal of Mathematics. 1976. V. 25. P. 287−304.

122. V.H. SOTIROV. Modal theories with intuitionistic logic // Proceedings of the Conference on Mathematical Logic, Sofia, 1980. Bulgarian Academy of Sciences, 1984, pages 139−171.

123. E. spaan. Complexity of modal logics. PhD thesis, Department of Mathematics and Computer Science, University of Amsterdam, 1993.

124. C.P. stirling. Modal logics for communicating systems // Theoretical Computer Science. 1987. V. 49. P. 311−347.

125. M.H. STONE. Application of the theory of Boolean rings to general topology // Transactions of the American Mathematical Society. 1937. V. 41. P. 321−364.

126. S.K. THOMASON. An incompleteness theorem in modal logic // Theoria. 1974. V. 40. P. 30−34.

127. S.K. THOMASON. The logical consequence relation of propositional tense logic // Zeitschrift fur mathematische Logik und Grundlagen der Mathematik. 1975. V. 21. P. 29−40.

128. S.K. THOMASON. Undecidability of the completeness problem of modal logic // Universal Algebra and Applications, Banach Center Publications. PNW-Polish Scientific Publishers, Warsaw. 1982. V. 9. P. 341−345.

129. J.A.F.K. van Benthem. Modal reduction principles // Journal of Symbolic Logic. 1976. V. 41. P. 301−312.

130. J.A.F.K. VAN BENTHEM. Modal logic and classical logic. Bibliopolis, Napoli, 1983.

131. J.A.F.K. VAN BENTHEM. Correspondence theory. In Handbook of Philosophical Logic, (D.M. Gabbay, F. Guenthner, eds.) Reidel, Dordrecht, 1984. V. 2. P. 167−247.

132. J.A.F.K. van Benthem. Notes on modal definability. // Notre Dame Journal of Formal Logic. 1989. V. 39. P. 20−39.

133. D. WlJESEKERA. Constructive modal logic /// Annals of Pure and Applied Logic. 1990. V. 50. P. 271−301.

134. T. WILLIAMSON. On intuitionistic modal epistemic logic // Journal of Philosophical Logic. 1992. V. 21. P. 63−89.

135. F. WOLTER. Lattices of modal logics. PhD thesis, Freie Universitat Berlin, 1993.

136. F. WOLTER. Properties of tense logics // Mathematical Logic Quarterly. 1996. V. 42. P. 481−500.

137. F. WOLTER. Completeness and decidability of tense logics closely related to logics above K4 // Journal of Symbolic Logic. 1997. V. 62. P. 131−158.

138. F. wolter. Fusions of modal logics revisited //In (M. Kracht, M. de Rijke, H. Wansing, M. Zakharyaschev editors), Advances in Modal Logic, 1997, CSLI, Stanford.

139. M. zakharyaschev. Theorem proving in intermediate and modal logics // Lecture Notes in Computer Science. (O.B. Lupanov, editor) 1987. V. 278. P. 492−496.

140. M. zakharyaschev. Canonical formulas for K4. Parti: Basic results // Journal of Symbolic Logic. 1992. V. 57. P. 1377−1402.

141. M. zakharyaschev. Intermediate logics with disjunction free axioms are canonical // IGPL Newsletter. 1992. V. 1. P. 7−8.

142. M. zakharyaschev. A sufficient condition for the finite model property of modal logics above K4 // Bulletin of the IGPL. 1993. V. 1. P. 13−21.

143. M. zakharyaschev, A new solution to a problem of Hosoi and Ono // Notre Dame Journal of Formal Logic. 1994. V. 35. P. 450−457.

144. M. zakharyaschev. Canonical formulas for K4. Part II: Cofinal subframe logics // Journal of Symbolic Logic. 1996. V. 61. P. 421−449.

145. M. zakharyaschev. Canonical formulas for K4. Part III: The finite model property 11 Journal of Symbolic Logic. 1997. V. 62. P. 950−975.

146. M. zakharyaschev. The greatest extension of S4 into which intuitionistic logic is embeddable // Studia Logica. 1997. V. 59. P. 345−358.

147. M. zakharyaschev. Canonical formulas for modal and superintuitionistic logics: a short outline. In M. de Rijke, editor, Advances in Intensional Logic, pp. 195−248, Kluwer Academic Publishers, 1997.

148. M. zakharyaschev, a. alekseev. All finitely axiomatizable normal extensions of K4.3 are decidable // Mathematical Logic Quarterly. 1995. V. 41. P. 15−23.