Модальная Логика

Область логики, в к-рой наряду с обычными высказываниями рассматриваются модальные высказывания, т. е. высказывания типа "необходимо, что.,.", "возможно, что..." и т. п. В математич. логике рассматриваются различные формальные системы М. л., выявляется взаимосвязь между этими системами, изучаются их интерпретации. Элементы М. л. имелись по существу еще у Аристотеля (4 в. до н. э.), а от него перешли в классич. философию. Впервые М. л. была формализована К. Льюисом [1], к-рый построил пять пропозициональных систем М. л., получивших в литературе обозначения S1-S5 (их формулировки приведены ниже). Затем были построены и исследованы другие системы М. л. Большое разнообразие систем М. л. объясняется тем, что понятия "возможно" и "необходимо" можно уточнять различными способами и, кроме того, по-разному трактовать сложные модальности типа, "необходимо возможно" и "взаимоотношения" модальностей с логич. связками. Большинство изучавшихся систем М. л. опирается на классич. логику, однако рассматриваются и системы, основанные на интуиционистской логике (см., напр., [6]). Ниже описывается несколько наиболее хорошо изученных пропозициональных систем М. л. Язык каждой из этих систем получается из языка классич. исчисления высказываний Р добавлением новых одноместных связок (модальных операторов) (необходимо) и (возможно). Поскольку почти во всех системах имеет место соотношение то в качестве исходного берется один модальный оператор, напр. , а другой определяется через него с помощью соотношения (*). Система S1. Схемы аксиом:1) все формулы вида , где — выводимая в Р формула,2) 3) Правила вывода:I) II)III) Система К. Схемы аксиом:1) все схемы аксиом исчисления высказываний Р,2) Правила вывода: модус поненс и A/яA(я-введение). Система Т: Система В: Система S4: Система S5: Среди вышеупомянутых систем важное значение имеет S4, т. к. в ней интерпретируется интуционист-ское исчисление высказываний I, т. е. по всякой пропозициональной (немодальной) формуле Аможно построить такую формулу модальной логики, что В связи с этим особый интерес представляет система Гжегорчика (см. [5]): для к-рой верна теорема о переводе: для любого множества схем аксиом Г и любой формулы А где причем G — самая сильная система с таким свойством. Эта теорема позволяет переносить нек-рые свойства (напр., полноту или разрешимость) с расширений системы S4 (или G) на промежуточные логики. Для каждой пропозициональной системы М. л. S можно рассмотреть соответствующую предикатную систему, к-рая получается добавлением к языку системы S предметных переменных, предикатных символов и кванторов (или одного из них). Также добавляются обычные схемы аксиом и правила вывода для кванторов. Кроме того, иногда добавляют и другие аксиомы, описывающие действие модальных операторов на кванторы, напр. т. н. формулу Баркан: Алгебраич. интерпретация систем М. л. задается нек-рой алгеброй (называемой также матрицей) где М- множество истинностных значений, D- множество выделенных истинностных значений, — операции на М, соответствующие связкам . Формула наз. общезначимой на алгебре , если при всякой оценке ее пропозициональных переменных элементами Мона принимает выделенное значение. Система М. л. S наз. полной относительно класса алгебр , если всякая формула выводима в S тогда и только тогда, когда она общезначима на всякой алгебре из . Напр., система S4 полна относительно класса конечных т. н. топологических булевых алгебр (см. [3]). Вообще, система S наз. финитно аппроксимируемой, если она полна относительно конечных алгебр. Если система конечно аксиоматизируема и финитно аппроксимируема, то она разрешима, т. е. для нее алгоритмически разрешима проблема распознавания выводимости. Матрица наз. характеристической, или адекватной, для системы S, если S полна относительно . Никакая из упомянутых выше пропозициональных систем М. л. не имеет конечной адекватной матрицы, но каждая из этих систем финитно аппроксимируема и поэтому разрешима. С другой стороны, всякое расширение системы S5 имеет конечную адекватную матрицу с одним выделенным значением. Свойством финитной аппроксимируемости обладают также все расширения системы Важным инструментом изучения М. л. являются Крипке модели, имеющие вид (), где W- множество "миров", "ситуаций", R- нек-рое отношение на — оценка пропозициональных переменных подмножествами W. Для отношение можно трактовать как "мир t возможен в мире s". Пару (W, R )наз. структурой Крипке, или остовом (встречается также термин шкала). Формула Аназ. общезначимой на остове (W, R), если для всякой оценки формула Аистинна в модели Крипке . Система S наз. полной по Крипке, если всякая не выводимая в S формула опровержима на нек-рой структуре Крипке, на к-рой общезначимы все выводимые в S формулы. Напр., система Т полна относительно структур (W, R), где R- рефлексивное отношение; S4 полна относительно структур с рефлексивным и транзитивным отношением. Среди конечно аксиоматизируемых расширений системы S4 существуют такие, к-рые не полны по Крипке (см. [7]). Для предикатных систем М. л. модели Крипке имеют вид — универсум мира — интерпретация предикатных символов в — оценка, сопоставляющая каждой предметной переменной нек-рый элемент множества Для систем, содержащих формулу Баркан, надо также потребовать, чтобы Модели Крипке имеют, как правило, более наглядную структуру, чем алгебраич. модели, поэтому часто они удобнее для изучения различных систем М. л. Лит.;[1] Lewis С. I., LangfordC. H., Symbolic Logic, 2 ed., N. Y., 1959; [2] Фейс Р., , [пер. с англ.], М., 1974; [3] Расева Е., Сикорский Р., Математика метаматематики, пер. с англ., М., 1972; [4] Минц Г.