Семантика темпоральной логики
Понятие модели Крипке (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) для любой формулы А.
Формула (А ® В) ® ( А ® В) является тавтологией относительно класса всех шкал Крипке. Такие формулы называют естественно истинными. Формула А ® А верна относительно некоторого класса шкал. Такие формулы называются условно истинными.