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

Понятие модели Крипке (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 |= |= В. Теорема доказана.

Условные тавтологии

Чтобы охватить формулы, верные при дополнительных условиях (аксиомах), рассматриваются модели с фиксированной шкалой или набором шкал.

Формула А называется вернойв модели M = (W, R, h), если она верна для всех tÎW. Формула А называется тавтологией относительно шкалы, если она верна для любой модели с данной шкалой. Формула А называется тавтологией относительно класса шкал С, если она является тавтологией относительной каждой шкалы из класса С.

Теорема (о рефлексии). Пусть р – атом. Формула р ® р является тавтологией относительно шкалы (W, R), если и только если R – рефлексивное отношение (т.е. wRw для всех w Î W).

Доказательство. Пусть R – рефлексивно. Пусть М – модель со шкалой (W, R), tÎW – произвольный мир и пусть M, t |= р ® р. Поскольку модель М – произвольная, то р ® р – тавтология относительно шкалы (W, R).

Пусть, наоборот, р ® р – тавтология относительно (W, R). Пусть t Î W. Докажем, что (t, t) Î R. С этой целью определим модель М = (W, R, h), полагая (при фиксированном t)

h(p) = {u Î W : (t, u) Î R}.

Ясно, что M, t |= р. Но р ® р верно, стало быть, M, t |= р. Отсюда t Î h(p). Следовательно, (t, t) Î R, что и требовалось доказать.

Упражнение 5

Доказать, что если R Í W ´ W – рефлексивно, то А ® А – тавтология относительно шкалы (W, R) для любой формулы А.

Формула (А ® В) ® ( А ® В) является тавтологией относительно класса всех шкал Крипке. Такие формулы называют естественно истинными. Формула А ® А верна относительно некоторого класса шкал. Такие формулы называются условно истинными.