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

Фиксируется бесконечное счётное множество Р. Элементы из Р называются простыми высказываниями, или (пропозициональными) атомами, и обычно обозначаются через 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 – формулы.