Исследования допустимых правил в нестандартных логиках тема автореферата и диссертации по математике, 01.01.06 ВАК РФ

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

С-1 сч.'

БАБЕНЫШЕВ СЕРГЕЙ ВАЛЕРЬЕВИЧ

УДК 517.11

ИССЛЕДОВАНИЯ ДОПУСТИМЫХ ПРАВИЛ В НЕСТАНДАРТНЫХ ЛОГИКАХ

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

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук

Красноярск-1995

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

Научный руководитель доктор физико-математических наук,

профессор РЫБАКОВ В.В. Официальные оппоненты: доктор физико-математических наук,

профессор БУДКИН А.И. кандидат физико-математических наук,

МАРДАЕВ С.И.

Ведущая организация Иркутский государственный университет,

г. Иркутск

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

седании диссертационного совета Д.064.61.02 в Красноярском государственном университете по адресу 660041, г. Красноярск, пр. Свободный, 79.

С диссертацией можно ознакомиться в библиотеке Красноярского государственного университета.

WuMi 1996 г. в /LU часов на за-

ло

Автореферат разослан " 42. " с^МЛи

уМ

1996 г.

Ученый секретарь диссертационного совета

доктор физико-математических наук У\ Знаменский C.B.

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

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

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

Цель работы

1. разработать более общий подход к построению критериев допустимости правил вывода с метапеременными в модальных пропозициональных логиках, расширяющих логику Льюиса й4, применимый в случаях логик Б4.2 и 84.1.

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

3. исследовать разрешимость проблемы допустимости в наибольшем и наименьшем модальном напарниках КС — логиках 84.2Сгг и 84.2, а также проверить является ли 84.2 модальным напарником КС по допустимости.

4. с помощью разработанной техники исследовать проблему существования базиса допустимых правил вывода от конечного числа переменных в логиках 84.1, 84.2 и 84.20гг.

5. разработать алгоритм построения некоторых решений логических уравнений в модальных логиках 84.1, Э4.2 и 84.20гг.

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

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

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

Аппробация работы. Результаты диссертации докладывались на X всесоюзной конференции по математической логике (Алма-Ата, 1990), XI межреспубликанской конференции по математической логике (Казань, 1992 III международной конференции по алгебре памяти Каргаполова (Красноярск, 1993), международной конференции по математической логике посвященной 85-летию со дня рождения А.И. Мальцева (Новосибирск, 1994), русско-японском логическом коллоквиуме К8Ь'95 (Иркутск, 1995), а также

на заседаниях семинаров "Алгебра и логика" при Новосибирском государственном университете, семинара по неклассическим логикам при Институте математики СО РАН (Новосибирск) и на заседаниях Красноярского алгебраического семинара. ,

Публикации. По теме диссертации опубликовано 9 работ [5-13].

Структура и объем работы. Диссертация состоит из введения, трех глав, заключения и списка литературы из 77 наименований и занимает 99 страниц машинописного текста.

Много раз результаты и ход работы обсуждались с Владимиром Владимировичем Рыбаковым, которому я обязан также за поддержку и терпение. Я также благодарен Голованову М.И. и Безгачевой Ю.В. за полезные обсуждения на семинарах кафедры алгебры и математической логики Красноярского госуниверситета. Я обязан также Левчуку Владимиру Михайловичу за внимание и поддержку.

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

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

Напомним, что правило вывода

где переменные ... ,<¡7} выделены как метапеременные, называется допустимым в логике Л, если для любого набора формул 71,.. •, 7к'-

<*(71, • • •, 1к, ?1, • • •, ?() € А /?(71,..., 7^, ...,?()€ А.

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

ТЕОРЕМА 1.13. [Рыбаков В.В] (Критерий допустимости через п-характеристические модели) Пусть ТП(А), и £ Н, есть последовательность п-характеристических моделей для модальной логики А. Правило вывода г = а(рг, д^//3(Рг, 9.?) допустимо в А тогда и только тогда, когда для любого натурального п и любого формульного означивания ц переменных из г на фрейме ХП(А) такого, что /х(<7;) = двыполняется следующее:

(это значит, что г истинно на1п(Л) относительно формульных означиваний).

2. Во второй главе изложены основные результаты, относящиеся к построению семантических и алгоритмических критериев допустимости в модальных логиках 84.1, 84.2, 84.20гг и суперинтуиционистской логике КС.

В разделе 1 вводится и обсуждается ключевое понятие этой главы — понятие схемы деления для множества формул:

ОПРЕДЕЛЕНИЕ 2.1. Модель 21 = (Л, Я, <р) называется схемой деления с наборами параметров N С Т{Р{Р{Ф))) для множества формул Ф с параметрами Р(Ф) С ^(Ф), если выполнены следующие условия:

1. модель есть конечная рефлексивная, транзитивная модель Крипке, причем с1от(<р) ~Э У(Ф);

2. для любых элементов х и у модели 21:

х — у {а в Ф | х II- а} = {а 6 Ф | у 1Н а};

3. для любых элементов хну людели 21;

хИу (уа е Ф)(у 1Ь Оа х 1Ь Оа);

4■ для любой антицепи элементов V С 21 и множества С £ N существуют множество элементов

С^ = | « £ С} С 21, г<?е а^ 1Ь ? £ и, такое, что:

a) (V* £ Су)(Уа £ Ф)(г II- Оа (Зг/ £ Су)(г/ а) V (Зу £ У)(у II" Оа));

b) (V гбСу)(УуеУ)(а:Ду).

Понятие схемы деления является развитием идеи моделей из [1,7], строящихся по правилу вывода, более того она обобщает их на случай правил вывода с метапеременными. Использование множества формул, не связанного жестко с правилом вывода, позволяет более гибко использовать схемы деления для доказательства алгоритмических критериев допустимости. Доказывается основная теорема раздела 1 — теорема о распространении означивания, характеризующая главное свойство схемы деления:

ТЕОРЕМА 2.2. (О распространении означивания) Пусть

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

2. {В — схема деления с наборами параметров N С Р('Р(Р{Ф))) для конечного множества формул Ф с множеством параметров Р(Ф),

3. 03 < 21 и 023 = 21 и все элементы 25 формульны в 21,

4. для любого сгустка С модели 21

{{<г£Р(Ф) | 21, я 11-9} |г£С}£УУ.

Тогда, если <р есть означивание модели 21, то существует означивание V, формульное в 21, такое, что

1. для любого д £ Р(Ф): и(д) = <р(д),

2. для любого а 6 Ф: 21, V II" а 93 1Ь а.

Теорема о распространении означивания является обобщением теоремы достаточности из [7] на случай правил вывода с метапеременными. Случай редуцированных форм правил вывода несколько упрощает доказательство.

В разделе 2 доказываются необходимые условия допустимости правил вывода в исследуемых модальных логиках, сводящие недопустимость к существованию для правила вывода схемы деления со специальными свойствами — схемы опровержения. Приведем, для примера, определение схемы опровержения для правила вывода с метапеременными в логике 84.1:

ОПРЕДЕЛЕНИЕ 2.7. Модель 21 называется схемой опровержения в логике Б^Л для правила вывода г = а//? с метапеременными Р(г), если выполнены следующие условия:

1. модель 21 есть схема деления с наборами параметров Т(Р(г)) для множества формул БиЬ({а, (3}) и {ри \ и 6 ^(^(г))} с метапеременными Р(г);

2. модель 21 вкладывается как открытая подмодель в п-характеристи-ческую модель 1П(84.1) логики где п = ^(г)! и 021 = 1„(84.1).

Ключевое свойство схем опровержения формулируется в:

ТЕОРЕМА 2.10. Если правило вывода г с параметрами не допустимо в логике А € {84.1,84.2,84.2Сгг}, то существует схема опровержения для г в логике А с тем же множеством параметров.

В доказательстве этой теоремы используются подходы, разработанные первоначально для доказательства полноты по Крипке [4].

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

логик 84.1, Б4.2 и Б4.2Сг2. Там же рассматриваются примеры применения полученных критериев к исследованию допустимости конкретных правил вывода и построению решений логических уравнений *

Следующая теорема является аналогом семантического критерия из [1]:

ТЕОРЕМА 2.12. (Семантический критерий допустимости) Правило вывода г = а/0 с метапеременными Р(г) допустимо в логике Л € {84.1, 84.2, 84.20гг} тогда и только тогда, когда для любой п-характери-стической модели Т„(А) и для любого означивания на ТП(А), сохраняющего истинность параметров на элементах:

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

ТЕОРЕМА 2.13. (Алгоритмический критерий допустимости) Правило вывода г с метапеременными допустимо в логике А (А=84.1, 84.2 или 84.2Сгг) тогда и только тогда, когда не существует схемы опровержения для г в логике А.

Построенные критерии дают также алгоритм конструирования опровергающей подстановки для правила вывода, которое не является допустимым, и поэтому критерии дают возможность построения решений логических уравнений в указанных логиках. Алгоритмические критерии позволяют заключить, что проблемы допустимости правил вывода с метапеременными в модальных пропозициональных логиках 84.1, Э4.2 и 84.2Сгг, и,

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

ЗАМЕЧАНИЕ. Нетрудно видеть, что проблема разрешимости по допустимости для исследуемых модальных логик N Р-полна. Поэтому семантический критерий часто оказывается даже более удобным для построения конкретных примеров не допустимых правил вывода, чем алгоритмический, хотя и требует, в нашем случае, работы с бесконечными га-характеристическими моделями.

Сформулированные выше результаты имеют алгебраические аналоги: а именно, получено, что квазиэквациональные теории свободных алгебр Зи,(84.2), 3^(84.20^) и ^(Б4.1) разрешимы. Для 84.1 можно усилить этот результат: имеем, что универсальная теория свободной алгебры $ш(84.1) разрешима.

В разделе 5 рассматриваются логики Э4.2 и 84.2Сгг, являющиеся, соответственно, наименьшим и наибольшим модальным напарником КС, и доказывается, что 84.2 сохраняет допустимость правил вывода при геделе-вом переводе этих правил.

3. Глава 3 посвящена применению полученных критериев допустимости для логик 84.1, Э4.2 и 84.20гг к исследованию теорий допустимых правил вывода этих логик, в частности, к вопросу о существовании конечного базиса допустимых правил. В разделе 1 изложены предварительные результаты по вопросу о существовании базиса допустимых правил вывода от конечного числа переменных, приведен, с доказательством, критерий сущес-

твования базиса квазитождеств от конечного числа переменных для произвольного квазимногообразия. Описываются квазиэквациональные теории свободной алгебры счетного ранга многообразий, порожденных логиками Б4.2 и 84.2Сгг.

ЛЕММА 3.1. Пусть А одна из логик 84.1, Э4.2 или 84.2Сгг. Тогда квазиэквациональные теории классов алгебр

ША): пёМ} и{Т+(А) : п € 1С}

совпадают.

Раздел 2 описывает последовательность моделей Крипке Е„ со специальными свойствами, которая будет применяться для доказательства отсутствия базиса допустимых правил вывода.

ТЕОРЕМА 3.3. Все п-порожденные подалгебры алгебры Еп входят в квазимногообразие, порожденное свободной алгеброй$Ш{БА.2) ($ш{54.2Сгг))

Доказательство теоремы 3.3. использует двойственность между р-морф-ными образами фреймов Крипке и подалгебрами модальных алгебр.

Хорошим примером применения результатов второй главы служит:

ТЕОРЕМА 3.4. При п> 2 справедливо:

4.2)), Д+ 0?(&,(84.2Си)).

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

В разделе 3 доказывается, что существование последовательности моделей Крипке из раздела 2 противоречит, согласно критерию, существованию базисов квазитождеств от конечного числа переменных квазиэквациональ-ных теорий свободных алгебр многообразий, порожденных логиками 84.1, Б4.2 и 84.2Сгг. В виде следствий формулируются аналогичные результаты для теорий допустимых правил вывода этих логик.

ТЕОРЕМА 3.5. Квазимногообразия, порожденные свободными ал-гебралш За,(84.1), Зш(84.2) и &Д84.20гг), не имеет базиса квазитождеств от конечного числа переменных.

Ввиду отмеченной в [2,3] взаимосвязи базиса квазитождеств и базиса допустимых правил, справедлива

ТЕОРЕМА 3.6. Не существует базиса допустимых правил логик 84.1, 84.2 и 84.2вг2 от фиксированного конечного числа переменных. В частности, логики 84.1, 84.2 и 84.2Сгг не имеют конечного базиса допустимых правил.

Алгебраические аналоги этих результатов формулируются так: отсутствуют базисы квазитождеств от конечного числа переменных квазиэква-циональных теорий свободных алгебр &,(84.2) и (^ш(84.2Сгг), в частности, не существует конечного базиса квазитождеств этих квазиэквациональных теорий.

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

ОСНОВНЫЕ РЕЗУЛЬТАТЫ

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

1. Получен семантический критерий допустимости правил вывода с ме-тапеременными в логиках 84.1, 84.2 и 84.2Сгг через истинность на фреймах п-характеристических моделей.

2. Доказана разрешимость проблемы допустимости правил вывода с ме-тапеременными в модальных пропозициональных логиках 84.1, 84.2 и Б4.2Сгг. Доказана разрешимость квазиэквациональных теорий свободных алгебр Зы(84.1), &,(84.2) и За,(84.2Сгг).

3. Доказано отсутствие базиса допустимых правил вывода от конечного числа переменных в логиках S4.1, S4.2 и S4.2Grz. В частности не существует конечного базиса допустимых правил вывода в этих логиках.

4. Логики S4.2 и S4.2Grz являются модальными напарниками по допустимости суперинтуиционистской логики слабого закона исключенного третьего — логики КС.

5. Доказана разрешимость проблемы допустимости правил вывода с параметрами в суперинтуиционистской логике КС.

ЛИТЕРАТУРА

1. Рыбаков В.В. Критерий допустимости правил в модальной системе з4 и интуиционистской логике // Алгебра и логика. 1984. Т. 23. №5. С. 346-572.

2. Рыбаков В.В. Базисы допустимых правил логик S4 и Int // Алгебра л логика. 1985. Т. 24. № 1. С. 87-107.

3. Циткин А.И. О допустимых правилах интуиционистской логики вы-жазываний // Математический сборник. 1977. Т. 102. №2. С. 314-323.

4. Fine К. Logics containing К4. Part II // Journal of Symbolic Logic. L985. V. 50. №3. P. 619-651.

РАБОТЫ АВТОРА ПО ТЕМЕ ДИССЕРТАЦИИ

5. Бабенышев C.B. Разрешимость проблемы допустимости правил вы-зода в модальной логике S4.2 // Материалы XXIX всесоюзной научной :туденческой конференции. Математика. Новосиб. ун-т. Новосибирск, L991. С. 3-6.

6. Бабенышев С.В. Отсутствие конечного базиса допустимых правил вывода в модальных логиках S4.2 и S4.2Grz // Материалы XXX международной научной студенческой конференции. Математика. Новосиб. ун-т. Новосибирск, 1992. С. 6-9.

7. Бабенышев С.В. Разрешимость проблемы допустимости правил вывода в модальных логиках S4.2 и S4.2Grz и суперинтуиционистской логике КС // Алгебра и логика. 1992. Т. 31. №4. С. 341-359.

8. Бабенышев С.В. Базисы допустимых правил вывода модальных логик S4.2 и S4.2Grz // Алгебра и логика. 1993. Т. 32. №2. С. 117-130.

9. Бабенышев С.В. Допустимые правила вывода модальных логик S4.2, S4.2Grz и интуиционистской логики КС //XI межреспубликанская конференция по математической логике: Тез. сообщений. Казанский ун-т. — Казань, 1992. С. 9.

10. Бабенышев С.В. Критерий допустимости правил вывода с параметрами в суперинтуиционистской логике КС // Международная конференция по математической логике:' Тез. сообщений. Новосиб. ун-т. — Новосибирск, 1994. С. 14-16.

11. Бабенышев С.В. Квазиэквациональные теории квазимногообразий, соответствующих модальным логикам S4.2 и S4.2Grz // III международная конференция по алгебре: Тез. докл. Красноярский ун-т. — Красноярск, 1993. С. 25.

12. Babyonyshev S.V. Basis of admissible rules with finite number of variables for logic КС does not exist // NSL'95: Abstracts. University of Irkutsk. — Irkutsk, 1995. P. 94. На англ. яз.

13. Babyonyshev S.V. Admissibility of inference rules in modal logics S4.1 and S4.2 // Logic Colloqium'95: Abstracts. Technion Israel Institute of Technolo; University of Haifa. —Haifa, 1995. PROOF-39. На англ. яз.