logo
МЛиТА 6 - 7

Модели Крипке

Чтобы задать интерпретацию модальных формул, надо задать функцию на атомах (из P). Значения этой функции зависят также от состояний. Оценкой называется функция h: P  P(W), определённая на множестве всех атомов и принимающая значения во множестве всех подмножеств множества W. Атом p называется истинным в мире w, если w  h(p), и ложным в других случаях.

Тройка (W, R, h) называется моделью Крипке. Шкала Крипке может быть превращена в модели Крипке в зависимости от функции оценки h.

Пусть М = (W, R, h) – модель Крипке. Для формулы А и мира t  W определим утверждение M, t |= A с помощью индукции:

  1. если р – атом, то M, t |= р тогда и только тогда, когда t  h(p);

  2. M, t |= 1 (всегда);

  3. M, t |= А тогда и только тогда, когда утверждение M, t |= А ложно;

  4. M, t |= А & В тогда и только тогда, когда M, t |= А и M, t |= В;

  5. M, t |= А тогда и только тогда, когда М, u |= А для всех таких u  W, что tRu.

Запись: tRu означает, что (t, u)  R. Выражение M, t |= А читается: «М удовлетворяет в мире t формуле А», или «формула А выполняется в мире t для модели М». Другие обозначения: М |= А(t), М |=t А, .

Легко видеть, что имеют место утверждения, дополняющие свойства 1 – 5:

  1. M, t |= А  В, если и только если M, t |= А или M, t |= В;

  2. M, t |= (А  В) если и только если из M, t |= А следует, что M, t |= В;

  3. M, t |= А, если и только если M, t |= А для некоторого u  W такого, что tRu.