Смысловые значения модальностей

Уточним, что мы понимаем под символами: , , [F], [P], <F>, <P>. Значения этих символов зависят от области применения и могут обладать неодинаковыми свойствами. Например, А = «А обязательно», А = «А возможно» обладают свойством А  А («Если сегодня в Москве обязательно идёт дождь, то в Москве идёт дождь»). А модальности А = «необходимо А», А = «допустимо А» не обладают этим свойством. Например, высказывание: «Если необходим дождь, то идёт дождь» – может быть ложным.

Другие значения модальностей: А = «А известно» и А = «А предположительно», А = «А всегда верно» и А = «А иногда верно». При доказательстве правильности программ используются модальности А = «после окончания работы программы будет верно А» и А = «программа может закончиться так, что А станет верным». Темпоральные связки в зависимости от области применения могут принимать значения: [F]А = «А будет всегда верно», <F>А = «А будет верно в некоторый момент»; или [F]А = «А будет верно всегда, начиная с этого момента времени», <F>А = «А верно сейчас или будет верно потом». Значения [P]А и <P>А определяются симметрично к [F]А и <F>А и относятся к прошедшему времени. Связки «завтра» и «вчера», «до тех пор, пока не» и «с тех пор, как» будут определены позже.

Заметим, что , [F], [P] похожи на квантор всеобщности, а , <F>, <P> – на квантор существования.

Примеры

Рассмотрим смысловые значения формул модальной логики:

А = «известно, что А известно»;

А = «необходимо, чтобы А было допустимо»;

А  А = «если известно, что А верно, то А – верно»;

[P][P]А  [P]А = «если всегда было верно, что А было верно всегда, то А всегда было верно»;

А  А = «если известно, что А известно, то А известно»;

А  А = «если агент знает А, то он знает, что он знает А»;

А  [F]<P>А = «если А верно, то в будущем всегда будет верно, что в некоторый момент прошлого было верно А»;

<P>А = «возможно, что А не было верным никогда»;

А & В  (А & В) = «если А и В известны, то известно А & В».