Оглавление:
Главная страница djvu-student.narod.ru
Электрический привод
Математическая логика
Биология
Бжд
История
Психология
Литература
Экономика
Химия
Информатика
Юриспруденция
Высшая математика
Школьная математика
Сопротивление материалов
Теоретическая механика
Теоретические основы электротехники
Физика
Программы, бесплатный софт
Обратная связь
Наша кнопка


Скачать эту страницу
в формате PDF, 220 КБ

Математическая логика, учебник

Учебник, часть 6

6. Модальная и темпоральная логикИ

Модальная логика восходит к начатым Аристотелем исследованиям утверждений, содержащих слова: «неизбежно» и «возможно». В действительности модальностями такого вида богаты и человеческий, и научный языки, например: «обязательно» и «допустимо», «всегда» и «иногда». Поэтому проблемы модальной логики интересовали математиков всегда. Модальная логика перенесла бурное развитие в 60-х годах ХХ века, благодаря методу интерпретации модальностей с помощью моделей Крипке.

Темпоральная логика изучает высказывания, содержащие слова, связанные со временем, например: «будет всегда» и «произойдёт», «завтра» и «вчера». Её основатель – Артур Прайер.

В 80-х годах ХХ века интерес к модальной логике повысился в связи с новым подходом к алгоритмической логике Хоара, применяемой для доказательства правильности программ. Этот подход был основан Воганом Праттом, предложившим рассматривать каждую программу как особый вид модальности.

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

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

Дополнительные логические связки

Символ 0 (ложь) и связки , ,  введём как сокращенные записи операций:
0 = 1, А  В = (А & В), А  В = (А &В), А  В = (А  В) & (В  А). Положим: А = А для модальности. В случае темпоральных формул введём сокращения: <F>A = [F]А и <P>A = [P]А. В некоторых случаях сокращения 0,  и  будут использоваться как самостоятельные символы.

Замечание. Обычно вместо [F]А и [P]А применяется запись: GA и HA соответственно. В этом случае вместо <F>A и <P>A пишут: FA и PA.

Приоритеты операций

С целью уменьшения количества скобок будем предполагать, что приоритеты унарных связок выше, чем приоритеты бинарных и располагаются в порядке убывания следующим образом:

, , , [F], [P], <F>, <P>, &, , , .

Для унарных операций взаимные приоритеты не имеют значения (и могут считаться равными). Например, А & В  С означает: (((А) & ( (В)))  С).

Смысловые значения модальностей

Уточним, что мы понимаем под символами: , , [F], [P], <F>, <P>. Значения этих символов зависят от области применения и могут обладать неодинаковыми свойствами. Например, А = «А обязательно», А = «А возможно» обладают свойством А  А («Если сегодня в Москве обязательно идёт дождь, то в Москве идёт дождь»). А модальности А = «необходимо А», А = «допустимо А» не обладают этим свойством. Например, высказывание: «Если необходим дождь, то идёт дождь» – может быть ложным.

Другие значения модальностей: А = «А известно» и А = «А предположительно», А = «А всегда верно» и А = «А иногда верно». При доказательстве правильности программ используются модальности А = «после окончания работы программы будет верно А» и А = «программа может закончиться так, что А станет верным». Темпоральные связки в зависимости от области применения могут принимать значения: [F]А = «А будет всегда верно», <F>А = «А будет верно в некоторый момент»; или
[F]А = «А будет верно всегда, начиная с этого момента времени», <F>А = «А верно сейчас или будет верно потом». Значения [P]А и <P>А определяются симметрично к [F]А и <F>А и относятся к прошедшему времени. Связки «завтра» и «вчера», «до тех пор, пока не» и «с тех пор, как» будут определены позже.

Заметим, что , [F], [P] похожи на квантор всеобщности, а , <F>, <P> – на квантор существования.

Примеры

Рассмотрим смысловые значения формул модальной логики:

А = «известно, что А известно»;

А = «необходимо, чтобы А было допустимо»;

А  А = «если известно, что А верно, то А – верно»;

[P][P]А  [P]А = «если всегда было верно, что А было верно всегда, то А всегда было верно»;

А  А = «если известно, что А известно, то А известно»;

А  А = «если агент знает А, то он знает, что он знает А»;

А  [F]<P>А = «если А верно, то в будущем всегда будет верно, что в некоторый момент прошлого было верно А»;

<P>А = «возможно, что А не было верным никогда»;

А & В  (А & В) = «если А и В известны, то известно А & В».

6.2. Семантика модальной логики

Под семантикой понимается метод интерпретаций формул как истинных или ложных. Поскольку слова можно толковать по-разному, то выделяются семантики, удовлетворяющие дополнительным условиям. В частности, выделяются семантики, для которых истинна формула:

(p q) (p q).

Такие семантики относятся к нормальным. Рассмотрим одну из них.

Семантика Крипке

Рассматривается множество миров. Модальное высказывание А считается истинным, если А истинно в некоторых из возможных миров. Истинность обычных формул измеряется по отношению к текущему миру. (Идея принадлежит Лейбницу, и была разработана Сеулом Крипке).

Возьмём произвольное множество W; его элементы будем называть мирами или состояниями. Рассмотрим произвольное бинарное отношение R на W. Если значение предиката R(t, w) равно 1, то w называется возможным или доступным миром для t.

Определение. Пара множеств (W, R), где W – непустое множество, а RWW – бинарное отношение на W, называется шкалой Крипке. Отношение R называется отношением доступности.


Пример 1

Пусть W = {1, 2, 3, 4, 5}, R = {(1, 1), (1, 2), (2, 3), (1, 5), (5, 4), (4, 4), (4, 3)}. Шкалу Крипке (W, R) можно рассматривать как ориентированный граф, вершинами которого служат элементы из W, а рёбрами – пары, принадлежащие R. Например, для мира 1 будут доступны миры 1, 2 и 5, ибо (1, 1), (1, 2) и (1, 5) принадлежат R.

Пример 2

Каждое частично упорядоченное множество (Х, ) будет шкалой Крипке, имеющей множество миров Х и отношение доступности . В частности, N = (, ), (Z, ), (Q, ), (R, ) – множества натуральных, целых, рациональных и действительных чисел, с обычным отношением порядка будут составлять шкалы Крипке.

Пример 3

Существуют шкалы с циклами, например, W = {1, 2, 3, 4} с отношением R = {(1, 2), (2, 3), (3, 4), (4, 1)}.

Можно привести искусственные примеры, такие, как шкала рекурсии Макинсона (, R), где R состоит из пар (m, n), для которых m  n + 1.

Модели Крипке

Чтобы задать интерпретацию модальных формул, надо задать функцию на атомах (из P). Значения этой функции зависят также от состояний. Оценкой называется функция h: P  P(W), определённая на множестве всех атомов и принимающая значения во множестве всех подмножеств множества W. Атом p называется истинным в мире w, если w  h(p), и ложным в других случаях.

Тройка (W, R, h) называется моделью Крипке. Шкала Крипке может быть превращена в модели Крипке в зависимости от функции оценки h.

Пусть М = (W, R, h) – модель Крипке. Для формулы А и мира t  W определим утверждение M, t |= A с помощью индукции:

  1. если р – атом, то M, t |= р тогда и только тогда, когда t  h(p);

  2. M, t |= 1 (всегда);

  3. M, t |= А тогда и только тогда, когда утверждение M, t |= А ложно;

  4. M, t |= А & В тогда и только тогда, когда M, t |= А и M, t |= В;

  5. M, t |= А тогда и только тогда, когда М, u |= А для всех таких u  W, что tRu.

Запись: tRu означает, что (t, u)  R. Выражение M, t |= А читается: «М удовлетворяет в мире t формуле А», или «формула А выполняется в мире t для модели М». Другие обозначения: М |= А(t), М |=t А, .

Легко видеть, что имеют место утверждения, дополняющие свойства 1 – 5:

  1. M, t |= А  В, если и только если M, t |= А или M, t |= В;

  2. M, t |= (А  В) если и только если из M, t |= А следует, что M, t |= В;

  3. M, t |= А, если и только если M, u |= А для некоторого u  W такого, что tRu.

Упражнение 1

Следующие утверждения предлагается проверить самостоятельно:

  1. M, t |= (А  В), если и только если M, t |= А & В;

  2. M, t |= А, если и только если M, t |= А;

  3. M, t |= А, если и только если M, t |= А.

Упражнение 2

Пусть p, q  P. Рассмотрим модель M = (W, R, h), где W = {1, 2, 3, 4, 5},
R = {(1, 1), (1, 2), (2, 3), (1, 5), (5, 4), (4, 4), (4, 3)}, h(p) = {1, 2, 5}, h(q) = {1, 3, 4} и
h(r) =  для всех r  {p, q}.

(Высказывание р верно в мирах 1, 2 и 5; q – в 1, 3 и 4). Проверить утверждения:

  1. р верно в 1 и 3, ложно в 4;

  2. р верно в 3, 0 верно в 3;

  3. q & q верно в 1, q ложно в 1;

  4. q, q оба верны в 2, ибо только 3 доступно из 2;

  5. 1  q верно во всех мирах, т.е. эта формула – тавтология модели М.

Семантика темпоральной логики

Понятие модели Крипке (W, R, h) такое же, как для модальной логики. Определяется истинность формул [F]А и [P]А, вместо А.

Если tRu, то говорят, что t – прошлое для u, а u – будущее для t. (Напомним, что tRu означает (t, u)  R.)

Обычно отношение R предполагается транзитивным в том смысле, что из tRu и uRv следует: tRv (исключением являются шкалы с циклическим временем). Утверждения для интерпретации А заменяются на следующие:

  1. M, t |= [F]А, если и только если M, u |= А для всех u  W таких, что tRu.

  2. M, t |= [P]А, если и только если M, u |= А для всех u  W таких, что uRt.

Упражнение 3

Доказать утверждения:

  1. M, t |= <F>А, если и только если существует u  W такой, что tRu и M, u |= А.

  2. M, t |= <P>А, если и только если существует такой u  W, что uRt и M, u |= А.

Тавтологии

Будем рассматривать тавтологии относительно семантики Крипке. Формула А называется тавтологией если M, t |= А для любых модели M = (W, R, h) и мира t  W. Формула А называется выполнимой, если существуют такие модель М и мир t, что
M, t |= А. Формулы А и В называются эквивалентными, если для любых модели М и мира t утверждение M, t |= А равносильно утверждению M, t |= В.

Упражнение 4

Доказать утверждения:

  1. А тавтология, если и только если А невыполнимо;

  2. А выполнимо, если и только если А не тавтология;

  3. А и В эквивалентны тогда и только тогда, когда А  В – тавтология.

  4. тавтологии исчисления высказываний являются тавтологиями модальной логики;

  5. А эквивалентно А;

  6. (А  В) эквивалентно (А & В).

Теорема (о нормальности). Для любых формул А и В имеет место тавтология:

(А  В)  (А  В).


Доказательство. Пусть M = (W, R, h) – модель Крипке, t  W – мир. Предположим выполнение M, t |= (А  В). Докажем, что А  В верно в мире t. С этой целью докажем, что из M, t |= А следует M, t |= В. Пусть u  W – мир, для которого
(t, u)  R. Если верно M, t |= А, то M, u |= А. По предположению, M, t |= (А  В), значит, M, u |= А  В. Получаем из M, u |= А и M, u |= А  В, что M, u |= В. Теорема доказана.

Условные тавтологии

Чтобы охватить формулы, верные при дополнительных условиях (аксиомах), рассматриваются модели с фиксированной шкалой или набором шкал.

Формула А называется верной в модели M = (W, R, h), если она верна для всех tW. Формула А называется тавтологией относительно шкалы, если она верна для любой модели с данной шкалой. Формула А называется тавтологией относительно класса шкал С, если она является тавтологией относительной каждой шкалы из класса С.

Теорема (о рефлексии). Пусть р – атом. Формула р р является тавтологией относительно шкалы (W, R), если и только если R – рефлексивное отношение (т.е. wRw для всех w W).

Доказательство. Пусть R – рефлексивно. Пусть М – модель со шкалой (W, R), tW – произвольный мир. Если M, t |= р, то M, u |= р для каждого такого uW, что (t,u)  R. В силу рефлексивности в этом случае имеет место M, t |= р. Следовательно, M, t |= р  р. Поскольку модель М – произвольная, то р  р – тавтология относительно шкалы (W, R).

Пусть, наоборот, р  р – тавтология относительно (W, R). Пусть t  W. Докажем, что (t, t)  R. С этой целью определим модель М = (W, R, h), полагая (при фиксированном t)

h(p) = {u W : (t, u) R}.

Ясно, что M, t |= р. Но р  р верно, стало быть, M, t |= р. Отсюда t  h(p). Следовательно, (t, t)  R, что и требовалось доказать.

Упражнение 5

Доказать, что если R  W  W – рефлексивно, то А  А – тавтология относительно шкалы (W, R) для любой формулы А.

Формула (А  В)  (А  В) является тавтологией относительно класса всех шкал Крипке. Такие формулы называют естественно истинными. Формула А  А верна относительно некоторого класса шкал. Такие формулы называются условно истинными.

6.3. Алгоритмическая логика Хоара

Интуитивно программа понимается как набор операторов, переводящих машину из одних состояний в другие. Хоар предложил для отладки и верификации программ рассматривать формулы, описывающие состояния машины перед выполнением (предусловие) и после выполнения (постусловие) программы. Программе  сопоставлялась запись: {А}{В}, означающая, что предусловие описывается формулой А, а постусловие формулой В. Пратт предложил запись: А  []В – если перед выполнением программы состояние машины описывается формулой А, то после выполнения верна формула В. Это позволило описывать вычислительные процессы, состоящие из комплексов программ, с помощью модальной логики, рассматривая каждую программу как модальность.

Пропозициональная динамическая логика

Пусть 0 – произвольное множество. Его элементы называются базисными программами. Предположим, что   0 – такое множество слов, что вместе с любыми
1, 2   оно содержит:

  1. 1  2 (неопределённый выбор одной из программ 1 или 2);

  2. 1 ; 2 (выполнение 1 ,затем 2);

  3. 1* (выполнение 1 конечное, возможно нулевое, количество раз);

  4. 1  2 (одновременное выполнение программ 1 или 2).

Элементы из  будем называть программами. Рассмотрим атомы из Р как простые высказывания о состояниях машины, в которую загружаются программы. Для каждой программы    обозначим через [] соответствующую ей модальность. Определим формулы пропозициональной динамической логики PDL по индукции:

  1. атомы р  Р – формулы;

  2. А & В, А, []А – формулы для любых формул А и В, и элемента   ;

  3. все формулы PDL составляются с помощью правил 1 – 2.

Введём обозначение: <>А как сокращение для []А.

Для каждой формулы А определим программу: А?  , тестирующую, верна ли формула А. Эта программа заканчивает работу, если формула А верна, и зависает (аварийно завершает работу), если нет. Эта программа вводится с целью интерпретации оператора

if (A) then 1 else 2

как программы

(А?; 1)  ((А)? ; 2)  .

Семантика пропозициональной динамической логики

Пусть 0 – множество базисных программ,  – множество всех программ, Р – атомные формулы, F(P) – все формулы, W – множество состояний машины, в которой могут работать программы . Для каждого    определена модальность []. Стало быть, мы должны каждому  поставить в соответствие некоторое отношение доступности R  W  W.

Шкала Крипке (или система переходов) будет состоять из пары: (W, (R)), где W – множество состояний, а Rотношения R  W  W.

Программу можно интерпретировать как множество пар (x, y)  R таких, что после выполнения программы  машина из состояния х перейдёт в состояние y. Каждому атому p  P ставится в соответствие подмножество h(p)  W состояний, при которых высказывание р верно.

Интерпретацией называется тройка M = (W, (R), h), состоящая из шкалы Крипке и оценки h : P  P(W), удовлетворяющих соотношениям:

  1. R = R R;

  2. R ; = R R;

  3. ;

  4. RA? = {(x, x) : x W и M, x |= A}.

Здесь R* – наименьшее рефлексивное транзитивное отношение, содержащее R. Расширим h на множество формул F(P), полагая t  h(A), если и только если M, t |= A. Получим соотношения:

  1. h(A B) = h(A) h(B);

  2. h(A) = W \ h(A);

  3. h(<>A) = {t  W : (t, u)  R для некоторого u  h(A)}.

В некоторых случаях под семантикой логики PDL понимают шкалу с расширенной на F(P) оценкой, удовлетворяющие соотношениям 1 – 7.

Аксиомы PDL

Можно ожидать, что для любых формулы А и программы    формула <*>А, (означающая возможность того, что после циклического применения  машина перейдёт в состояние, удовлетворяющее формуле А), будет равносильна формуле А  <; *>А, (означающей, что верно А, или А будет, возможно, верно после применения  не менее, чем 1 раз). Получим аксиому:

<*>А  А  <; *> А.

Аналогично, исходя из других соображений, получаем аксиомы PDL и формальную теорию:

  1. все тавтологии исчисления высказываний;

  2. <>A & <>B <>(A & B);

  3. <>(A B) <>A <>B);

  4. < >A <>A <>A;

  5. < ; >A <><>A;

  6. <A?>B A&B;

  7. A <><*>A <*>A;

  8. <*>A A <*> (A & <>A).

Аксиомы 1 – 3 стандартны для модальных логик. Аксиома 8 равносильна аксиоме Сегерберга:

[*](A []A) (A [*]A)

и называется аксиомой PDL – индукции.

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

; .

Для формальной теории PDL справедливы теорема корректности и полноты.

Логика Хоара

Как мы уже отмечали, логика Хоара предназначалась для дедуктивного доказательства правильности программ. Её формулами являются тройки {А}{В}, состоящие из предусловия А, программы  и постусловия В. Приведём форму записи, применяемой Хоаром, и её перевод на язык исчисления PDL:




Форма {A}{B} называется тройкой Хоара. Логика Хоара является формальной теорией для вывода с помощью троек Хоара. Преобразуя аксиомы языка PDL, можно получить следующие правила вывода логики Хоара:

(композиция)

(условие)

(цикл)

(следствие).

6.4. Системы Гильберта

Опишем формальную теорию, которая называется системой K:

Аксиомы

  1. Если А(Р1, …, Рn) – тавтология исчисления высказываний, а В1, …, Вn – модальные формулы, то А(В1, …, Вn) – аксиома системы K (пропозициональные тавтологии).

  2. Для любых формул А и В формула (А  В)  (А  В) является аксиомой системы K (аксиома нормальности).

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

; .

Формальная теория, содержащая систему K, называется системой Гильберта.

Строгие системы Гильберта

Добавляя аксиомы к системе K, получаем её усиления. Эти аксиомы соответствуют различным (указанным далее в квадратных скобках) свойствам шкал Крипке (речь о свойствах пойдёт далее):

Т: А  А [рефлексивность];

D: А  А [определённость всюду];

4: А  А [транзитивность];

В: А  А [симметричность];

5: А  А [с аксиомой Т – отношение эквивалентности].

Система К вместе с аксиомой Т обозначается через KТ или S. Такое определение записывается как:

S = K + {А  А}.

Аналогично, добавляя к K другие аксиомы, получаем следующие системы Гильберта:

K4 = K + {А  А };

S4 = K + {А  А, А  А};

S5 = K + {А  А, А  А}.

Выводимость. Пусть H – система Гильберта. (Согласно определению, она должна содержать аксиомы и правила вывода системы K).

Определение. Запись HA означает, что существует последовательность формул А1, …, Аn таких, что

1) An = A;

2) Каждая формула Ai является либо аксиомой системы H, либо получена аз некоторых формул последовательности A1, …, Ai-1 с помощью правил вывода системы H.

В этом случае А называется теоремой в H, а последовательность A1, …, Anвыводом формулы (или доказательством теоремы) А. Число n называется длиной вывода (доказательства).

Пример 1

Последовательность:

A & B A, (A & B A), (A & B A) ((A & B) A), (A & B) A

является доказательством длины 4 теоремы (A & B)  A.

Корректность и полнота систем Гильберта

Можно показать, что KA имеет место тогда и только тогда, когда А – тавтология; утверждение A равносильно тому, что А – тавтология относительно класса всех рефлексивных шкал Крипке; S4A равносильно тому, что А – тавтология относительно класса транзитивных шкал.

Свойства шкал Крипке

Мы раньше доказывали, что аксиома Т (q  q) является тавтологией относительно шкалы F = (W, R) тогда и только тогда, когда R – рефлексивно. Можно доказать, что аксиома 4 (q  q) является тавтологией относительно F = (W, R), если и только если R транзитивно. Аксиома D(q  q) будет тавтологией относительно (W, R) тогда и только тогда, когда Dom R = W (т.е. tWuW (tRu)). Возникает вопрос о способе нахождения свойства шкал, относительно которых заданная формула является тавтологией. Опишем один из путей решения этой проблемы, принадлежащий Салквисту. С этой целью рассмотрим символы: 1, 0, &, , ,  как примитивные (не связанные между собой). Но А  В будет по-прежнему сокращением для формулы: (А & В).

Строго позитивными будем называть формулы: р, p, p, …, где р – атом. Позитивной называется формула, не использующая . Негативная формула – это отрицание некоторой позитивной формулы. Несвязной называется формула, полученная из негативных и строго позитивных формул с помощью операций & и . Формулой Салквиста называется отрицание некоторой несвязной формулы. Например:

формула р  р эквивалентна формуле Салквиста ([p] & [p]);

р  р – формуле Салквиста ([р] & [р])

и формуле Салквиста ([р] & [р]);

р  р – формулам Салквиста ([р] & [р]) и ([р] & [р]);

р  р – формуле Салквиста ([р] & [р]).

Однако (pp) не эквивалентна никакой формуле Салквиста.

Теорема Салквиста. В 1973 году Салквист установил, что каждой формуле Салквиста соответствует некоторое свойство шкалы. Перед формулировкой этой теоремы введём определения и докажем лемму.

Пусть F = (W, R) – шкала Крипке, и пусть h, h : P  P(W) – оценки. Полагая hh, если h(p)  h(p) для всех p  P, получим отношение порядка на множестве оценок. Если hh, то h называется сужением h, а h – расширением h.

Лемма. Пусть А – позитивная формула, F = (W, R) – шкала Крипке, h h – оценки, t W – произвольный мир. Тогда, если (W, R, h), t |= A, то (W, R, h), t |= A.

Доказательство. С помощью индукции по количеству логических связок и модальностей в формуле А. Для атомов р:

(W, R, h), t |= р  t  h(p)  t  h(p)  (W, R, h), t |= р.

Если А = 1, или А = 0, то утверждение справедливо. Случаи А & В и А  В проверяются легко. Случай А не возникает в силу позитивности формулы А. Докажем утверждение для А (аналогично для А), в предположении, что для А оно верно. Пусть (W, R, h), t |= А. Тогда для всех u  W, для которых tRu, будет верно (W, R, h),
u |= А. Для А утверждение верно, значит, (W, R, h), u |= А. Следовательно, (W, R, h),
t |= А, что и требовалось доказать.

Мы можем переводить модальные формулы в формулы языка первого порядка.

Пусть х – переменная. Переводом формулы А будет некоторая формула А*(х) языка первого порядка, имеющая не более одной свободной переменной и определённая по индукции:

  1. атом р  Р переводится в р*(х), где р* – символ унарного отношения;

  2. 1* = 1; 0* = 0;

  3. (А)* = (А*);

  4. (А & В)* = А* & В*; (А  В)* = А*  В*;

  5. (А)*(х) = (y(xRy  A*(y)));

  6. (А)*(х) = (y(xRy & A*(y))).

Здесь R – отношение доступности. Например:

(р  р)*(х) = (р & р)*(х) = (р*(х) & р*(х)) = (y(xRy  p*(y)) & р*(х));

( (p  q))*(x) = y(xRy  (p q)*(y)) = y(xRy  (p*(y)  z(yRz & q*(z)))).

Теорема (о соответствии Салквиста). Каждой формуле Салквиста А соответствует некоторое свойство первого порядка шкал Крипке. Шкала Крипке будет обладать этим свойством тогда и только тогда , когда А будет тавтологией относительно этой шкалы. Существует алгоритм получения этого свойства из формулы А.

Замечание. Салквист установил, что после добавления формулы Салквиста к системе K в качестве аксиомы получается корректная и полная формальная теория.

Доказательство теоремы. Пусть А – несвязная формула. Например:

А = (q & ([c] & [p])) & [p],

где c – позитивная формула. Здесь А построена из строго позитивных p, p, q и негативной c формул с помощью & и . Предположим, что А не является тавтологией относительно шкалы F = (W, R). Тогда существует модель (W, R, h) и мир tW такие, что M, t |= A. Для нашего примера:

M, t |= (q & (c & [p])) & [p].

Это означает, что существует схема из шести миров, соответствующих ромбикам, связанных с помощью путей в графе R с миром t. Для этих миров ti справедливы утверждения: M, ti |= Bi, где Bi – либо строго позитивные, как р, либо негативные, как с.

Далее будем использовать префиксную форму записи R(x, y) для xRy. Таким образом, R(x, y) = 1, если и только если (x, y)  R.

Чтобы получить имена миров, будем использовать стандартный перевод А*(t). В нашем примере А*(t) будет утверждением о существовании миров t1, …, t6, удовлетворяющих следующим условиям:

R(t, t1), R(t1, t2), R(t1, t3), R(t3, t4), R(t, t5), R(t5, t6); M, t2 |= q; M, t3 |= с; M, t4| = p; M, t6 |= p.

По лемме, если мы ‘сузим’ h, сделав атомы истинными в меньшем подмножестве миров, то негативные формулы, например с, все останутся верными в их собственных мирах в схеме (в нашем примере в t3). Существует наименьшая оценка h, которая сохраняет все полученные формулы истинными в их мирах. Можно доказать, что наименьшая оценка, делающая истинной А в мире t будет из тех, которые делают истинными все строго позитивные формулы р в их мирах.

В нашем случае истинность р в мире t4 означает, что в каждом мире, доступном за 2 шага из t4, истинна формула р. Значит, р будет истинной для всех х, удовлетворяющих формуле:

y(R(t4, y) & R(y, x)).

Аналогично р будет означать истинность р для таких х, что R(t6, x). Формула q верна для всех таких х, что х = t2. Таким образом, если мы сделаем p и q верными только в тех мирах, которые строятся по строго позитивным формулам, то А будет верным в мире t.

Эта интерпретация h называется ленивой. Она определяется с помощью формул языка первого порядка:

Мы делаем р истинным в мирах х тогда и только тогда, когда формула:

p*(x) = y(R(t4, y) & R(y, x)) R(t6, x)

истинна в шкале. А q истинна в x, если и только если x = t2. Значит, q*(x) = (x = t2).

Преобразуем далее формулу A*(t):

  1. перемещаем кванторы ti в начало формулы;

  2. заменяем р*(х) нашим ленивым выражением y(R(t4, y) & R(y, x))  R(t6, x);

  3. заменяем р*(y) на формулу z(R(t4, z) & R(z, y))  R(t6, y);

  4. аналогично для подформул р*(z), р*(t), р*(t4) и т.д.;

  5. заменяем все q*(х) на x = t2, q*(y) на y = t2 и т.д.;

  6. вместо (р)* подставляем 1.

Полученную в результате формулу обозначим: (t). Эквивалентны следующие свойства:

  1. (W, R, h), t |= A для некоторых t  W и h;

  2. (W, R, h), t |= A для некоторых t  W и t1, …, t6;

  3. (W, R) |= (t) для некоторого t  W (в смысле классической логики).

В этом случае формула А будет тавтологией относительно шкалы (W, R) тогда и только тогда, когда (W, R) |= t(t). Мы построили алгоритм, который каждой формуле А сопоставляет формулу (t), которой должна удовлетворять шкала (W, R).

Опишем шаги алгоритма Салквиста, сопоставляющего формуле А формулу t(t) для шкалы (W, R), относительно которой формула А будет тавтологией.

Будем предполагать, что А – формула Салквиста. Например, в случае

А = (р  р) = ([р] & [р])

на входе будет формула ([р] & [р]), а на выходе – формула x R(x, x).

Алгоритм Салквиста

Вход: Формула А, где А – несвязная.

Выход: Свойство шкал, соответствующее А.

Действия:

  1. Выделить негативные и строго позитивные части формулы А.

  2. Нарисовать схему, показывающую, что означает выполнение А в мире t; включить имена миров (например, t1, t2, …), провести между ними рёбра отношения R и отметить миры, на которых верны строго позитивные формулы р.

  3. Определить ленивую оценку, делающую строго позитивные оценки истинными в их мирах.

  4. Для перевода А в А*(t) сделать следующее:

  • поставить впереди формулы А*(t) кванторы s, где s пробегает имена миров, соответствующих ромбикам ;

  • найти строго позитивные подформулы и заменить их на 1;

  • заменить все оставшиеся предикаты р*(х), q*(y), …, соответствующие атомам;

  • произвести упрощения, если можно.

В результате работы алгоритма Салквиста получаем некоторую формулу (t), истинность которой означает, что формула А верна в шкале (W, R) в некотором мире t относительно некоторой оценки.

Значит, формула А будет тавтологией тогда и только тогда, когда (W, R) удовлетворяет формуле t(t) (как модель языка первого порядка, состоящего из единственного бинарного предикатного символа R).

Тем самым, теорема доказана.

Замечание. Ленивая оценка определяет формулы р*(х) следующим образом: Рассматриваем подформулы р, р, р, …, для которых существуют миры среди
t, t1, t2, … . Пути к соответствующим мирам будут давать формулы:

р*(х) = (x = t)  R(t, x)  x1(R(t, x1) & R(x1, x))  …

 x1x2xm(R(t, x1) & R(x1, x2) & … & R(xm, x)).

Пример 2

Найдём формулу (t) для формулы А = (р  р). С этой целью представим А как р & р. Делаем 1 шаг перевода А*(t) = р*(t) & р*(t). Заменяем строго позитивную формулу р*(t) на 1, ибо ленивая оценка делает её истинной. Поскольку р*(t) даёт ленивое определение р*(х) = R(t, x), то А*(t)=1 & р*(t)=R(t, t). Получаем: (t) =
= R(t, t). Если А – тавтология, то (W, R) |= t(t). Следовательно, (W,R) |= tR(t, t).

Пример 3

Пусть А = (р  р). Легко видеть, что А = р & р. Отсюда А*(t) = р*(t) & р*(t). Оценка р*(t) = 1 даёт ленивое определение р*(х) = R(t, x). Ленивая оценка превращает формулу р*(t) в истинную:

x(R(t, x) р*(x)) = xy(R(t, x) (R(x, y) р*(y))).

Следовательно, (t) = xy(R(t, x) & R(x, y)  R(t, y)). Утверждение (W, R) |= t(t) превращается в

(W, R) |= txy(R(t, x) & R(x, y) R(t, y)).

Пример 4

Рассмотрим формулу р  р. Она эквивалентна формуле (р & р). Получаем формулу Салквиста ([р] & [p]). Положим А = [р] & [p]. Стандартный перевод равен:

А*(t) = p*(t) & t1(R(t, t1) & p*(t1)).

Переводим t1 в начало формулы:

А*(t) = t1(p*(t) & R(t, t1) & p*(t1)).

Из условия истинности p*(t1) получаем ленивое определение: р*(х) =R(t1, x). Следовательно, А*(t) = t1(R(t1, t) & R(t, t1)). Формула А будет тавтологией относительно (W, R) тогда и только тогда, когда

(W, R) |= tt1(R(t1, t) & R(t, t1)).

Получаем, что отношение R симметрично:

tt1(R(t, t1) R(t1, t)).

Пример 5

Пусть А – формула, рассмотренная при доказательстве теоремы Салквиста. Найдём А*(t) в случае, когда с = p  q:

A = (q & ([(p q)] & [p])) & [p].

Мы получили формулу:

А*(t) = R(t, t1) & R(t1, t2) & R(t1, t3) & R(t3, t4) & R(t, t5) & R(t5, t6) & q*(t2) & c*(t3) & p*(t4) & p*(t6).

Ленивое определение получаем из условия: p*(t4) & p*(t6) = 1. Мы установили, что

р*(х) = y(R(t4, y) & R(y, x))  R(t6, x);

q*(x) = (x = t2).

Поставив с*(t3) = p*(t3)  q*(t3) в формулу для А*(t), получим:

А*(t) = R(t, t1) & R(t1, t2) & R(t1, t3) & R(t3, t4) & R(t, t5) & R(t5, t6) & (p*(t3)  q*(t3));

(t) = t1t2t3t4t5t6(R(t, t1) & R(t1, t2) & R(t1, t3) & R(t3, t4) & R(t, t5) & R(t5, t6) & (x(R(t3, x)  p*(x))  (t3 = t2)) = t1t2t3t4t5t6(R(t, t1) & R(t1, t2) & R(t1, t3) & R(t3, t4) & R(t, t5) & R(t5, t6) & (x(R(t3, x)  y(R(t4, y) & R(y, x))  R(t6, x))  (t3 = t2))

Пример 6

По заданной формуле ([p] & [q] & [(p  q)] найдём свойство шкал (W, R), относительно которых эта формула является тавтологией. Положим:

А = [p] & [q] & [(p  q)];

(t) = t1t2t3R(t, t1) & R(t1, t2) & p*(t2) & R(t, t3) & q*(t3) & ((p*(t)  q*(t))).

Из условий истинности:

p*(t2) = x(R(t2, x) p*(x)),

q*(t3) = x(R(t3, x) q*(x)),

найдём ленивые определения:

p*(x) = R(t2, x); q*(x) = R(t3, x).

Подставляя их в (t) и учитывая, что p*(t2) = 1 и q*(t3) = 1, получим:

(t) = t1t2t3R(t, t1) & R(t1, t2) & R(t, t3) & (x(R(t, x)  R(t2, x))  R(t3, t)).

Утверждение (W, R) |= t(t) приводит к формуле 1-го порядка:

tt1t2t3(R(t, t1)  R(t1, t2)  R(t, t3)  x(R(t, x)  R(t2, x))  R(t3, t)).

Упражнения

Найти свойства шкал Крипке, соответствующих формулам:

  1. А  А (Ответ: u(wRu));

  2. А  А (Ответ: wRu & wRu  vRu);

  3. А  А (Ответ: wRv & wRu  v = u);

  4. А  А (Ответ: wRv  u(wRu & uRv));

  5. А  А (Ответ: wRv & wRx  u(vRu & xRu)).

6.5. Темпоральная логика

Для темпоральной логики вместо символа используются символы [F] – «будет» и [P] – «было». Аналогично символу  определяются символы <F> = [F] и
<Р> = [Р]. Модель Крипке M = (W, R, h) была определена как граф вместе с оценкой h : P  P(W). Напомним, что истинность формул [F]A и [P]A устанавливается с помощью выражений:

M, t |= [F]A, если и только если M, u |= A для всех u  W, таких, что R(t, u);

M, t |= [P]A, если и только если M, u |= A для всех u  W, таких, что R(u, t).

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

Формальная теория 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 A ,означает, что А – теорема в формальной теории 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 верно, если и только если А – тавтология относительно всех потоков времени.

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

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

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

tu (t < u v(t < v <u)).

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

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

tu (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).

Стандартный перевод

С целью обобщения теоремы Салквиста на темпоральную логику применяются преобразования:


Рассмотрим темпоральные операции, применяемые при описании программ и в параллельном программировании.

Завтра и вчера

Добавляются одноместные операции T(завтра) и Y(вчера), и новое правило для построения формул:

Если А – формула, то TA и YA – формулы. Семантика в модели M = (Z, <, h):

M, t |= TA, если и только если M, t+1 |= A;

M, t |= YA, если и только если M, t-1 |= A.

Вместо TA применяются также записи Next A, 0A, XA.

Since, Until

Для любых формул А и В добавляются формулы ASB и AUB. Семантика в модели M = (W, <, h):

M, t |= AUB, если и только если для некоторого u > t верно M, u |= B и при всех v, удовлетворяющих соотношениям t < v < u, верно M, v |= A (иными словами, А верно до тех пор, пока не В);

M, t |= ASB, если и только если для некоторого u < t верно M, u |= B, а для всех v, удовлетворяющих соотношениям u < v < t, верно M, v |= A (с тех пор, как случилось В, верно А).

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

Можно сформулировать темпоральную логику для применений одного типа, выбирая отдельные логические связки и темпоральные операторы. Булевы связки &,  и символ 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) называется экспрессивно полной относительно С, если для любой формулы первого порядка (х, Р1, …, Рn) существует формула А(p1, …, pn) темпоральной логики, для которой А*(х, p1*, …, pn*) эквивалентна (х, p1*, …, pn*) над С. То есть, для любой модели М с потоком времени из С верно:

M |= x (A*(x) (x)).

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

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

  1. X Y = T;

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

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

 Вверх...
Заметки:
» Тепловое оборудование, выбор и расчёт мощности
» Электропривод с двигателем постоянного тока приводит в движение лебедку
» Электротехника, решение задач это просто

Обучение за рубежём:
» Учеба в Великобритании
» Образование в Германии
» Образование в США
» Обучение во Франции

На этом сайте размещены ссылки на найденные в интернете книги, учебную литературу, интересный софт. Мы никак не связаны с сайтами, которые хранят научные труды на своих серверах. Все права принадлежат их авторам. Если у Вас есть авторские права на файлы и Вы не желаете чтобы они были доступны для поиска у нас, напишите нам.

Hosted by uCoz