Выбор операторов

Можно сформулировать темпоральную логику для применений одного типа, выбирая отдельные логические связки и темпоральные операторы. Булевы связки &,  и символ 1 включаются всегда.

Примеры

Темпоральная логика FT состоит из формул, построенных из символа 1 и атомов с помощью &, , <F> и Т. Она включает оператор [F], ибо [F] = <F>.

Логика FPTY состоит из формул, построенных из символа 1 и атомов &, , <F>, <P>, T и Y.

Логика US состоит из формул, построенных из символа 1 и атомов с помощью &, , U, S.

В общем случае <F> и <P> невозможно выразить операторы T и Y. Тем не менее, операторы T и Y бывают нужны. Логика US включает формулы из FPTY:

<F>A = 1UA, <P>A = 1SA, TA = 0UA, YA = 0SA.

Стандартный перевод формул логики US основывается на определении:

(B U A)*(x) = y(y > x & A*(y)) & z(x < z < y  B*(x)).

Перевод S определяется симметрично.

Пусть С – класс потоков времени. Темпоральная логика (такая, как FP или US) называется экспрессивно полной относительно С, если для любой формулы первого порядка (х, Р₁, …, Р_n) существует формула А(Р₁, …, Р_n) темпоральной логики, для которой А*(х, Р₁*, …, Р_n*) эквивалентна (х, Р₁*, …, Р_n*) над С. То есть, для любой модели М с потоком времени из С верно:

M |= x (A*(x)  (x)).

Теорема 3 (Кемп). Темпоральная логика US экспрессивно полна над любым классом полных по Дедекинду линейных потоков времени.

Под полным по Дедекинду линейным потоком времени (T, <) понимается линейно упорядоченное множество, в котором нет таких непустых подмножеств X,YT, таких, что

1. X  Y = T;

2. x < y для всех x  X и y  Y;

3. X не имеет наибольшего, а Y – наименьшего элементов.