Математическая энциклопедия - модальная логика

область логики, в к-рой наряду с обычными высказываниями рассматриваются модальные высказывания, т. е. высказывания типа "необходимо, что.,.", "возможно, что..." и т. п. В математич. логике рассматриваются различные формальные системы М. л., выявляется взаимосвязь между этими системами, изучаются их интерпретации.

Элементы М. л. имелись по существу еще у Аристотеля (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 предметных переменных, предикатных символов и кванторов (или одного из них). Также добавляются обычные схемы аксиом и правила вывода для кванторов. Кроме того, иногда добавляют и другие аксиомы, описывающие действие модальных операторов на кванторы, напр. т. н. формулу Баркан:

Алгебраич. интерпретация систем М. л. задается нек-рой алгеброй (называемой также матрицей)