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

Актуальность темы

В этой работе будут исследоваться на разрешимость по допустимости правил вывода некоторые многомодальные логики, расширяющие 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 Пф, г := 1,., t.

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

3) Пусть S5tC? — это логика S5tCt плюс аксиомы ^ Д О* (ft, А Д чрД. 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 мы доказали, что логики, порожденные фреймами (ф, >, <), >, <) финитно-аппроксимируемы и разрешимы по допустимости. В связи с этими результатами возникает также вопрос о разрешимости по допустимости логик, порожденных, например, фреймами г, >, <), (лг, >, <), (я, >, <) и (я, >, <).