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

• Автор: Кошелева, Анна Владимировна
• Шифр специальности: 01.01.06
• Научная степень: Кандидатская
• Год защиты: 2007
• Место защиты: Красноярск
• Количество страниц: 73 с.

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

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

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

2. Правила вывода 55гСгЛогик

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

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

2.3. Разрешимость по допустимости правил вывода финитио-аппроксимируемых и разрешимых логик Л 2 SbtCt
2.4. Необходимые и достаточные условия разрешимости по допустимости правил с метаперемеппыми в логиках S5tC[, I < t, S5tJ

2.5. Структурная неполнота логик 55tC/,/< 55t J

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

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

3.2. Разрешимость по допустимости правил вывода
логик LinT и Lin DA
4. Логика SbtCt с ограниченным объемом сгустков
4.1. Логики S5tC? и 55tC"2
4.2. Алгебра Bt
Заключение
Список литературы
Работы автора по теме диссертации

Актуальность темы. В этой работе будут исследоваться на разрешимость по допустимости правил вывода некоторые многомодальные логики, расширяющие S5(, t Є N, а также линейные логики LinT и LinDA, и для исследуемых логик будут построены алгоритмические критерии определения допустимости правил вывода. Правило вывода — это правило, регламентирующее допустимые способы перехода от некоторой совокупности формул ai ап, называемых посылками, к некоторой определенной формуле /3, называемой заключением. Правило вывода обычно записывается в виде выражения а,... ,ап /0. Правило вывода называется истинным в логике А, если из того, что аі о„ Є А следует, что 0 € А, называется выводимым (или доказуемым) в А, если 0 выводится из посылок с помощью аксиом и постулированных правил логики А, и допустимым в А, если при любой подстановке е, из af Є А a£ Є А следует, что 0Е є А. Допустимые правила вывода — это наибольший класс правил, которые мы можем использовать в выводах данной логики А, сохраняя множество ее доказуемых формул, т. е. с помощью таких правил мы не получим формул, которые не являются теоремами логики А. Так как в аксиоматике логик постулированных правил немного, то использование допустимых правил позволяет сокращать и упрощать процесс доказательства. Например, в исчислении высказываний (ИВ) и исчислении предикатов ничуть не реже, чем постулированное правило modus ponens: а, а —у 0 /0, используется правило а -* 0, 0 —» 7 /а -» 7.. Но в ИВ все допустимые правила доказуемы, а в логиках первого порядка, модальных и суперинтуиционистских логиках существуют допустимые, но не доказуемые правила вывода, и впервые это было замечено для интуиционистского исчисления Н (примерно в 50-х годах прошлого века в разных работах). Определение допустимого правила появилось в работе П. Лоренцеиа [51] в 1955 году. Правило называлось допустимым, если после добавления его к исходной системе все теоремы, выводимые при использовании этого правила, были бы теоремами исходной системы. П. Хар-роп в работе [46] за 1960 г. показал, что в II допустимо, но не доказуемо правило -їх -* (у V z) / (-їх —* у) V (-їх —► z). До этого Г. Крайзель и X. Патнэм в [49] показали, что интуиционистской логике не принадлежит формула (-їх —> (у V в)) —♦ ((-<х -* у) V (-їх -* z)). Г. Е. Минц в работе [9] доказал, что если правило г допустимо в Я и не содержит связок —> или V, то г выводимо в Я, и показал, что правило ((а; —► у) -* (х V у)) / (((л —> у) -у х) V ((х —> у) г))) допустимо, но не выводимо в Я. Выводимость допустимых в Я правил исследовалась также А. И. Цит-

киным в [34]. В модальных логиках 54, 54.1, Єгг допустимо, по не выводимо правило Леммона-Скотта □ (□ (ПОПр —> Пр) —> (Пр V □ ->□ р) / ПОПр V □ -іОр, [67].
Логики, в которых все допустимые правила доказуемы, называются структурно-полными. Такими логиками являются, к примеру, ИВ и модальная логика ЗА .'Юг г. Модальные логики К, Т, КА, 54, 55 не являются структурио-полиыми. В этих логиках допустимо, но ие доказуемо правило 0-*х Л Ох /у. Структурной полнотой су-перинтуиционистских логик занимались А. И. Циткин [35], Т. Прукнал [57], а структурную полноту модальных логик исследовали В. Джиобяк [39], В. В. Рыбаков [67]. Что касается немодальных и несуперинтуициоиистских логик, то известны такие результаты: Токарз установил структурную полноту некоторых логик Лукасевича [76], Прукнал доказал структурную полноту логики Медведева конечных задач [56], Войтыляк показал, что конечные классы многозначных логик являются структурнополными [77].
По аналогии с проблемой разрешимости логик возникает вопрос о разрешимости по допустимости правил вывода. Впервые этот вопрос был поставлен в начале 70-х годов прошлого века X. Фридманом для интуиционистского исчисления Н. В 1973 г. А. В. Кузнецов поставил вопрос о существовании конечного базиса допустимых правил для логики Я. Базис допустимых правил — это такие правила, из которых все остальные получаются как следствия. Положительное решение первого вопроса в 1984 г. в работе [17] и отрицательное решение второго вопроса в 1985 г. в [19] были даны В. В. Рыбаковым. Им же были найдены алгоритмические критерии и решены вопросы о базисах для широкого класса суперинтуиционистских и транзитивных одномодальных логик [14, 31, 67], [60]-[66]. К примеру, разрешимыми по допустимости оказываются логики КА, КА. 1, К А.2, КА.Ъ, 54, 54.1, 54.2, 54.3, Єгг, Єгг.2, Єгг.З, Ы, Я, КС, ЬС, логики КА, КАЛ, КА.2, 54, 54.1, 54.2, Сгг, вгг.2, Ы, Я, КС не имеют конечного базиса допустимых правил, а логика 54.3 и все ее нормальные расширения такой базис имеют и состоит он из одного правила Ох Л -> Ох / у. То есть логика 54.3 и все ее нормальные расширения оказываются не только финитно-аппроксимируемы [37] и конечно аксиоматизируемы [40], но разрешимы по допустимости и обладают конечным базисом допустимых правил. Если же правило не допустимо в некоторой нормальной логике Л Э 54.3, то оно опровергается на конечном фрейме, адекватном данной логике. Таким свойством ие обладают, к примеру, финитно-аппроксимируемые логики КА, 54, Єгг, ЄЬ [68]. В работах Р. Иемхофф [48] и В. В. Рыбакова [70] были построены бесконечные базисы для логик Я и 54 соответственно. А. Н. Руцким был построен бесконечный явный базис для логики КА [12], а

4. Логика 55*(7* с ограниченным объемом сгустков
4.1. Логики 55гС(п и 55гС£2
Пусть £ДС" — это логика 55^ плюс аксиомы
^ = - Д о*(р4л Д -.?*), л
1<г<пЦ 1<;#г<п+1
Несложно проверить, что на конечных фреймах, адекватных логике £5(С,(, формула будет истинна тогда и только, когда все сгустки по отношению Д содержат не более п элементов. Пусть £5(С£2 — это логика £5(С(П плюс аксиомы Р;Р:р —> ДПгр, УгД € {1,
Нетрудно проверить, что любая рефлексивная корневая одноэлементная модель является моделью для логик £54С" и 5540|2» а а Л -^а опровергается на всех таких моделях, следовательно, данные логики непротиворечивы.
Введем обозначения. Вместо х Я;, Х2 А х2 Я2 хз Л ... Л Д^. х* будем писать х^ Д2 Д2... Д-4 х*, или что существует путь Д, Д2... Д4 из точки х в точку хк. Точки, достижимые ИЗ Х ПО пути Д, Д2 ... Я Д Яг! Я2 • • • -Я* — ЭТО те точки, которые ДОСТИЖИМЫ ИЗ XI по пути Я1 Яг • • • Я* И 1Ю ДОСТИЖИМЫ ПО Я; Яг • • • Яг
Теорема 4.1. Логика £54С" финитно-аппроксимируема.
Доказательство.
Пусть Л4 — корневая, адекватная логике 55(С'" 554-модель с означиванием V, а — некоторая формула с переменными из Яогтг(У), опровергающаяся на Л4. Пусть Я := {А, • ■ •,/?щ} ~~ множество всех конъюнкций, в которые входят или подформула формулы а, или отрицание этой подформулы. Формула (5(Д) := (Л$есга(&) Л □т(Удес-(А)$)> т := 1,... Д, /г := 1,... ,щ, где Ст(Д) - сгусток, который содержит элемент, на котором истинна формула Д, будет истинна на том и только том сгустке Ст, который является р-морфпым прообразом сгустка С"”(Д). Обозначим множество всевозможных формул <5(Д) как
Пусть XI е Л4, а 2/г Уг — это все точки, достижимые из XI по отношению
Д. Тогда на точках XI, г/2 У1 истинны некоторые формулы из множества Я
Д Д, соответственно и некоторая формула <5{ € Д. Тогда на XI истинна формула £1 := Д Л Д. Кроме того, на Х истинна некоторая формула 7 := 52 Л ... Л <5‘.