Семантика темпоральной логики

Понятие модели Крипке (W, R, h) такое же, как для модальной логики. Определяется истинность формул [F]А и [P]А, вместо А.

Если tRu, то говорят, что t – прошлое для u, а u – будущее для t. (Напомним, что tRu означает (t, u) Î R.)

Обычно отношение R предполагается транзитивным в том смысле, что из tRu и uRv следует: tRv (исключением являются шкалы с циклическим временем). Утверждения для интерпретации А заменяются на следующие:

1) M, t |= [F]А, если и только если M, u |= А для всех u Î W таких, что tRu.

2) M, t |= [P]А, если и только если M, u |= А для всех u Î W таких, что uRt.

Упражнение 3

Доказать утверждения:

1) M, t |= <F>А, если и только если существует u Î W такой, что tRu и M, u |= А.

2) M, t |= <P>А, если и только если существует такой u Î W, что uRt и M, u |= А.

Тавтологии

Будем рассматривать тавтологии относительно семантики Крипке. Формула А называется тавтологией если M, t |= А для любых модели M = (W, R, h) и мира t Î W. Формула А называется выполнимой, если существуют такие модель М и мир t, что
M, t |= А. Формулы А и В называются эквивалентными, если для любых модели М и мира t утверждение M, t |= А равносильно утверждению M, t |= В.

Упражнение 4

Доказать утверждения:

1) А тавтология, если и только если ØА невыполнимо;

2) А выполнимо, если и только если ØА не тавтология;

3) А и В эквивалентны тогда и только тогда, когда А « В – тавтология.

4) тавтологии и исчисления высказываний являются тавтологиями модальной логики;

5) Ø А эквивалентно àØА;

6) Ø (А ® В) эквивалентно à(А & ØВ).

Теорема (о нормальности). Для любых формул А и В имеет место тавтология:

(А ® В) ® ( А ® В).

Доказательство. Пусть M = (W, R, h) – модель Крипке, t Î W – мир. Предположим выполнение M, t |= (А ® В). Докажем, что А ® В верно в мире t. С этой целью докажем, что из M, t |= А следует M, t |= В. Пусть u Î W – мир, для которого
(t, u) Î R. Если верно M, t |= А, то M, u |= А. По предположению, M, t |= |= (А ® В), значит, M, u |= А ® В. Получаем из M, u |= А и M, u |= А ® В, что M, u |= |= В. Теорема доказана.