Система Гильберта для темпоральной логики

Формальная теория K_t состоит из следующих аксиом и правил вывода.

Аксиомы

1. Формулы D(B₁, … B_n), где D(p₁, …, p_n) – пропозициональные тавтологии.

2. [F](A  B)  ([F]A  [F]B); [P](A  B)  ([P]A  [P]B) (нормальность).

3. [F]A  [F][F]A (транзитивность).

4. A  [F]<P>A; A  [P]<F>A (отражение).

Правила вывода

; .

Здесь А, В, В₁, …, В_n – темпоральные формулы, возможно, содержащие [F] и [P].

Исходя из того, что для любой интерпретации с помощью шкалы Крипке формулы A  [F]<P>A и A  [P]<F>A будут тавтологиями, легко доказать следующую теорему корректности и полноты:

Теорема 1. Для любой темпоральной формулы А утверждение K_tA верно, если и только если А – тавтология относительно каждой шкалы Крипке (W, R), имеющей транзитивное отношение R. Здесь K_t ,означает, что А – теорема в формальной теории K_t.

Потоки времени

В темпоральной логике используются нерефлексивные транзитивные шкалы Крипке.

Шкала Крипке (W, <) называется потоком времени, если

1. x  W ((x < x)),

2. x, y, z  W (x < y & y < z  x < z).

Если t < v, то v называется будущим для t, а t – прошлым для v.

Теорема 2. Для любой темпоральной формулы А утверждение K_tA верно, если и только если А – тавтология относительно всех потоков времени.