Синтаксис модальной логики

Модальная и темпоральная логикИ

Модальная логика восходит к начатым Аристотелем исследованиям утверждений, содержащих слова: «неизбежно» и «возможно». В действительности модальностями такого вида богаты и человеческий, и научный языки, например: «обязательно» и «допустимо», «всегда» и «иногда». Поэтому проблемы модальной логики интересовали математиков всегда. Модальная логика перенесла бурное развитие в 60-х годах ХХ века, благодаря методу интерпретации модальностей с помощью моделей Крипке.

Темпоральная логика изучает высказывания, содержащие слова, связанные со временем, например: «будет всегда» и «произойдёт», «завтра» и «вчера». Её основатель – Артур Прайер.

В 80-х годах ХХ века интерес к модальной логике повысился в связи с новым подходом к алгоритмической логике Хоара, применяемой для доказательства правильности программ. Этот подход был основан Воганом Праттом, предложившим рассматривать каждую программу как особый вид модальности.

Синтаксис модальной логики

Фиксируется бесконечное счётное множество Р. Элементы из Р называются простымивысказываниями, или (пропозициональными) атомами, и обычно обозначаются через p, q, r, или p₁, p₂, p₃, …. (Модальные) формулы строятся из атомов и символа 1 («истина») с помощью логических связок & и Ø, и модальности («квадрат») по индукции:

1) каждый атом p Î P является формулой;

2) символ 1 является формулой;

3) если A и B – формулы, то ØA, A & B, A – формулы;

4) каждая формула построена по этим трём правилам.

Темпоральные формулы используют вместо символа квадрата символы: [F] и [P] (будущего и прошлого). Вместо А применяется запись: [F]A или [P]A. Для образования темпоральных формул применяются правила 1, 2, 4 и правило:

3¢) если А и В – формулы, то ØA, A & B, [F]A и [P]A – формулы.