Правила вывода многомодальных логик

Кошелева, Анна Владимировна

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

Кошелева, Анна Владимировна АВТОР

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

Красноярск МЕСТО ЗАЩИТЫ

2007 ГОД ЗАЩИТЫ

01.01.06 КОД ВАК РФ

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

Автореферат диссертации на тему "Правила вывода многомодальных логик"

на правах рукописи УДК 510 64

Кошелева Анна Владимировна

Правила вывода многомодальных логик

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

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

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

ш®!!1!ш

Работа выполнена в Институте естественных и гуманитарных наук Сибирского федерального университета

Научный руководитель Официальные оппоненты

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

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

профессор В В Рыбаков

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

профессор А.Д. Яшин

кандидат физико-математических наук,

доцент В В Римацкий

Институт математики имени

С.Л. Соболева СО РАН. г. Новосибирск

Защита состоится 10 ноября 2007 г в 14 часов на заседании диссертационного совета Д-212 099 02 в Институте естественных и гуманитарных наук Сибирского федерального университета по адресу 660041, г Красноярск, пр Свободный, 79

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

Автореферат разослан ()/(/Н С>/1 (Я 2007 г

Ученый секретарь диссертационного совета, кандидат физико-математических наук, ^ ^ -/Голованов М И доцент

Общая характеристика работы

Актуальность темы. В диссертации исследуются на разрешимость по допустимости правил вывода некоторые многомодальные логики, расширяющие Sbt, t G N, a также линейные логики LinT и Lin DA, и для исследуемых логик будут построены алгоритмические критерии определения допустимости правил вывода Правило вывода — это правило, регламентирующее допустимые способы перехода от некоторой совокупности формул aj, ,ап, называемых посылками, к некоторой определенной формуле ß, называемой заключением Правило вывода называется истинным в логике Л, если из того, что , , ап G Л следует, что ß G А, называется выводимым (или доказуемым) в Л, если ß выводится из посылок с помощью аксиом и постулированных правил логики Л, и допустимым в Л, если при любой подстановке е, из а\ 6 Л, , аЕп е А следует, что ße € Л. Допустимые правила вывода — это наибольший класс правил, которые мы можем использовать в выводах данной логики Л, сохраняя множество ее доказуемых формул, т е с помощью таких правил мы не получим формул, которые не являются теоремами логики Л Так как в аксиоматике логик постулированных правил немного, то использование допустимых правил позволяет сокращать и упрощать процесс доказательства. Например, в исчислении высказываний (ИВ) и исчислении предикатов ничуть не реже, чем постулированное правило modus ponens а, а —> ß /ß, используется правило а —> ß, ß —> /а Но в ИВ все допустимые правила доказуемы, а в логиках первого порядка, модальных и суперинтуиционистских логиках существуют допустимые, но не доказуемые правила вывода, и впервые это было замечено для интуиционистского исчисления H (примерно в 50-х годах прошлого века в разных работах) Определение допустимого правила появилось в работе П Лоренцена [23] в 1955 году П Харроп в работе [21] за 1960 г показал, что в H допустимо, но не доказуемо правило -1 х —» (у V z) / (-1 х —» у) V (-1 х —> z) Г Е Минц в [6] доказал, что

если правило г допустимо в Н и не содержит связок —> или V, то г выводимо в Н, и показал, что правило ((х —> у) —* (х V у)) / (((ж —> у) —* х) V ((х —у у) —> г))) допустимо, но не выводимо в Я В модальных логиках 54, 54 1, Сгг допустимо, но не выводимо правило Леммона-Скотта □ (□ (ОООр -» Ор) {ар V □ -I Пр) / ПО ар V □ -1 Пр.

Логики, в которых все допустимые правила доказуемы, называются структурно-полными. Такими логиками являются, к примеру, ИВ и модальная логика 54 3С?г;г Модальные логики К, Т, К4, 54, 55 не являются структурно-полными В этих логиках допустимо, но не доказуемо правило О -¡ж Л Ох /у. Структурной полнотой суперинтуиционистских логик занимались А И. Циткин [18], Т Прукнал [24], а структурную полноту модальных логик исследовали В Джиобяк [19], В В Рыбаков [26]

хофф [22] и В В Рыбакова [27] были построены бесконечные базисы для логик Н и 54 соответственно. А Н Руцким был построен бесконечный явный базис для логики К4 [8], а В. Р Федоришиным для логики <?£ [17]. Разрешимость по допустимости логик 54 2, КС и отсутствие у этих логик конечного базиса было доказано С В Бабены-шевым в [1], [2] Ю. В Безгачева доказала, что транзитивные конечно-аксиоматизируемые и финитно-аппроксимируемые логики ширины 2 разрешимы по допустимости [3], а В В Римацким было доказано, что модальные финитно-аппроксимируемые логики ширины 2 имеют конечный базис допустимых правил [7] Большое значение для решения задач, связанных с допустимостью правил, имела возможность представления свободных алгебр из многообразия модальных алгебр данной логики специальными моделями Крипке {являющимися реляционными) — п-характеристическими моделями В [26] получен также критерий, при котором логика первого порядка разрешима относительно допустимости правил вывода Такими логиками оказываются только логики, порожденные конечной моделью.

Наряду с обычными правилами рассматриваются также правила вывода с метапеременными, или, как еще говорят, с параметрами Причиной изучения таких правил стали проблемы подстановки и разрешимости логических уравнений, и проблема разрешимости уравнений в свободных алгебрах, соответствующих некоторой алгебраической логике Сформулируем, например, вопрос о подстановке для заданной логики А существует ли алгоритм, который для произвольной формулы а(Ръ 41, ,<й)> где 31, ,<й — это метапвременные, определяет,

найдутся ли такие формулы /Зь , /?п, что а (01, .,/Зп, , ©) 6 А? Разрешимость проблемы подстановки для Н была доказана В, В Рыбаковым в работе [15] за 1990 год Он доказал также разрешимость по допустимости правил вывода с метапеременными большого класса суперинтуиционистских и транзитивных модальных логик [26, 13, 14, 15]

К этому классу принадлежат К4, КАЛ, К4.2, К4.3, 54, 54 1, 54.2, 54 3, Огг, От г 2, Сгг 3, ОЬ, Н, КС, ЬС В Р. Кияткиным доказано, что все предтабличные логики, расширяюхцие 54, и все конечно-аксиоматизируемые логики конечной глубины, разрешимы по допустимости правил вывода с метапеременными [5].

К настоящему времени существует глубоко развитая теория допустимых правил для транзитивных одномодальных логик, однако в нетранзитивных и многомодальных логиках кажется с пшиком сложным построить алгоритмы определения допустимости правил для достаточно широкого класса таких логик Допустимости правил в нетранзитивных логиках посвящены, к примеру, работа М И Голованова и Е М Юрасовой [4], в которой доказана разрешимость по допустимости для нетранзитивной одномодальной логики с оператором «завтра», и Рыбакова [28], а допустимости в многомодальных логиках — работы [29, 30, 32, 33]

Одним из условий существования алгоритмов в [26] является обычная разрешимость логики и ее финитная аппроксимируемость И в нашем случае алгоритмические критерии будут доказаны только для логик, обладающих этими двумя свойствами Несмотря на то, что все расширения логики 55 финитно-аппроксимируемы, уже среди расширений логики 55з встречаются не финитно-аппроксимируемые логики, [20] Но хотя обычно алгоритмы определения допустимости правил вывода строились для финитно-аппроксимируемых логик, в [29] Рыбаковым В В был построен алгоритм определения допустимости правил для двух не финитно-аппроксимируемых логик, это логики, порожденные фреймами (г, >, <), (и, >, <)

Цель работы.

1) Исследовать разрешимость проблемы допустимости правил вывода в логиках 55(Сь I < Ь, и 5547, где 554(7;, I < t — это логика с

дополнительными к аксиоматике S5t аксиомами апП32 ■ алР п*2 • • °itP,

Vil, -,,3i, il, ■ 1, ,t},l <t,]k^3s, ik is при к ji

s, a Sbt-J получена добавлением к S5t аксиом □ tp —» □ гр, г = 1,. , t.

2) Исследовать на разрешимость по допустимости правил вывода линейные логики Ьгп Т и Lin DA.

3) Пусть S5tC't — это логика SbtCt плюс аксиомы

{Рп = ~" Л о*(р*Л Д ке{1,. .,«}

Выяснить, является ли эта логика логика табличной.

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

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

Основные результаты. В диссертации получены следующие основные результаты

1) Доказана разрешимость по допустимости правил вывода финитно-аппроксимируемых и разрешимых логик, расширяющих S5tCt

2) Доказана разрешимость по допустимости правил вывода линейных финитно-аппроксимируемых и разрешимых логик, расширяющих LmDA

3) Доказано, что логика S5tC" является табличной, и ее наибольшие конечные корневые фреймы содержат не более пг элементов

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

Апробация работы. Результаты диссертации докладывались на

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

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

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

Публикации. По теме диссертации опубликовано пять работ [31]-

[35]

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

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

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

Вторая глава посвящена исследованию разрешимости проблемы допустимости правил вывода в некоторых логиках, расширяющих ¿бЯ,и обозначенных автором как 55¿Сг, / < £, и 55е3

В параграфе 2.1 вводится аксиоматика логик Б^Си £ < ¿, и 55<7 554-логику с дополнительными (к аксиоматике 55{) аксиомами

^'Л, .Л, Я. ,4 € {1, ,<}, I < г, Зк ф За, гк Ф гв при к ф з, назовем ¿>5<С(, а 55{-логику с дополнительными аксиомами

П*Р Огр, г = 1, ,4,

назовем 55{ J

В параграфе 2 2 доказывается финитная аппроксимируемость изучаемых логик Сначала доказывается

Лемма 2.6 Пусть М. — корневая БЪ^модель, адекватная логике 5'5{С;, I < I Тогда справедливы следующие утверждения

а)\/аеМ,Уг1, ,г; е {1, ,£}, г, ф %к при ] ф к а II- СЗП Ог2 аг, а =Ф- М II- а,

б)еслиЗа€М а\Ь а, тоУгх,. € {1, г^ Ф гьпри] Ф к, М 1ЬОг1Ог2 Ог;а

В этой лемме утверждаются важнейшие свойства исследуемых логик

С помощью этой леммы, а также следующей теоремы и предложения

Теорема 2.3. Формула

алпй • 1°г2 ■ °»пР> е {1. ,«}, в,т,пе N (1)

истинна на фрейме тогда и только тогда, когда он удовлетворяет, условию:

УхУуи . , Уп (х Лгх У1 А У1 Яг? У2 А -Л Уп-1 Дг„ Уп (2)

Зг1,...,гт(хЯнг1 Л гхК^яг Л -Л 2т_х Л гт = ?/«)).

Предложение 2.5. 1) Фрейм канонической модели Свьл удовлетворяет условию

2) Фрейм канонической модели Сз^с^ удовлетворяет условию

ЧхУу{хНъУхП3у), Уг, э е {1, .,*}

Отношения йх, на фреймах канонических моделей Сз^Сч

I < I, Сяьл являются рефлексивными, транзитивными и симметричными

доказывается

Теорема 2.9. Логики 55¿Сг, ? < 55^ финитно-аппроксимируемы

Из этой теоремы и конечной аксиоматизируемости исследуемых логик получаем следующую теорему

Теорема 2.10. Логики 55¿С;, ? < £, 5547 разрешимы

В параграфе 2.4 будет доказана разрешимость по допустимости правил вывода финитно-аппроксимируемых и разрешимых логик А Э 56464, откуда в силу предложения

Предложение 2.2. 1) Логика 55*Сг является расширением логики 554С„, I <п<Ь.

2) 55*7 является расширением 55¿С*

будет следовать и разрешимость по допустимости правил вывода логик БЬгСи 1<Ъ и 55(7.

Используя лемму 2 6 мы докажем, что верна

Лемма 2.15. Пусть А — финитно-аппроксимируемая логика и А 2 БЪгСг, Л — корневая подмодель модели СН\(п), и все элементы в Л имеют разное означивание Тогда любой элемент подмодели Л будет формулъно определимым в СЬ,\(п).

С помощью этого результата, леммы 2.6 и следующих двух лемм-

Лемма 2.13. Если С^ .. а . . ,рп) ¡3 (рх, ,рп) € А Э в^Сг, то правило

г — 9 (Р1>-1Ёл1 допустимо в А

/?(Рь ,Рп)

Лемма 2.14. Пусть А 2 ¿>5« и дано правило г = " >Рп), Если

Р{Ри ,Рп)

формула а (рг, . ,рп) опровергается при всех означиваниях п переменных одноэлементного рефлексивного фрейма, то г допустимо в А

мы получаем алгоритмический критерий определения допустимости правила г = д -Щ в финитно-аппроксимируемой и разрешимой

Р{Р1, • ,Рп) логике А 2 БЬ&г

Теорема 2.16. 1) Правило г •— ' допустимо в финитно-

Р(ри -,Рп)

аппроксимируемой и разрешимой логике А 2 тогда и только то-

гда, когда или а) а опровергается на любой одноэлементной корневой подмодели модели СН\(п) или б) п4а —»/3 е А

2) Условия а) и б) алгоритмически распознаваемы, и, следовательно, логика А разрешима по допустимости правил вывода

который применим и к исследуемым логикам 554 Си I < и 55(«7

В параграфе 2 4 будут приведены некоторые необходимые и достаточные условия разрешимости по допустимости правил с метаперемен-ными в логиках 55^;, I < S5tJ, но алгоритмический критерий разрешимости по допустимости правил вывода с метапеременными найден не будет

В параграфе 2.5 доказывается структурная неполнота логик З^С;, I < Ь, и БЪ^, а также теорема

Теорема 2.20. Пусть дано правило вывода г = —<:>хХ ^1

и пусть А — финитно-аппроксимируемая и разрешимая логика, расширяющая Если г истинно на корневой и адекватной для этой логики модели ЛЛ с областью означивания V, то на Л4 истинно любое допустимое в А правило с переменными из Оот(У)

В работе [29] В В Рыбаковым было доказано, что логики, порожденные фреймами >, <}, {/V, >, <) разрешимы по допустимости В третьей главе будет доказано, что линейные логики ЬгпТ — {<5, >, <) и ЬгпВА = (<3, >, <} также разрешимы по допустимости правил вывода (Теорема 3.7)

В червертой главе в параграфе 4 1 вводятся две логики и

5'54С'™2 и исследуются их конечные фреймы 5'54С" — это логика плюс аксиомы

¥>*=-■ Д <>к(Р.Л Д -прД Ае{1, л)

1<г<п+1 1<]ф1<п+1

Несложно проверяется, что на конечных фреймах, адекватных логике 5'5 формула истинна тогда и только, когда все сгустки по отношению Н}. содержат не более п элементов А 55* С? 2 ~ это логика 55(С™ плюс аксиомы Рг □ Зр —* Огр, Уг, ] € {1, В результате получена

Теорема 4.2. Наибольший (по числу элементов) конечный корневой

фрейм, адекватный логике Й^С™, содержит не боже п1 элементов, а для логики совпадает с фреймом Т™

Где Т™ — фрейм специального вида, построенный в той же главе

В теореме 4 1 доказывается, что

Теорема 4.1. Логика БЬьС" финитно-аппроксимируема

Тогда из теорем 4 1 и 4 2 следует

Теорема 4.3. Логика й^С™ является табличной

Для логики БЪгС^ 2 также верна

Теорема 4.5. Все конечные корневые фреймы логики ,55¿С',2 2 являются р-морфными образами фрейма

Приведен пример, показывающий, что для логик БЬ± С™ а с большим объемом сгустка уже не всегда конечный корневой фрейм является р-морфным образом фрейма Т™

В параграфе 4 2 строится конечная булева алгебра с 2* элементами Ее элементы представляют собой конечные кортежи (ку, , А;4), где кг — это 0 или 1, а операции -I, —», определены на кортежах стандартным образом покомпонентно Кроме стандартных операций, на этой алгебре задается оператор /», г € {1, ,£} /г (кг, . ,кь) = (пч, ,т() кг Ф тг и Ч] ф г, к0 — т3

Далее определяется логика Л в языке алгебры Задаются аксиомы и правила вывода этой логики

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

Предложение 4.7. Всякая теорема логики Л является тождественно истинной на алгебре Вг.

Лемма 4.9. (Теорема о полноте ) Если формула а логики А является тождественно истинной, то она является теоремой логики Л.

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

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

Список литературы

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

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

[3] БЕЗГАЧЕВА Ю В Допустимость правил вывода в логиках ширины 2 //Деп ВИНИТИ -27 07.98 - №2377-В98

[4] Голованов М И , Юрасова Е М. Критерий допустимости правил вывода логики с оператором «Завтра» // Красноярск, Краен университет - 2004 - Деп в ВИНИТИ - 22 10 04 - Ш654-В2004

[5] Кияткин В Р Правила вывода с метапеременными и логические уравнения в табличных и предтабличных локально конечных модальных логиках // Красноярск, Краен университет - 1995 -Деп в ВИНИТИ - 15 12 95 - №3350-В95

[6] Минц Г Е. Производность допустимых правил. // Записки научного семинара ЛОМИ АН СССР. - 1972 - №32 - С 85-99

[7] РимацкиЙ В В О конечной базируемости допустимых правил вывода модальных логик ширины 2 // Алгебра и логика - 1999 -Т38 - №4 - С 436-455

[8] РУЦКИЙ А Н Явный базис для правил вывода, допустимых в модальной системе К А //Красноярск, Краен университет - 2002. - Деп в ВИНИТИ - 11 11 2002 - Ж939-В2002

[9] Рыбаков В В Допустимые правила предтабличных модальных логик // Алгебра и логика - 1981 - Т 20 - №4 - С 440-464

[10] Рыбаков В В Критерий допустимости правил в модальной системе 54 и интуиционистской логике // Алгебра и логика - 1984 -Т23 -JV«5 - С 546-572

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

[12] Рыбаков В В Разрешимость по допустимости модальной системы Grz и интуиционистской логики // Известия АН СССР Сер математическая. - 1986 - Т50 - №3 - С 598-616

[13] Рыбаков В В Уравнения в свободной топобулевой алгебре // Алгебра и логика - 1986 - Т 25 - №2 - С 172-204

[14] Рыбаков В В Уравнения в свободной топобулевой алгебре и проблема подстановки. // Доклады АН СССР - 1986 - Т287 -№3 - С 554-557

[15] Рыбаков В В Критерии допустимости правил вывода с параметрами в интуиционистской пропозициональной логике // Известия АН СССР Сер математическая -1990 -Т.54 -№6 -С 1331-1341

[16] Рыбаков В В Разрешимость логических уравнений в модальной системе Grz и интуиционистской логике. // Сибирский математический журнал -1991 -Т32 - №2 - С 140-153

[17] Федоришин В Р Явный базис для допустимых правил вывода логики Геделя-Леба GL // Красноярск, Краен университет -2002 - Деп в ВИНИТИ - 11 11 2002 - №1938-В2002

[18] Циткин А. И О структурной полноте суперинтуиционистских логик // Доклады АН СССР - 1978 - Т 241 - №1 - С 40-43

[19] Dziobiak W Structural completeness of modal logics containing K4. // Bulletin of the Section of Logic - 1983. - V 12 - №1 - P 32-36

[20] Gabbay D M , Kurucz A , Wolter F , Zakharyaschev M Many-dimensional modal logics- theory and applications // Studies in Logic and Foundations of Mathematics, Elseiver Sci Publ., North-Holland. - 2003 - V 148 - 768 p

[21] HARROP R Concerning formulas of the types A В V С, A —> 3 xB(x) in mtuitionistic formal system // Journal of Symbolic Logic -1960 -V.25 - №1 -P 27-32

[22] Iemhoff R. On the admissible rules of mtuitionistic prepositional logic //Journal of Symbolic Logic.-2001.-V.66 - №2 -P 402-428

[23] Lorenzen P Einfung in Operative Logik und Mathmatik. // Berlin

- Gottmgen - Heidelberg - 1955 - 412 p

[24] PruCNAL T Structural completeness of some fragments of intermediate logics. //' Bulletin of the Section of Logic. - 1983. - V.12.

- №1 - Р18-21

[25] Rybakov V V Rules of inference with parameters for mtuitionistic logic // Journal of Symbolic Logic - 1992 - V.57 - № - P 912-923

[26] Rybakov V V. Admissibility of logical inference rules // Studies in Logic and Foundations of Mathematics, Elseiver Sci Publ, North-

• Holland - New-York - Amsterdam - 1997 - V 136 - 617 p

[27] Rybakov V. V Construction of an explicit basis for rules admissible m modal system SA / / Mathematical Logic Quarterly - 2001 - V.47 - Ш. - P.441-446

[28] Rybakov V V. Logical consecutions in intransitive temporal linear logic of finite intervals // Journal of Logic Computation. - 2005 -

V 15 -№5 -P 663-678.

[29] Rybakov V. V Logical consecutions discrete linear temporal logic // Journal of Symbolic Logic - 2005 - V 70 - №4 - P 1137-1149.

[30] Rybakov V V Logics with universal modality and admissible consecutions // Journal of Applied Non-Classical Logics. - 2007 -

V 17 - №3 - P 381-394

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

[31] Кошелева А В. Разрешимость проблемы допустимости правил вывода в некоторых S5t-логиках. // Материалы международной конференции, посвященной 75-летию со дня рождения профессора А И Кокорина «Алгебра, логики и кибернетика». - С 163.

[32] Golovanov М I., Kosheleva А. V , Rybakov V V Logic of visibility, perception, and knowledge, and admissible inference rules // Logic Journal of IGPL - 2005 - V 13. - №2 - P 201-209

[33] Кошелева А В. Разрешимость проблемы допустимости правил вывода в некоторых ¿¡^-логиках // Алгебра и логика - 2005 -Т.44 - №4 - С 438-458.

[34] Кошелева А В. Разрешимость по допустимости правил вывода некоторых линейных логик // Вестник КрасГу - Красноярск, КрасГУ - 2006 - Сер Физ -Мат науки, Вып 9 - С 59-63

[35] Кошелева А В Логика в^Сь с ограниченным объемом сгустков // Препринт №6 - Красноярск ИВМ СО РАН - 2007 - 15 с

Подписано в печать / №. О У Бумага типографская Уел печ л 1

Тираж 100 экз. Заказ № ЮЪ

Формат бумаги 60 х 84/16 Печать офсетная Уч-изд л 1,1 Цена договорная

Сибирский федеральный университет Институт естественных и гуманитарных наук Издательский центр

660041 г Красноярск, пр Свободный, 79

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

Введение.

1. Основные определения и теоремы.

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

1.2. Допустимые и выводимые правила.

2. Правила вывода SbtCt-логик.

2.1. Аксиоматика исследуемых логик.

2.2. Финитная аппроксимируемость логик 55tC/, I < t, S5tJ.

2.3. Разрешимость по допустимости правил вывода финитно-аппроксимируемых и разрешимых логик Л Э SbtCt.

2.4. Необходимые и достаточные условия разрешимости по допустимости правил с метапеременными в логиках S5tQ, I < t, S5tJ.

2.5. Структурная неполнота логик S5tCi, I < t, S5tJ.

3. Правила вывода некоторых линейных логик.

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

3.2. Разрешимость по допустимости правил вывода логик Lin Т и LinDA.

4. Логика SbtCt с ограниченным объемом сгустков.

4.1. Логики S^C? и 55(Cî|2.

4.2. Алгебра Bt.

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

Актуальность темы. В этой работе будут исследоваться на разрешимость по допустимости правил вывода некоторые многомодальные логики, расширяющие S5t, t € N, а также линейные логики LinT и LinDA, и для исследуемых логик будут построены алгоритмические критерии определения допустимости правил вывода. Правило вывода — это правило, регламентирующее допустимые способы перехода от некоторой совокупности формул ai, .,ап, называемых посылками, к некоторой определенной формуле ß, называемой заключением. Правило вывода обычно записывается в виде выражения . ,ап/ß. Правило вывода называется истинным в логике А, если из того, что а\,.,ап € А следует, что ß € А, называется выводимым (или доказуемым) в А, если ß выводится из посылок с помощью аксиом и постулированных правил логики А, и допустимым в А, если при любой подстановке е, из af £ А,., аеп € А следует, что ße 6 А. Допустимые правила вывода — это наибольший класс правил, которые мы можем использовать в выводах данной логики А, сохраняя множество ее доказуемых формул, т. е. с помощью таких правил мы не получим формул, которые не являются теоремами логики А. Так как в аксиоматике логик постулированных правил немного, то использование допустимых правил позволяет сокращать и упрощать процесс доказательства. Например, в исчислении высказываний (ИВ) и исчислении предикатов ничуть не реже, чем постулированное правило modus ponens: а, а ß /ß, используется правило а ß, ß —» 7/а —► 7. Но в ИВ все допустимые правила доказуемы, а в логиках первого порядка, модальных и супериптуиционистских логиках существуют допустимые, но не доказуемые правила вывода, и впервые это было замечено для интуиционистского исчисления Н (примерно в 50-х годах прошлого века в разных работах). Определение допустимого правила появилось в работе П. Лоренцеиа [51] в 1955 году. Правило называлось допустимым, если после добавления его к исходной системе все теоремы, выводимые при использовании этого правила, были бы теоремами исходной системы. П. Хар-роп в работе [46] за 1960 г. показал, что в Я допустимо, но не доказуемо правило -ix -* (у V z) / (~>х —► у) V (~>х —► z). До этого Г. Крайзель и X. Патнэм в [49] показали, что иитуициоиистской логике не принадлежит формула (->х —► (у v z)) —► ((-<х —► у) V (~>х -* z)). Г. Е. Минц в работе [9] доказал, что если правило г допустимо в Я и не содержит связок —» или V, то г выводимо в Я, и показал, что правило ((х —» у) —► (х V у)) / (((х у) -* х) V ((х —> у) 2))) допустимо, но не выводимо в Я. Выводимость допустимых в Я правил исследовалась также А. И. Циткиным в [34]. В модальных логиках 54, 54.1, йгг допустимо, но не выводимо правило Леммопа-Скотта □ (□ (□<>□;> -> Пр) -> {Пр V □ □ р) / ПОПр V □ -л Пр, [67].

Логики, в которых все допустимые правила доказуемы, называются структурно-полными. Такими логиками являются, к примеру, ИВ и модальная логика 54.3йгг. Модальные логики К, Т, #4, 54, 55 не являются структурно-полными. В этих логиках допустимо, но не доказуемо правило 0-<х А Ох /у. Структурной полнотой су-периптуиционистских логик занимались а. И. Циткин [35], Т. Прукнал [57], а структурную полноту модальных логик исследовали В. Джиобяк [39], В. В. Рыбаков [67]. Что касается немодальных и иесуперинтуиционистских логик, то известны такие результаты: Токарз установил структурную полноту некоторых логик Лукасевича [76], Прукнал доказал структурную полноту логики Медведева конечных задач [56], Войтыляк показал, что конечные классы многозначных логик являются структурно-полными [77].

По аналогии с проблемой разрешимости логик возникает вопрос о разрешимости по допустимости правил вывода. Впервые этот вопрос был поставлен в начале 70-х годов прошлого века X. Фридманом для интуициоиистского исчисления Я. В 1973 г. А. В. Кузнецов поставил вопрос о существовании конечного базиса допустимых правил для логики Я. Базис допустимых правил — это такие правила, из которых все остальные получаются как следствия. Положительное решение первого вопроса в 1984 г. в работе [17] и отрицательное решение второго вопроса в 1985 г. в [19] были даны В. В. Рыбаковым. Им же были найдены алгоритмические критерии и решены вопросы о базисах для широкого класса суперинтуициоиистских и транзитивных од-номодальных логик [14, 31, 67], [60]-[66]. К примеру, разрешимыми по допустимости оказываются логики #4, #4.1, #4.2, #4.3, 54, 54.1, 54.2, 54.3, вгг, вгг.2, вгг.3, Ы, Я, КС, 1С, логики #4, #4.1, #4.2, 54, 54.1, 54.2, Стг, вгг.2, Ы, Я, КС не имеют конечного базиса допустимых правил, а логика 54.3 и все ее нормальные расширения такой базис имеют и состоит он из одного правила Ох А -«Ох/у. То есть логика 54.3 и все ее нормальные расширения оказываются не только финитно-аппроксимируемы [37] и конечно аксиоматизируемы [40], но разрешимы по допустимости и обладают конечным базисом допустимых правил. Если же правило не допустимо в некоторой нормальной логике Л Э 54.3, то оно опровергается на конечном фрейме, адекватном данной логике. Таким свойством не обладают, к примеру, финитно-аппроксимируемые логики #4, 54, С?гг, [68]. В работах Р. Иемхофф [48] и В. В. Рыбакова [70] были построены бесконечные базисы для логик Я и 54 соответственно. А. Н. Руцким был построен бесконечный явный базис для логики #4 [12], а

Б. Р. Федоришиным для логики йЬ [33]. Разрешимость по допустимости логик ¿'4.2, КС и отсутствие у этих логик конечного базиса было доказано С. В. Бабенышевым в [1], [2]. Ю. В. Безгачева доказала, что транзитивные конечно-аксиоматизируемые и финитно-аппроксимируемые логики ширины 2 разрешимы по допустимости [3], а В. В. Римацким было доказано, что модальные финитно-аппроксимируемые логики ширины 2 имеют конечный базис допустимых правил [11]. Большое значение для решения задач, связанных с допустимостью правил, имела возможность представления свободных алгебр из многообразия модальных алгебр данной логики специальными моделями Крипке (являющимися реляционными) — п-характеристическими моделями. В [67] получен также критерий, при котором логика первого порядка разрешима относительно допустимости правил вывода. Такими логиками оказываются только логики, порожденные конечной моделью. Результаты о базисах и алгоритмические критерии для некоторых других модальных, временных и суперинтуиционистских логик смотрите, например, в работах [4, 10, 36, 45, 71, 72, 73].

Наряду с обычными правилами рассматриваются также правила вывода с мета-переменными, или, как еще говорят, с параметрами. Пусть, например, дано правило г := а (рь. ,рп, дь., 9/) //? (рь. ,рп, дь., и подстановки в это правило будем делать только вместо переменных р!,.,рп. Тогда переменные (¡1,- ■ ■, % называются метаперемениыми, а само правило г — правилом вывода с метапеременными. Оно считается допустимым в логике А при выполнении следующего условия. Если при некоторой подстановке вместо переменных р\,.,рп формулами 71,.,7П из того, что а(71,. ,7„, 91,. ,ф) € А следует, что ¡3(71,. ,7п, <7ь ■ ■ •,£

Причиной изучения таких правил стали проблемы подстановки и разрешимости логических уравнений, и проблема разрешимости уравнений в свободных алгебрах, соответствующих некоторой алгебраической логике. Сформулируем, например, вопрос о подстановке для заданной логики А: существует ли алгоритм, который для произвольной формулы а (р1,. ,рп, 91,., 9/), где 91,., 9; — это метапеременные, определяет, найдутся ли такие формулы /?!,.,/?„, что а (/?1, .,/?„, 91,. ,9;) € А? Проблема подстановки для интуиционистской логики Я в 50-х годах прошлого века обсуждалась в Московской и Ленинградской логических школах. Разрешимость проблемы подстановки для Н была доказана В. В. Рыбаковым в работе [29] за 1990 год. В этой работе он показал, что разрешимость проблемы подстановки, разрешимость логических уравнений, и разрешимость уравнений в свободной алгебре некоторой логики можно свести к разрешимости проблемы допустимости соответствующих правил вывода с метапеременными в соответствующей логике А. Он доказал разрешимость по допустимости правил вывода с метаперемеппыми большого класса суперинтуиционистских и транзитивных модальных логик [67, 24, 25, 28, 29, 31, 60, 62, 64]. К этому классу принадлежат КА, КАЛ, КА.2, КА.З, 54, 54.1, 54.2, 54.3, вгг, вгг.2, С?г,г.3, йЬ, Н, КС, ЬС. В. Р. Кияткиным доказано, что все предтабличные логики, расширяющие 54, и все конечно-аксиоматизируемые логики конечной глубины, разрешимы по допустимости правил вывода с метаперемеппыми [6].

Добавим еще, что также исследовались уравнения в свободных группах и свободных полугруппах. Уравнения свободных групп изучались Р. К. Линдоном [52], [53], а в свободных полугруппах Г. С. Макании построил алгоритм для нахождения решения таких уравнений [54], [55].

К настоящему времени существует глубоко развитая теория допустимых правил для транзитивных одномодальных логик, однако в нетраизитивных и многомодальных логиках кажется слишком сложным построить алгоритмы определения допустимости правил для достаточно широкого класса таких логик. Допустимости правил в иетрапзитивиых логиках посвящены, к примеру, работа М. И. Голованова и Е. М. Юрасовой [5], в которой доказана разрешимость по допустимости для нетраизитив-иой одномодальной логики с оператором «завтра», и Рыбакова [71], а допустимости в многомодальных логиках — работы [72, 73, 79, 80].

Одним из условий существования алгоритмов в [67] является обычная разрешимость логики и ее финитная аппроксимируемость. И в нашем случае алгоритмические критерии будут доказаны только для логик, обладающих этими двумя свойствами. Несмотря на то, что все расширения логики 55 финитно-аппроксимируемы, уже среди расширений логики 55з встречаются не финитно-аппроксимируемые логики, [41]. Эти логики относятся к особому классу многомодальных логик — многомерным логикам, основные результаты о которых суммированны в [41]. Но хотя обычно алгоритмы определения допустимости правил вывода строились для финитно-аппроксимируемых логик, в [72] Рыбаковым В. В. был построен алгоритм определения допустимости правил для двух не финитно-аппроксимируемых логик, это логики, порожденные фреймами {2, >, <), (/V, >, <).

Широкий круг вопросов о свойствах многомерных и многомодальных логик рассмотрен в работах [42, 43, 47, 50, 58, 74, 75].

Цель работы.

1) Исследовать разрешимость проблемы допустимости правил вывода в логиках 55¿С;, I < Ь, и 55^, где 55^, I < Ь — это логика с дополнительными к аксиоматике

S5t аксиомами л nj2 ■ ■ ■ пи • • • пчР,

У il,.,il, Vji,.,ji, il,.,il € {1 ,.,t},l <t, jk ф js, ik ф is при к ф s, a S5tJ получена добавлением к Sbt аксиом □ tp —> Пф, г := 1,. ,t.

2) Исследовать на разрешимость по допустимости правил вывода линейные логики ЫпТ и LinDA.

3) Пусть S5tC? — это логика S5tCt плюс аксиомы ^ Д О* (ft А Д чрД . l<t<n+l l<jy«<n+l

Выяснить, является ли эта логика логика табличной.

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

Основные результаты. В диссертации получены следующие основные результаты.

1) Доказана разрешимость по допустимости правил вывода финитно-аппроксимируемых и разрешимых логик, расширяющих SbtCt.

2) Доказана разрешимость по допустимости правил вывода линейных финитно-аппроксимируемых и разрешимых логик, расширяющих Lin DA.

3) Доказано, что логика S5tC? является табличной, и ее наибольшие конечные корневые фреймы содержат не более пь элементов.

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

Апробация работы. Результаты диссертации докладывались на

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

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

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

Публикации. По теме диссертации опубликовано пять работ [78]-[82].

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

Заключение диссертации по теме "Математическая логика, алгебра и теория чисел"

Заключение

К настоящему времени существует глубоко развитая теория допустимых правил для транзитивных одномодальных логик, но получено очень мало результатов о допустимости правил вывода в многомодальных логиках. Допустимости правил вывода в многомодальных логиках посвящены, например, работы [72, 73, 79, 80]. Поэтому полученные в диссертации результаты могут быть полезны для дальнейшего изучения правил вывода в многомодальных логиках. Имеет смысл исследовать на разрешимость по допустимости не только расширения логики £>5г, но и саму эту логику.

В работе Рыбакова [72] было доказано, что бимодальные логики, порожденные фреймами (2, >, <), (./V, >, <) не являются финитпо-аппроксимируемыми, но разрешимы относительно допустимости правил вывода. В параграфе 3.2 мы доказали, что логики, порожденные фреймами (ф, >, <), >, <) финитно-аппроксимируемы и разрешимы по допустимости. В связи с этими результатами возникает также вопрос о разрешимости по допустимости логик, порожденных, например, фреймами г, >, <), (лг, >, <), (я, >, <) и (я, >, <).

Список источников диссертации и автореферата по математике, кандидата физико-математических наук, Кошелева, Анна Владимировна, Красноярск

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

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

3. Кияткин В. Р. Правила вывода с метапеременными и логические уравнения в табличных и предтабличных локально конечных модальных логиках. // Красноярск, Краен, университет. 1995. - Деп. в ВИНИТИ - 15.12.95. - ДО3350-В95.

4. Кияткин В. Р. Правила вывода с метапеременными и логические уравнения в предтабличной модальной логике РМ1. // Сибирский математический журнал.- 2000. Т.41. - №1. - С.88-97.

5. Мендельсон Э. Введение в математическую логику. // Москва, Наука. -1971.- 320 с.

6. Минц Г. Е. Производность допустимых правил. // Записки научного семинара ЛОМИ АН СССР. 1972. - №32. - С.85-99.

7. Руцкий А. Н. Явный базис для правил вывода, допустимых в модальной системе КА. // Красноярск, Краен, университет. 2002. - Деп. в ВИНИТИ -11.11.2002. - М939-В2002.

8. Руцкий А. Н., Федоришин Б. Р. Критерий наследования допустимых правил вывода модальной логики К А. / / Сибирский математический журнал. 2002. -Т.43 - №6.

9. Рыбаков В. В. Допустимые правила предтабличных модальных логик. // Алгебра и логика. 1981. - Т.20. - №4. - С.440-464.

10. РЫБАКОВ В. В. Базисы квазитождеств конечных модальных алгебр. // Алгебра и логика. 1982. - Т.21. - №2. - С.219-228.

11. РЫБАКОВ В. В. Разрешимость проблемы допустимости в конечнослойных модальных логиках. // Алгебра и логика. 1984. - Т.23. - №1. - С.100-116.

12. РЫБАКОВ В. В. Критерий допустимости правил в модальной системе 54 и интуиционистской логике. // Алгебра и логика. 1984. - Т.23. - №5. - С.546-572.

13. Рыбаков В. В. Допустимые правила логик, включающих 54.3. // Сибирский математический журнал. 1984. - Т.25. - №5. - С.141-145.

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

15. РЫБАКОВ В. В. Базисы допустимых правил модальной системы Grz и интуиционистской логики. // Математический сборник. 1985. - Т. 128. - №3. -С.321-339.

16. Рыбаков В. В. Универсальные теории свободных А-алгебр при А 3 54.3. // Сложностные проблемы математической логики. Калинин. 1985. - С.72-75.

17. РЫБАКОВ В. В. Алгебраические методы в пропозициональной логике. // Семиотика и информатика. 1986. - Вып.28. - С.102-121.

18. РЫБАКОВ В. В. Разрешимость по допустимости модальной системы Grz и интуиционистской логики. // Известия АН СССР: Сер. математическая. 1986. - Т.50. - №3. - С.598-616.

19. РЫБАКОВ В. В. Уравнения в свободной топобулевой алгебре. // Алгебра и логика. 1986. - Т.25. - №2. - С.172-204.

20. Рыбаков В. В. Уравнения в свободной топобулевой алгебре и проблема подстановки. // Доклады АН СССР. 1986. - Т.287. - №3. - С.554-557.

21. Рыбаков В. В. Базисы допустимых правил модальной системы Grz и интуиционистской логики. // Математический сборник. 1987. - Т.56. - №2. - С.311-331.

22. РЫБАКОВ В. В. Критерии допустимости правил вывода с параметрами в интуиционистской пропозициональной логике. // Известия АН СССР: Сер. математическая. 1990. - Т.54. - №6. - С.1331-1341.

23. РЫБАКОВ В. В. Семантические критерии допустимости правил вывода в логиках SA и Grz. // Математические заметки. 1991. - Т.50. - Вып.1б. - С.84-91.

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

25. ЦИТКИН А. И. О структурной полноте суперинтуициопистских логик. // Доклады АН СССР. 1978. - Т.241. - №1. - С.40-43.

26. Bezgacheva J. v. Admissible rules of temporal logic LinTGrz. // Bulletin of the Section of Logic. 1997. - V.26. - №2. - P.60-69.

27. Bull R. That all normal extension of 54.3 have the finite model property. // Z. fur Math. Log. und Grundl. der Math. 1967. - V.12. - P.325-329.

28. Chagrov A., Zakharyaschev M. Modal logics. // London, Cambridge Press. -1997. 589 p.

29. Dziobiak W. Structural completeness of modal logics containing KA. // Bulletin of the Section of Logic. 1983. - V.12. - M. - P.32-36.

30. Fine K. Logic containing 54.3. // Z. fur Math. Log. und Grundl. der Math. 1971. - V.17. - P.371-376.

31. Gabbay D. M., Kurucz A., Wolter F., Zakharyaschev M. Many-dimensional modal logics: theory and applications. // Studies in Logic and Foundations of Mathematics, Elseiver Sci. Publ., North-Holland. 2003. - V.148. - 768 p.

32. Gabbay D., shehtman V. Products of modal logics. Part I. // Logic Journal of the IGPL. 1998. - V.6. - P.73-146.

33. Gabbay D., Shehtman V. Products of modal logics. Part III. Products of modal and temporal logics. // Studia Logica. 2002. - V.72. - №2. - P. 157-183.

34. Goldblatt R. Logic of time and computation. // Center for the Study of Language and Information, Leland Stanford Junior University. 1987. - №7. - 126 p.

35. Golovanov M. I, Rybakov V. V., Yurasova E. M. A necessary condition for the rules to be admissible in temporal tomorrow logic. // Bulletin of the Section of Logic. 2003. - V.32. - №4. - P.213-220.

36. Harrop R. Concerning formulas of the types A —> B v C, A 3 xB(x) in intuitionistic formal system. // Journal of Symbolic Logic. 1960. - V.25. - №1. -P.27-32.

37. Hirch R., Hodkinson I., and Kurucz A. On modal logics between K x K x K and S5 x S5 x S5. // Journal of Symbolic Logic. 2002. - V.67. - P.221-234.

38. IemhOFF R. On the admissible rules of intuitionistic propositional logic. // Journal of Symbolic Logic. 2001. - V.66. - №2. - P.402-428.

39. Kreisel G., Putnam H. Eine Unableitbarkeitsbeweismethode fur den intuitionistischen Aussagankalkiil. // Arch. Math. Logik Grundlagenforsch. 1957.- V.3. Nos.3-4, 74-78.

40. Kurucz A. On axiomatising products of Kripke frames. // Journal of Symbolic Logic. 2000. - V.65. - P.923-945.

41. LORENZEN P. Einfiing in Operative Logik und Mathmatik. // Berlin. Gottingen.- Heidelberg. 1955. - 412 p.

42. Lyndon R. C. Equations in free groups. // Trans. Amer. Math. Soc. -1960. V.96.- P.445-457.

43. Lyndon R. C. Equations in free metabelian groups. // Pros. Amer. Math. Soc. -1966. V.17. - P.728-730.54. makanin G. S. Problem of solvability for equations in free semigroups. // Mathemetical Sbornik. 1977. - №.2. - P. 147-236.

44. PRUCNAL T. Structural completeness of some fragments of intermediate logics. // Bulletin of the Section of Logic. 1983. - V.12. - №1 - P.18-21.

45. Reynolds M. and Zakharyaschev M. On the products of linear modal logics. // Journal of Logic and Computation. 2001. - V.ll. - P.909-931.

46. RlMATSKlY V. V. Finite bases of admissible inference rules for modal logics of width 2. // Bulletin of the Section of Logic. 1997. - V.26. - №3. - P. 126-134.

47. RYBAKOV V. V. Metatheories of first-order theories. // Proc. of the 4-th Asian Logic Conference. CSK Educational Center. Tokyo, Japan. - 1990. - P. 16-17.

48. Rybakov V. V. Rules of inference with parameters for intuitionistic logic. // Journal of Symbolic Logic. 1992. - V.57. - №3. - P.912-923.

49. Rybakov V. V. Admissibility of logical inference rules. // Studies in Logic and Foundations of Mathematics, Elseiver Sci.Publ., North-Holland. New-York.- Amsterdam. 1997. - V.136 - 617 p.

50. Rybakov V. V. Construction of an explicit basis for rules admissible in modal system 54. // Mathematical Logic Quarterly. 2001. - V.47. - №4. - P.441-451.

51. Rybakov V. V. Logical consecutions in intransitive temporal linear logic of finite intervals. // Journal of Logic Computation. 2005. - V.15. - №5. - P.C63-678.

52. Rybakov V. V. Logical consecutions discrete linear temporal logic. // Journal of Symbolic Logic. 2005. - V.70. - №4. - P.1137-1149.

53. Rybakov V. V. Logics with universal modality and admissible consecutions. // Journal of Applied Non-Classical Logics. 2007. - V.17. - №3. - P.381-394.

54. Segerberg K. Modal logic with linear alternative relations. // Theoria. 1970. -V.36. - P.301-322.75. shehtman V. Two-dimensional modal logics. // Mathematical Notices of the USSR Academy of Sciences. 1978. - V.23. - P.417-424.