Термин модальной логики
В модальной логике модальная глубина формулы является самой глубокой вложенностью из модальные операторы (обычно и ). Модальные формулы без модальных операторов имеют модальную глубину, равную нулю.
Содержание
- 1 Определение
- 2 Пример
- 3 Модальная глубина и семантика
- 4 Ссылки
Определение
Модальная глубина может быть определена следующим образом. Пусть будет функцией, которая вычисляет модальную глубину для модальной формулы :
- , где - атомарная формула.
Пример
Th е следующее вычисление дает модальную глубину :
Модальная глубина и семантика
Модальная глубина формулы указывает, «как далеко» нужно смотреть в Крипке модель при проверке действительности формулы. Для каждого модального оператора необходимо перейти от мира в модели к миру, доступному через отношение доступности. Модальная глубина указывает на самую длинную «цепочку» переходов от одного мира к другому, которая необходима для проверки правильности формулы.
Например, чтобы проверить, , нужно проверить, есть ли существует доступный мир , для которого . Если это так, нужно проверить, существует ли еще такой мир , такой что и доступны из . Мы сделали два шага от мира (от до и от до ) в модели, чтобы определить, верна ли формула; это, по определению, модальная глубина этой формулы.
Модальная глубина - это верхняя граница (включительно) количества переходов, как и для блоков, модальная формула также верна, когда в мире нет доступных миров (т. Е. сохраняется для всех в мире при , где - это набор миров, а - отношение доступности). Чтобы проверить, соответствует ли , может потребоваться выполнить два шага в модели, но это может быть меньше, в зависимости от структуры модели. Предположим, что в нет доступных миров; формула теперь тривиально выполняется в силу предыдущего наблюдения о действительности формул с прямоугольником в качестве внешнего оператора.
Ссылки