logo
МЛиТА 6 - 7

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

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

Аксиомы

  1. Формулы D(B1, … Bn), где D(p1, …, pn) – пропозициональные тавтологии.

  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 (отражение).

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

; .

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

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

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

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

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

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

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

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

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

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