Допустимые и выводимые правила вывода в нестандартных логиках Юрасова Екатерина Михайловна

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

Введение

1 Предварительные сведения о допустимых правилах вывода в нестандартных логиках 19

1.1 Модальные, временные и суперинтуиционистские логики 19

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

1.3 Допустимые и выводимые правила вывода 32

2 Допустимость правил вывода для некоторого класса логик, не обладающих свойством ветвления 35

2.1 Предварительные сведения 36

2.2 Алгоритмический критерий допустимости правил вывода для некоторого класса .94-логик, не обладающих свойством ветвления 40

3 Допустимость правил вывода для логики с с оператором "завтра" 50

3.1 Предварительные сведения -51

3.2 Свойства логики С 53

3.3 Условие допустимости правил вывода в логике 57

4 Структурно-полные логики 66

4.1 Структурно-полные логики: необходимые предварительные сведения 66

4.2 Описание структурно-полных 5"4-логик ширины 2, порожденных конечным корневым фреймом с двухэлементным первым слоем 71

4.3 О ширине структурно-полных табличных логик -84

Заключение 87

Литература 89

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

• Семантика Крипке
• Алгоритмический критерий допустимости правил вывода для некоторого класса .94-логик, не обладающих свойством ветвления
• Условие допустимости правил вывода в логике
• Описание структурно-полных 5"4-логик ширины 2, порожденных конечным корневым фреймом с двухэлементным первым слоем

Введение к работе

Актуальность темы. Теория нестандартных систем логического вывода сформировалась в начале двадцатых-тридцатых годов 20-го века в работах Лукасе-вича, Льюиса, Геделя и Тарского, как результат анализа поведения аксиоматических систем оснований математики и парадоксов материальной импликации. Однако нестандартные логики по сравнению с классической логикой, отличаются большим разнообразием синтаксиса и семантики. Поэтому к концу 20-го века возникло много новых направлений исследований, связанных с применением идей и методов нестандартной логики в программировании, информатике, теории искусственного интеллекта, представлении знаний и других областях знаний (см., например, [40, 41, 54, 80, 83, 99]).

Большое влияние на становление теории нестандартных систем логического вывода оказано классической теорией доказательств, одним из центральных моментов которой являются правила вывода, поскольку от них зависит эффективность доказательств. Первыми работами, непосредственно посвященными изучению правил вывода, были работы Лося (1955), Тарского (1956) и Сушко (1958). При исследовании правил вывода естественно возник вопрос о том какие правила можно присоединять к логическим системам, сохраняя при этом множество доказуемых теорем системы. Такой класс правил, получивших название допустимых правил вывода, был определен П. Лоренценом [71] в 1955 году. Оказалось, что это в точности допустимые правила вывода - правила, относительно которых данная логика замкнута. Несколько ранее проблема допустимых правил вывода для интуиционистской логики изучалась П.С. Новиковым, который наряду с понятием производного правила вывода (допустимого правила вывода) рассматривал понятие сильного производного правила вывода. В работе [16] Новиков затронул дедуктивные аспекты производных правил вывода в интуиционистской логике. Вслед за Лоренценом и Новиковым изучением допустимых правил вывода занимался СЮ. Маслов [11, 12, 13], им исследовалась возможность применения выводимых и допустимых правил вывода в различных сферах деятельности.

В нестандартных логиках, как правило, класс допустимых правил вывода шире класса выводимых правил вывода. Примеры допустимых, но не выводимых правил вывода, были получены Р. Харропом [55], Г.Е. Минцем [14, 15]. Логика, в которой множества допустимых и выводимых правил вывода совпадают, называется структурно-полной. В настоящее время известно, что большинство базисных логик, например, Я, А 4, 54, 5 5 и др., не являются структурно-полными. Структурная полнота не является инвариантом заданной логики, она зависит от выбора аксиоматической системы. Однако, во многих распространенных классах логик правила вывода обычно фиксированы и выбор аксиоматической системы зависит от изменения множества аксиом. Для таких классов логик имеет смысл понятие структурной полноты. Поэтому исследования, касающиеся структурной полноты, представляют интерес для многих ученых. Токарз установил структурную полноту некоторых логик Лукасевича [97], Прукнал доказал структурную полноту логики Медведева конечных задач [82], Войтыляк показал, что конечные классы многозначных логик являются структурно-полными [103]. Дзиобяк нашел полное описание локально конечных структурно-полных модальных логик, расширяющих К А [46]. В [29] Циткину удалось описать все наследственно структурно-полные суперинтуиционистские логики, т.е. логики, всякое расширение которых является структурно-полным. Позже Рыбаковым было получено полное описание наследственно структурно-полных мо дальных логик над К А [89]. А, именно, модальная логика А является наследственно структурно-полной тогда и только тогда, когда А не содержится ни в одной из двадцати специальных табличных логик. Однако уже для структурно-полных 5"4-логик малой глубины (меньше 5) класс структурно-полных логик шире класса наследственно структурно-полных логик. Поэтому особый интерес представляет описание классов структурно-полных логик над S4, К4.

После того как выяснилось, что для большинства нестандартных логик класс допустимых правил шире класса выводимых правил возникли вопросы алгоритмической разрешимости задачи распознавания допустимых правил вывода. Проблема нахождения алгоритма, распознающего допустимость правил вывода в интуиционистской логике была сформулирована в обзоре проблем X. Фридмана [50], родственная проблема существования конечного базиса для допустимых правил этой логики была поставлена А.В. Кузнецовым (см. [50] (проблема 42), [9]). Положительное решение проблемы Кузнецова давало бы и положительное решение проблемы Фридмана. Проблема алгоритмического распознавания допустимости в интуиционистской логике была решена положительно Рыбаковым [18], после чего вопрос о существовании конечного базиса был решен отрицательно так же Рыбаковым [19, 20]. Естественно возник вопрос построения бесконечного базиса, который позже был построен Ием-хофф для интуиционистской логики [59]. Затем Рыбаков построил, также бесконечный, базис для логики S4 [91]. Развивая методы, использованные для решения проблемы допустимости для интуиционистской логики, В.В.Рыбаков доказал разрешимость проблемы допустимости правил вывода в таких важных логиках, как QL, Grz, S4, К4 и в некоторых других логиках [21]-[28], [84]-[88]. В частности, была доказана разрешимость проблемы допустимости правил вывода во всех расширени ях логики 5"4.3, ЧТО является обобщением результата Файна [48] о разрешимости данных логик. На основе техники, разработанной В.В. Рыбаковым, проблема допустимости была решена для различных индивидуальных транзитивных логик (см. например [1, 2, 37, 5]).

При решении данных вопросов основным инструментом являлась реляционная семантика (или семантика Крипке, [64, 65]), причем ключевым моментом были специальные модели Крипке - n-характеристические модели. Так, разрешимость проблемы допустимости в логике эквивалентна разрешимости квазиэквациональной теории свободных алгебр многообразия, порожденного этой логикой. С помощью техники, позволяющей представить свободные алгебры из многообразия модальных алгебр n-характеристическими моделями, была решена проблема распознавания допустимых правил вывода для широкого класса модальных транзитивных логик. Отметим, что описание свободных модальных и псевдобулевых алгебр для многообразий модальных и псевдобулевых алгебр, соответствующих индивидуальным логикам, является распространенной задачей при исследовании нестандартных логик (см. [3, 17, 18, 31, 34, 35]). Особую важность представляло описание свободных алгебр не для индивидуальных многообразий, а для всех многообразий финитно-, аппроксимируемых транзитивных логик, которое и было дано Рыбаковым в [90].

Ранее было отмечено, что ценность допустимых правил вывода заключается в том, что такие правила позволяют нам сократить и упростить выводы в дедуктивной системе заданной логики. Другой причиной, по которой изучаются данные правила вывода, являются различные приложения. Так, в работе Л.Л. Максимовой [74] приведено исследование свойств строгой разрешимости модальных и интуиционистских исчислений, рассмотрена проблема строгой разрешимости проективного свойства

Бета над интуиционистским пропозициональным исчислением. Для доказательства строгой разрешимости проективного свойства Бета над интуиционистским пропозициональным исчислением достаточно решить проблему разрешимости по допустимости суперинтуиционистских логик с таким свойством. Максимовой [73] было показано, что существует точно 16 суперинтуиционистских логик, обладающих проективным свойством Бета. Из результатов В.В. Рыбакова [90] следует разрешимость проблемы допустимости для всех логик с таким свойством, кроме логик под номером 9, 13, 15 из полного списка логик с проективным свойством Бета [74]. Несмотря на то, что Рыбаков получил достаточно общий критерий допустимости правил вывода для финитно-аппроксимируемых логик [90], данный критерий не является универсальным, поскольку одним из условий является наличие свойства ветвления ниже к. Так, логика, указанная под номером 9 в полном списке логик с проективным свойством Бета, не обладает свойством ветвления ниже к ни для какого к. Решение проблемы распознавания допустимых правил вывода в данной логике представлено в настоящей диссертационной работе. Также с работой Л.Л.Максимовой [74] связано исследование логики 5 400 , не обладающей свойством ветвления, на разрешимость по допустимости правил вывода. Данная задача была решена в [93] и позволила обосновать предположение о строгой разрешимости интерполяционного свойства над логикой SA, которое было выдвинуто в статье Л.Л.Максимовой [74].

Несмотря на глубокую разработку направления допустимых правил вывода, большинство результатов было получено для транзитивных логик. В настоящее время особый интерес представляют нетранзитивные логики, так как основные результаты и техники, использующиеся для исследования допустимых правил вывода в транзитивных логиках, применять непосредственно при изучении допустимых правил вы вода в нетранзитивных логиках не удаётся. Как было отмечено, при исследовании допустимых правил вывода центральную роль играют n-характеристические модели Крипке: для всякого правила вывода в модальной логике существует конечное, с точностью до изоморфизма, множество n-характеристических моделей Крипке, на элементах которого можно проверять истинность правила, для выяснения его допустимости. Однако при построении п-характеристической модели возникает немало вопросов. На самом деле, построение п-характеристической модели является достаточно ясным только для расширений модальной логики КА и интуиционистской логики. В случае нетранзитивной логики данные модели описаны только для очень малого списка логик, в частности, для К (см., например, [42]). В случае нетранзитивных временных логик описание упомянутых выше моделей представляется еще более сложной задачей. Цель работы.

1. Исследовать на разрешимость по допустимости правил вывода суперинтуиционистскую логику, порожденную классом всех конечных корневых фреймов F, удовлетворяющих условию {xRyk {yRx)kyRzkyRu) -+ Sv(zRvkuRv), где R - отношение на фрейме F. Положительное решение данной задачи позволяет обосновать предположение о строгой разрешимости проективного свойства Бета над логикой /z1} которое было выдвинуто в статье Л.Л. Максимовой [74].

2. Исследовать на разрешимость по допустимости логику с оператором "завтра".

3. Получить описание конечных корневых -фреймов ширины 2, порождающих

структурно-полные логики.

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

Научная новизна. Все результаты, полученные в диссертации, являются новыми и снабжены подробными доказательствами. Результаты совместных работ получены в нераздельном соавторстве. Основные результаты. В диссертации получены следующие основные результаты.

1. Получен алгоритмический критерий распознавания допустимых правил вывода для б -логики fi2, порожденной классом всех конечных корневых фреймов F, удовлетворяющих условию (xRy&- (yRx)kyRz&yRu) - Bv(zRvkuRv), где R - отношение на фрейме F.

2. Доказано, что логика /х2 © Grz и суперинтуиционистская логика, порожденная классом всех конечных корневых фреймов F, удовлетворяющих условию (xRy&-i(yRx)kyRzk,yRu) —у 3v(zRvkuRv), где R - отношение на фрейме F, разрешима относительно допустимости правил вывода.

3. Получен алгоритмический критерий распознавания допустимых правил вывода для логики с оператором "завтра".

4. Получены необходимые и достаточные условия того, что 5"4-логика A(F) ширины 2, порожденная конечным корневым фреймом без узлов с двухэлементным первым слоем, является структурно-полной.

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

• XXXVII-международной научной студенческой конференции "Студент и научно-технический прогресс"(Новосибирск,1999),

• XXXVIII-международной научной студенческой конференции "Студент и научно-технический прогресс" (Новосибирск,2000),

• ХХХІХ-международной научной студенческой конференции "Студент и научно-технический прогресс"(Новосибирск,2001),

• XL-международной научной студенческой конференции "Студент и научно-технический прогресс" (Новосибирск, 2002),

• международной конференции "Ломоносовские чтения" (Москва, 2000),

• международной конференции "Логика и приложения", посвященной 60-летию со дня рождения Ю.Л. Ершова (Новосибирск, 2000),

• международной конференции "Дифференциальные уравнения и симметрия" (Красноярск, 2000),

• международной научной конференции "Молодая наука - XXI веку" (Иваново, 2001),

• II Всесибирском конгрессе, посвященному Софьи Ковалевской (Красноярск, 2002),

• международной конференции "Алгебра и ее приложения", посвященной 70-летию со дня рождения В.П.Шункова и 65-летию В.М.Бусаркина(Красноярск, 2002),

• международной конференции "Мальцевские чтения" (Новосибирск, 2003),

• международной конференции "Алгебра, логика и кибернетика", посвященной 75-летию со дня рождения А.И.Кокорина (Иркутск, 2004).

Публикации. По теме диссертации опубликовано 22 работы [104]-[125]. Структура и объём работы. Диссертация состоит из введения, четырех глав, заключения и библиографического списка, включающего 103 наименования. Объём работы 103 страницы машинописного текста. Обзор содержания диссертации и полученных результатов.

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

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

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

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

В разделе 1.3 дается описание n-характеристических моделей Крипке для модальных логик и ряд свойств n-характеристической модели. Приведены критерии допустимости правил вывода и структурной полноты модальных Л 4-логик через n-характеристические модели.

Во второй главе представлено решение проблемы допустимости правил вывода для модальной 54-логики /І2, порожденной классом всех конечных корневых фреймов F, удовлетворяющих условию

(xRyk-i(yRx)&yRzkyRu) -» Bv(zRvLuRv),

где R - отношение на фрейме F. Данная проблема также решена для модальной логики n2®Grz, откуда следует разрешимость по допустимости супериптуиционистской логики ці, порожденной классом всех конечных корневых фреймов F, удовлетворяющих условию (xRySz- (yRx)kyRzSzyRu) -» Sv(zRvkuRv).

В разделе 2.1 приведены необходимые сведения, касающиеся связи между модальными и суперинтуиционистскими логиками: определен Г-перевод для формул и правил вывода, сформулировано определение модальных напарников для суперинтуиционистских логик и др. В данном разделе представлены результаты, полученные В.В. Рыбаковым при исследовании проблемы допустимости правил вывода для модальных логик над К4, приведены определения свойства е/-ветвления ниже некоторого к, свойства ветвления ниже некоторого к, свойства реализации возможностей. В конце раздела введены определения, необходимые при исследовании логик цх, fi2, И2Ф Grz. Также введена модификация понятия свойства реализации возможностей, которая является важным моментом при исследовании логик /лх, ц2, Ц2 Ф Grz.

В разделе 2.2 представлено решение проблемы разрешимости по допустимости для логик /лх, Ц2, р-2 Ф Grz. Данные логики не обладают свойством ветвления ниже А; ни для какого к, наличие которого является одним из условий в алгоритмическом критерии допустимости правил вывода (см. [90], теорема 3.5.2). Однако исследование логики ці можно свести к работе над логикой 54.2, которая обладает свойством ветвления ниже 1 и к которой применим алгоритмический критерий допустимости правил вывода (см. [90], теорема 3.5.2). Пользуясь вышеуказанным свойством логики /J.2, в данном разделе разработан алгоритмический критерий распознавания допустимости правил вывода в модальных логиках ц2 и fi2®Grz. И ввиду известной связи между модальными и суперинтуиционистскими логиками (см. [90], теорема 3.2.2) получено решение проблемы разрешимости по допустимости для суперинтуиционистской ЛОГИКИ Цх Основными леммами раздела 2.2 являются

Лемма 2.2. Пусть правило вывода г := ах,... ,схп/0 от к переменных не допустимо в логике \i. Тогда существует ц-моделъ М := (M,R,S) = (U- i) U Дм где Mj - открытая подмодель модели М такая, что 3cjix Є MJ(XRCJ) и Вм множество висячих вершин модели М, удовлетворяющая условиям:

(а) подфрейм Si(M) изоморфен подфрейму S Ch k));

(б) модель М. имеет не более, чем 22 Г(п) + (1 + 2Г("))2 -1 сгустков, где п - число подформул правила г;

(в) модель Л4 имеет свойство реализации возможностей относитель)іо подформул правила г для каждой антицепи Е, не содержащей висячих вершин, причем если Е - антицепь, не содержащая висячих вершин, и Е С Mj, то существует элемент ХЕ Є M.J, для которого выполняется свойство реализации возможностей для антицепи Е;

(г) модель М. опровергает правило г.

Лемма 2.3. Пусть существует fi-модель М, описанная в лемме 2.2. Тогда правило вывода г := е і,... ,ап/Р от к переменных не допустимо в логике ц.

Из лемм 2.2, 2.3 вытекает главная теорема данного раздела

Теорема 2.2. Модальные логики ц2, /J 2 Ф Grz разрешимы относительно допустимости правил вывода.

Из теоремы 2.2 получаем

Следствие 2.1. Суперинтуиционистская логика /лі, наименьший модальный напарник Т(/ЛІ) и наибольший модальный напарник o (fj,i) логики цх над S4 разрешимы относительно допустимости правил вывода.

В третьей главе приведены результаты исследований проблемы допустимости правил вывода для временной нетранзитивной логики С с оператором "завтра". В настоящее время особый интерес представляют нетранзитивные логики, так как основные результаты и техники, использующиеся для исследования допустимых правил вывода в транзитивных логиках, применять непосредственно при изучении до пустимых правил вывода в нетранзитивных логиках не удаётся. Ранее допустимость правила вывода определялась его поведением на верхних слоях специальной «-характеристической модели Крипке [90]. В данной работе свойства правила вывода определяются через его поведение в ограниченной окрестности каждой из точек «-характеристической модели. Эта новая техника используется для доказательства разрешимости по допустимости логики С и ряда других свойств данной логики.

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

Основными результатами раздела 3.2 являются построение п-характеристической модели Chc{n) для логики С и описание свойств модели Chc(n). Показано, что в логике С любая формула представима в стандартном виде, а также отмечены некоторые эквивалентности логики , необходимые для доказательства дальнейших результатов. Кроме того, определен класс характеристических фреймов для логики С и показано, что логика С является финитно-аппроксимируемой и разрешимой.

В разделе 3.3 построен алгоритмический критерий допустимости правил вывода в логике С. При получении данного результата использовался критерий допустимости правил вывода в модальных логиках, основанный на n-характеристических моделях, построенных в разделе 3.2.

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

Теорема 3.1. Пусть правило вывода sf(r(x0,-.. ,Xk-i)) не допустимо в логике

С Тогда во фрейме G{r), порождённом правилом г, существует цикл С длины, не превышающей числа элементов G(r), и удовлетворяющий условиям:

1) цикл С содержит элемент Ш{0 такой, что формула о»,-0, входящая в посылку правила sf(r), содержит формулу - хо,

2) некоторый элемент u j цикла С является рефлексивным, т.е. UJRGUJJ. Теорема 3.2. Пусть во фрейме G(r), порождённом правилом r(xQ,... ,Xk-\),

существует цикл С, удовлетворяющий условиям 1)-2) теоремы 3.1. Тогда правило sf(r(xo,... , Xk-i)) не допустимо в логике С.

В силу конечности посылки правила вывода из теорем 3.1, 3.2 вытекает

Теорема 3.3. Модальная логика С разрешима относительно допустимости правил вывода.

Пользуясь алгоритмическим критерием допустимости правил вывода в логике , не сложно доказать следующую теорему.

Теорема 3.4. Логика С не является структурно-полной.

В четвертой главе на основе методов, разработанных В.В. Рыбаковым [90], приведено исследование структурно-полных 54-логик.

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

В разделе 4.2 получены необходимые и достаточные условия того, что -логика A(F) ширины 2, порожденная конечным корневым фреймом без узлов с двухэлементным первым слоем, является структурно-полной. Основным результатом раздела 4.2 является

Теорема 4.1 Логика A(F) ширины 2, порожденная конечным корневым фреймом

F без узлов таким, что ,S7i(F) = 2, является структурно-полной тогда и только тогда, когда F удовлетворяет следующим условиям:

1) сгустки первого слоя являются одноэлементными;

2) конакрытие для двух несравнимых сгустков является одноэлементным;

3) не существует конакрытия для двух несравнимых сгустков из разных слоев;

4) для любого слоя фрейма, отличного от корня, существует конакрытие;

5) все слои, кроме корня, состоят из двух сгустков.

В разделе 4.3 представлены результаты, касающиеся ширины структурно-полных табличных 5"4-логик.

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

Автор выражает искреннюю благодарность Владимиру Владимировичу Рыбакову и Михаилу Ивановичу Голованову за постановку задачи, помощь в работе, за неизменное внимание и терпение.

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

Актуальность темы. Теория нестандартных систем логического вывода сформировалась в начале двадцатых-тридцатых годов 20-го века в работах Лукасе-вича, Льюиса, Геделя и Тарского, как результат анализа поведения аксиоматических систем оснований математики и парадоксов материальной импликации. Однако нестандартные логики по сравнению с классической логикой, отличаются большим разнообразием синтаксиса и семантики. Поэтому к концу 20-го века возникло много новых направлений исследований, связанных с применением идей и методов нестандартной логики в программировании, информатике, теории искусственного интеллекта, представлении знаний и других областях знаний (см., например, [40, 41, 54, 80, 83, 99]). Большое влияние на становление теории нестандартных систем логического вывода оказано классической теорией доказательств, одним из центральных моментов которой являются правила вывода, поскольку от них зависит эффективность доказательств. Первыми работами, непосредственно посвященными изучению правил вывода, были работы Лося (1955), Тарского (1956) и Сушко (1958). При исследовании правил вывода естественно возник вопрос о том какие правила можно присоединять к логическим системам, сохраняя при этом множество доказуемых теорем системы. Такой класс правил, получивших название допустимых правил вывода, был определен П. Лоренценом [71] в 1955 году. Оказалось, что это в точности допустимые правила вывода - правила, относительно которых данная логика замкнута. Несколько ранее проблема допустимых правил вывода для интуиционистской логики изучалась П.С. Новиковым, который наряду с понятием производного правила вывода (допустимого правила вывода) рассматривал понятие сильного производного правила вывода. В работе [16] Новиков затронул дедуктивные аспекты производных правил вывода в интуиционистской логике. Вслед за Лоренценом и Новиковым изучением допустимых правил вывода занимался СЮ. Маслов [11, 12, 13], им исследовалась возможность применения выводимых и допустимых правил вывода в различных сферах деятельности. В нестандартных логиках, как правило, класс допустимых правил вывода шире класса выводимых правил вывода. Примеры допустимых, но не выводимых правил вывода, были получены Р. Харропом [55], Г.Е. Минцем [14, 15]. Логика, в которой множества допустимых и выводимых правил вывода совпадают, называется структурно-полной. В настоящее время известно, что большинство базисных логик, например, Я, А 4, 54, 5 5 и др., не являются структурно-полными. Структурная полнота не является инвариантом заданной логики, она зависит от выбора аксиоматической системы. Однако, во многих распространенных классах логик правила вывода обычно фиксированы и выбор аксиоматической системы зависит от изменения множества аксиом. Для таких классов логик имеет смысл понятие структурной полноты.

Поэтому исследования, касающиеся структурной полноты, представляют интерес для многих ученых. Токарз установил структурную полноту некоторых логик Лукасевича [97], Прукнал доказал структурную полноту логики Медведева конечных задач [82], Войтыляк показал, что конечные классы многозначных логик являются структурно-полными [103]. Дзиобяк нашел полное описание локально конечных структурно-полных модальных логик, расширяющих К А [46]. В [29] Циткину удалось описать все наследственно структурно-полные суперинтуиционистские логики, т.е. логики, всякое расширение которых является структурно-полным. Позже Рыбаковым было получено полное описание наследственно структурно-полных мо дальных логик над К А [89]. А, именно, модальная логика А является наследственно структурно-полной тогда и только тогда, когда А не содержится ни в одной из двадцати специальных табличных логик. Однако уже для структурно-полных 5"4-логик малой глубины (меньше 5) класс структурно-полных логик шире класса наследственно структурно-полных логик. Поэтому особый интерес представляет описание классов структурно-полных логик над S4, К4. После того как выяснилось, что для большинства нестандартных логик класс допустимых правил шире класса выводимых правил возникли вопросы алгоритмической разрешимости задачи распознавания допустимых правил вывода. Проблема нахождения алгоритма, распознающего допустимость правил вывода в интуиционистской логике была сформулирована в обзоре проблем X. Фридмана [50], родственная проблема существования конечного базиса для допустимых правил этой логики была поставлена А.В. Кузнецовым (см. [50] (проблема 42), [9]). Положительное решение проблемы Кузнецова давало бы и положительное решение проблемы Фридмана. Проблема алгоритмического распознавания допустимости в интуиционистской логике была решена положительно Рыбаковым [18], после чего вопрос о существовании конечного базиса был решен отрицательно так же Рыбаковым [19, 20]. Естественно возник вопрос построения бесконечного базиса, который позже был построен Ием-хофф для интуиционистской логики [59]. Затем Рыбаков построил, также бесконечный, базис для логики S4 [91]. Развивая методы, использованные для решения проблемы допустимости для интуиционистской логики, В.В.Рыбаков доказал разрешимость проблемы допустимости правил вывода в таких важных логиках, как QL, Grz, S4, К4 и в некоторых других логиках [21]-[28], [84]-[88]. В частности, была доказана разрешимость проблемы допустимости правил вывода во всех расширени ях логики 5"4.3, ЧТО является обобщением результата Файна [48] о разрешимости данных логик. На основе техники, разработанной В.В. Рыбаковым, проблема допустимости была решена для различных индивидуальных транзитивных логик (см.

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

Прежде, чем перейти к доказательству леммы 2.2, определим функцию Г(п) следующим образом Г(п) = (1+7(2) + ... + 7(2п + 1)), где 7(р+ 1) - некоторая функция, удовлетворяющая следующим неравенствам: 7(1) = 1,7(2) 22\7(р+1) 2 ). Лемма 2.2. Пусть правило вывода г := cxi,... , а„//3 от к переменных не допустимо в логине р.. Тогда существует ц-моделъ М := (M,R,S) = (U- i) U Вм, где Mj -открытая подмодель модели М такая, что BCJWX Є MJ(XRCJ) и Вм - множество висячих вершин модели М, удовлетворяющая условиям: (а) подфрейм Si{M) изоморфен подфрейму Si(Ch (k)); к (б) модель М. имеет не более, чем 22 Г(п) + (1 + 2Г())2 -1 сгустков, где п - число подформул правила г; (в) модель М имеет свойство реализации возможностей относительно подфор мул правила г для каждой антицепи Е, не содержащей висячих вершин, причем если Е - антицепь, не содержащая висячих вершин, и Е С Mj, то существует элемент ХЕ Є MJ, для которого выполняется свойство реализации возможностей для анти цепи Е; (г) модель М опровергает правило г. Доказательство. Пусть правило г - не допустимо в логике JJ,. Тогда в силу теорем 3.3.3 [90], 3.3.6 [90] существует означивание переменных правила г, опро вергающее г во фрейме некоторой модели Ch n). По лемме 3.4.2 [90] существует означивание S переменных правила г, при котором правило г опровергается в модели СК(к). Построим модель М. следующим образом. Вначале определим модель max(Y) U S Ch k)). Пусть Z CY и где Y - множество всех подформул правила г. Таким образом, Hz - это множество элементов из Ch k), на которых истинны только формулы из Z. Определим теперь QHz следующим образом. где qm(Hz) - множество всех квазимаксимальных элементов из Hz (для подмножества А множества W элемент а є W будем называть квазимаксимальным в А, если а Є А и Vw Є W,w Є aR - w . А). Другими словами, QHz - это множество всех квазимаксимальных элементов глубины 1 модели Ch k), на которых выполняются формулы только из Z. Тогда подмножество max(Y) модели Ch (k) определим следующим образом. Множество max(Y) состоит из всех сгустков, содержащих элементы из множества (J QHz- Объединяя множество max(Y) и S Ch k)) и перенося отношение и означивание на построенное множество с модели Ch (k), получаем модель max(Y)\J Si(Ch (k)). Основное свойство построенной модели заключается в сохранении истинности формул из Y (см. лемма 3.4.6, [90]). По построению фрейм модели W = max{Y) U S Ch k)) адекватен логике \i. Рассмотрим следующий, заданный индуктивно р-морфизм модели W.

Сгустки вто ir рого слоя, имеющие одинаковое означивание и из которых достижимы одни и те же сгустки первого слоя модели УУ, склеиваем. Отметим, что во втором слое квазикомпоненты преобразованной модели W (так же как и во втором слое квазикомпоненты модели Скц(к)) содержится меньше 22 элементов. Продолжая, аналогичные сжатия в следующих слоях, получим /u-модель М. — (J.Mj) U Вм, где Mj - открытая подмодель М такая, что 3cjix Є MJ(XRCJ) и Вм - множество висячих вершин модели М. Пункт (а) выполняется по построению модели М. (б) Оценим мощность модели М. Вначале оценим мощность одной квазикомпоненты Qwi(M). Пусть в Sp(Qwi(M)) содержится не более, чем 7(р) сгустков. Тогда количество антицепей сгустков в Sp(Qwi(M)) не превышает числа 21 и, следовательно, (р + 1)-ой слой квазикомпоненты Qwi(M) содержит не более, чем 21 СГуСТКОВ. Ранее бЫЛО ОТМечеНО, ЧТО КОЛИЧесТВО СГуСТКОВ ВО ВТОрОМ СЛОЄ QlVi(M) не более, чем 22 , следовательно, 7(2) 22 . Таким образом, получаем следующие рекуррентные неравенства для оценки количества сгустков в (р+ 1)-ом слое квазикомпоненты Qwi(M): 7(1) = 1, 7(2) 22\ 7(Р+ 1) 27(р)- в Qwt(M) выберем цепь элементов L. Пусть Li,L2 Є L. Тогда по построению модели М имеем, что {ф\Ьі \VS ф,ф Є Y} ф {Ф\Ь2 \\ s Ф,Ф Є Y}, где Y - множество всех подформул правила г. И, следовательно, глубина Qwi(M) 1 + 2П, где п - число элементов во множестве Y. Следовательно, квазикомпонента Qwi(M) содержит не более, чем Г(п) = (1 + 7(2) + + 7(2n + 1)) сгустков. По определению квазикомпоненты имеем, что количество квазикомпонент не более, чем 22 . Тогда количество сгустков в модели М без учета висячих вершин не более, чем 22 Г(п). Оценим количество ВИСЯЧИХ ВерШИН В МОДеЛИ М. КОЛИЧесТВО ВИСЯЧИХ ВерШИН МОДеЛИ М, ВИДЯЩИХ І НЄ сравнимых сгустков первого слоя, не превышает С\к_ 2г г. Отсюда количество 22 -i . 2 _1 . 2 висячих вершин модели М не превышает ]Г С\к 2г(п) г (1 + 2Г("))22 -1. І-2 2 -1 В итоге получаем, что количество сгустков модели М не более, чем 22 Г(тг) + (1 +2Г("))2 -1. Утверждение (б) доказано. (в) Покажем, что модель W имеет свойство реализации возможностей для каждой антицепи Е, не содержащей висячих вершин. В силу задания логики ц модель Ch k) имеет следующее разложение Ch k) = (\_\ Hj) U Всь.й{к), где Hj - квазикомпонента модели Ch (k), Bch (k) - множество висячих вершин модели Chfj,(k). По построению модель W представима в виде W = (U K?) U Bw, где Wj С Hj и Wj - открытая подмодель W такая, что 3CJWX Є WJ(XRCJ), Вуч - множество висячих вершин модели М. Отметим, что нетривиальной будем называть антицепь, количество сгустков в которой больше 1. В случае, если антицепь Е является тривиальной, то, очевидно, что для любого ХЕ, принадлежащего сгустку Е, выполняется свойство реализации возможностей. Пусть Е является нетривиальной антицепью. Тогда по построению Chu,(k) антицепь Е обладает одноэлементным конакрытием {с} в модели Ch k), причем если Е С Hj, то с Є Hj. Рассмотрим два возможных случая: с є W, с . W. Если с Є W, то для с выполняется свойство И, следовательно, модель W имеет свойство реализации возможностей для данной антицепи Е, причем если Е с Wj, то с Є Wj. Если с $ W, то в силу построения модели W элемент с не является квазимаксимальным и, следовательно, существует элемент с Є QHz такой, что cRc и S(c ,Y) = S(c, Y). При этом если с Є Hj, то с Є Hj и с Є Wj. Отсюда в силу того, что с является одноэлементным конакрытием получаем, что с удовлетворяет определению 2.9 и модель W имеет свойство реали

Условие допустимости правил вывода в логике

Лемма 3.9. Пусть правило вывода г(х0)... ,Хк-і) в форме 7 опровергается при некотором формульном означивании S модальной степени I, I 0 на модели Chc(n). Тогда (а) на каждом элементе модели Chcin) при означивании S истинна одна фор мула и {, Ui Є Q(s/(r)), причем значение u ,- в произвольной точке а0 определяется значениями пропозициональных переменных pi,... ,рп на цепи (а0,... , а;) длины I; (б) если на некотором элементе модели Chc{n) при означивании S истинна фор мула Ui A Ou j, LL I,UJJ Є ft(sf(r)), то она принадлежит посылке правила г. Доказательство. Поскольку каждая о;,- является элементарной конъюнкцией всех переменных о,... ,Xk-i, то на каждом элементе истинно не более одной элементарной конъюнкции. А так как посылка правила sf(r) всюду истинна, то на каждом элементе истинна хотя бы одна элементарная конъюнкция о ,-. Таким образом, первая часть утверждения (а) справедлива. По условию доказываемой леммы имеем, что S - формульное означивание модальной степени I. То есть означивание S переменных xi, 0 і (к — 1), правила г определяется некоторыми формулами d(pi,... ,рп), 0 і (к — 1), модальной степени /. Поскольку Ші являются элементарными конъюнкциями переменных ХІ, то deg(LOi(Co(pi,... ,Рп),--- ,Cfc-i(Pi,--- ,Рп))) = /, Vwi Є Q,(sf{r)), и вторая часть утверждения (а) следует из леммы 3.4. (б) Пусть а0 - произвольный элемент модели Chc(n). Рассмотрим цепь (а0,аі). В силу пункта (а) на элементе ао при означивании S истинна только одна формула вида UiAOuj. Так как посылка правила sf(r) всюду истинна, то в каждой точке истинен хотя бы один дизъюнктивный член посылки правила sf(r). Отсюда получаем, что формула Ш( Л Dujj принадлежит посылке правила г. Утверждение (б) верно. Лемма доказана. Теорема 3.1. (Необходимое условие недопустимости правила вывода в логике С) Пусть правило вывода sf(r(xo,... ,Xk-i)) не допустимо в логике С. Тогда во фрейме G(r), порождённом правилом sf(r), существует цикл С = (uiq,uji,... ,u}q-i,coq) длины q (2m — 2), где т - число элементов фрейма G{r), удовлетворяющий условиям: 1) цикл С содержит элемент ut такой, что формула ut, 1 t q, входящая в посылку правила sf(r), содержит в качестве конъюнктивного члена формулу - х0, 2) элемент ид цикла С является рефлексивным, т.е. uiqR.GUq. Доказательство. Пусть правило вывода sf(r) от переменных яо,... ,Xk-i не допустимо в логике С Тогда из теоремы 1.9 и леммы 3.5 следует, что существует формульное означивание S переменных х0,... ,xk-i правила г, опровергающее данное правило на фрейме некоторой модели Chc(n) с означиванием V переменных pi,... іРп- Следовательно, заключение х0 правила г ложно при означивании S на некотором элементе а0 данной модели.

Рассмотрим цепь (a0,ai,... ,aq) модели Chjc(n), где элемент ач является максимальным элементом модели СкЛп). В силу пункта (а) леммы 3.9 на элементе a,j, 0 j q, модели Chc(n) при означивании S истинна только одна формула и , и Є Q(sf(r)), причем па элементе а0 истинна формула Ш{0, содержащая в качестве конъюнктивного члена - ж0. Пусть означивание S переменных а?,-, О і (к — 1), правила г определяется некоторыми формулами &(рі,... ,р„), 0 і (к — 1), и модальная степень означивания равна /. Так как каждая элементарная конъюнкция и ,- содержит все переменные х0,...,хк-1, то 1єд(ш ((о(рі,--- ,Рп), , (k-i(pi,--- ,Рп))) = I, Vwt- Є Q(sf(r)). Поскольку элемент aq является максимальным в модели Chc(n) и, следовательно, рефлексивным элементом, получаем, что Uiq = Д Пг7г, где 7г - некоторая элементар !=0 ная конъюнкция пропозициональных переменных р\,... ,рп, истинная на элементе ач. По построению модели Chc{n) существует цепь (&о, hi,... , Ь/) длины / такая, что і biRao и b0 IHv Л ,?г- Отсюда по лемме 3.4 имеем, что b0 \hs iq- В силу пункта (а) »=о леммы 3.9 получаем, что на элементах Ь0,Ь1уЬ2... , истинны, соответственно, некоторые формулы иія,и ,и ... ,Ujn принадлежащие Q(sf(r)). Таким образом, в модели Chc(n) цепь (b0,bi,... ,6/, a0,.. . ag_i,ag) длины (l+q+1) такова, что на элементах Ь0, &i, - - - ,bi,a0,ai,...aq-i,aq при означивании S истинны, соответственно, формулы Ш{ч,и ,... , UJ, , U{0, и ,... , ,- ,0 , причем формула wi0 содержит в качестве конъюнктивного члена — ого, элемент ад является рефлексивным. Следовательно, на элементах b0,bi... ,bi,a0,ai,...aq i,aq при означивании S истинны, соответственно, формулы Uig Л Dujlt Ujx Л DUJ2,. .. , UJ, Л Оиі0, Ui0 Л Па;,-П

Описание структурно-полных 5"4-логик ширины 2, порожденных конечным корневым фреймом с двухэлементным первым слоем

Лемма 4.4. Пусть F = (W, R) - конечный корневой \-фрейм ширины 2. Пусть А = {Аі,Л2}; В = {.01,.} - антицепи сгустков из F, обладающие конакрытиями. Тогда если BiRAi, AiRBi, A2RB2, B2RA2, то логика A = X(F) не является структурно-полной. Доказательство. Пусть А = {Лі,Л2}, В = {Ві,В2} - антицепи сгустков из F, обладающие конакрытиями (рис. 4.1). Предположим, что А является структурно-полной логикой. Предположим, что А2 имеет единственного непосредственного последовате I I ля D2 (возможно, что D2RB2&B2RD2). Отобразим все элементы сгустка Л2 в произвольный элемент сгустка D2. Заданное отображение / является р-морфизмом. Следовательно, полученный фрейм i x = /(F) является А-фреймом. По лемме 4.2 существуетр-морфизм #: Ch\(n) на F и в Ch\(n) существует открытый подфрейм F такой, что gi = g\p является изоморфизмом между F и F. Если X С F и gi(X) = Y, то множество X обозначим через У. Так как F\ - А-фрейм, то по построению Ch\(n) для сгустков А[ С F С Ch\{n) и D 2 С F С Ch\(n) существует конакрытие С. Так как g - р-морфизм Ch\(n) на F, причем D 2, А[ соответственно отображаются в D2, Лі, то для С не существует р-морфного образа во фрейме F, что противоречит структурной полноте логики А. Таким образом, получили, что Л2 является конакрытием для нетривиальной антицепи D = {Di, D2], где AiRDx, DiRAi. Теперь рассмотрим сгусток Bi. Предположим, что Вх имеет единственного непосредственного последователя Е\. Проводя вышеописанные рассуждения для сгустков В\, Ei, получим противоречие со структурной полнотой логики А. Поэтому сгусток Bi является конакрытием для нетривиальной антицепи Е = {Ei,E2}, где B2RE2, E2RB2. Итак, имеем антицепи D, Е, обладающие конакрытиями. Причем EiRAiRDi (возможно Ei совпадает с Ль но Di не совпадает с Ai), D2RB2RE2 (возможно D2 совпадает с В2, но Е2 не совпадает с В2). Получили, что антицепи D, Е удовлетворяют условию доказываемой леммы, причем сгустки Ах, В2 не являются максимальными. Повторяя рассуждения для D, Е, придем к выводу, что D\ и Е2 -не максимальные сгустки. Поскольку фрейм F - конечный, то через конечное число шагов придем к противоречию. Лемма доказана. Следствие 4.3. Пусть A = X(F) - структурно-полная логика ширины 2, F - конечный корневой Х-фрейм. Пусть Л = {А,С}, В = {В,С} - антицепи сгустков из F, обладающие конакрытием, и BRA, ARB. Тогда сгусток А является непосредственным последователем сгустка В. В Ф Доказательство. Пусть Л = {А,С}, В = {В,С} - антицепи сгустков из F, обладающие конакрытием (рис. 4.2). Предположим, что сгусток А не является непосредственным последователем сгустка В. Пусть сгусток В имеет единственного непосредственного последователя Q. Тогда отобразим все элементы сгустка В в произвольный элемент сгустка Q. Полученный фрейм Fi является р-морфным образом фрейма F и, следовательно, А-фрейм ом.

Пусть F , X, 7i имеют такое же значение, что и в доказательстве леммы 4.4. По построению Ch\(n) на сгустки С", Q из F существует конакрытие Y. Т.к. А структурно-полная логика, то в силу леммы 4.2 Ch\(n) р-морфно отображается на F. При этом сгустки С", Q Є F р-морфно отображаются на сгустки С, Q Є F, но тогда для конакрытия У Є Ch\{n) не существует р-морфного образа во фрейме F, что противоречит структурной полноте логики А. Таким образом, В имеет два непосредственных последователя -Qi, Q2. Отсюда получаем, что фрейм F содержит антицепи {Qi, Q2} и {А, С}, обладающие конакрытием и удовлетворяющие условию предыдущей леммы. Следовательно, логика Л не является структурно-полной. Полученное противоречие и доказывает утверждение. Лемма 4.5. Пусть A(F) - структурно-полная логика ширины 2, F - конечный корневой фрейм без узлов такой, что S7i(F) = 2. Тогда фрейм Si(F), являющийся собственным подфреймолі фрейма F, \/г удовлетворяет следующим условиям: (а) любой слой фрейма Si(F) состоит из двух сгустков; (б) для двух несравнимых сгустков из разных слоев фрейма Si(F) не существует конакрытия в F; (в) для любого слоя фрейма Si(F) существует коиакрытие в F. Доказательство проведем индукцией по параметру к множества Sk(F). Утверждение (а) для Si(F) выполняется по условию. Утверждение (б) для Si(F) выполняется тривиально. Покажем, что для Si(F) выполняется утверждение (в). Предположим, что для первого слоя F не существует конакрытия. В силу того, что F -конечный корневой А-фрейм, то всегда можно выбрать максимальный сгусток С, видящий весь первый слой фрейма F. Рассмотрим CR-. Сгустки первого слоя фрейма CR- обозначим А\ и Вх. Сгусток С отобразим в себя, сгустки, видящие Лі, отобразим в Лі, а сгустки, видящие Бь отобразим в В\. Полученный фрейм как р-морфный образ CR- является А-фреймом. Следовательно, на любую двухэлементную