Линейные потоки времени

Чтобы ограничить виды потоков времени, к системе Kt добавляются аксиомы. Аксиомы <F>1 и <P>1 означают отсутствие наименьшего и наибольшего t  W.

Истинность аксиомы [F][F]A  [F]A равносильна свойству плотности отношения доступности:

tu (t < u  v(t < v <u)).

Например, Q и R – плотные линейно упорядоченные множества, а Z – нет.

Для того чтобы потоки времени были линейно упорядочены, т.е. удовлетворяли условию:

tu (t < u  t = u  u < t),

добавляется аксиома

<F>A&<F>B  <F>(A&B)<F>(A&<F>B)(B&<F>A)

(или её зеркальное отображение).

В случае шкалы (Z, <) добавляются аксиомы:

[F]([F]A  A)  (<F>[F]A  [F]A),

[P]([P]A  A)  (<P>[P]A  [P]A).

Для шкалы (N, <) добавляются аксиомы:

[F]([F]A  A)  (<F>[F]A  [F]A),

[P]([P]A  A)  [P]A.

Для (R, <) добавляются аксиомы, обеспечивающие плотность отношения порядка и отсутствие максимального и минимального элементов. Добавляется аксиома Прайера:

<F>[F]  <F>A  <F>)[F]A& <P>[F]A).