Введение к работе
Актуальность темы. Допустимые правила вывода вместе с аксиомами определяют дедуктивную силу логических систем. В то время как целью математического исследования часто является определение минимального необходимого набора выразительных средств, практические применения часто требуют корректного расширения используемых правил построения выводов. Для этих целей очень важна математическая проработка используемых систем рассуждений: решение вопросов о разрешимости, разрешимости по допустимости, конечной или эффективной аксиоматизируемости принятой логической системы и вопроса о существовании конечного базиса допустимых правил вывода. Отсутствие допустимости для правил вывода с метапеременными тесно связано с существованием решений логических уравнений, что дает эффективным критериям допустимости новую широкую область применений. Существует несколько интересных проблем, имеющих эквивалентную формулировку через допустимость подходящих правил вывода. Так свойство модальных логик быть замкнутыми относительно взятия подструктур может быть сведено к допустимости правила вывода подходящего вида.
Правила вывода с параметрами являются более общими объектами, чем логические уравнения. Наличие алгоритмических критериев допустимости правил вывода с параметрами позволяет исследовать еще один важный аспект выразительной силы логик — проблему существования неподвижных точек логических схем.
Цель работы
1. разработать более общий подход к построению критериев допустимости правил вывода с ыетапеременными в модальных пропозициональных логиках, расширяющих логику Льюиса S4, применимый в случаях логик S4.2 и S4.1.
-
адаптировать метод построения алгоритмических критериев допустимости к случаю суперинтуиционистских логик и исследовать проблему допустимости правил вывода с метапеременными в суперинтуиционистской логике слабого закона исключенного третьего — логике КС.
-
исследовать разрешимость проблемы допустимости в наибольшем и наименьшем модальном напарниках КС — логиках S4.2Grz и S4.2, а также проверить является ли S4.2 модальным напарником КС по допустимости.
-
с помощью разработанной техники исследовать проблему существования базиса допустимых правил вывода от конечного числа переменных в логиках S4.1, S4.2 и S4.2Grz.
5. разработать алгоритм построения некоторых решений логических
уравнений в модальных логиках S4.1, S4.2 и S4.2Grz.
Методика исследования. В исследовании применяются общие методы теоретико-модельной и алгебраической семантики для пропозициональных суперинтуиционистских и модальных логик.
Научная новизна. Все результаты, полученные в диссертации, являются новыми и снабжены строгими доказательствами.
Теоретическая и практическая ценность. Полученные результаты имеют теоретическую ценность и могут быть использованы в дальнейших исследованиях по проблемам допустимости правил вывода и разрешимости логических уравнений.
Аппробания работы. Результаты диссертации докладывались на X всесоюзной конференции по математической логике (Алма-Ата, 1990), XI межреспубликанской конференции по математической логике (Казань, 1992 III международной конференции по алгебре памяти Каргаполова (Красноярск, 1993), международной конференции по математической логике посвященной 85-летию со дня рождения А.И. Мальцева (Новосибирск, 1994), русско-японском логическом коллоквиуме NSL'95 (Иркутск, 1995), а также
на заседаниях семинаров "Алгебра и логика" при Новосибирском государ
ственном университете, семинара по неклассическим логикам при Инсти
туте математики СО РАН (Новосибирск) и на заседаниях Красноярского
алгебраического семинара. ,
Публикации. По теме диссертации опубликовано 9 работ [5-13].
Структура и объем работы. Диссертация состоит из введения, трех глав, заключения и списка литературы из 77 наименований и занимает 99 страниц машинописного текста.
Много раз результаты и ход работы обсуждались с Владимиром Владимировичем Рыбаковым, которому я обязан также за поддержку и терпение. Я также благодарен Голованову М.И. и Безгачевой Ю.В. за полезные обсуждения на семинарах кафедры алгебры и математической логики Красноярского госуниверситета. Я обязан также Левчуку Владимиру Михайловичу за внимание и поддержку.