Модальная логика, использующая модальные понятия необходимости и возможности

Часто высказывание указывает на отношение субъекта высказывания, т.е. того, кто говорит, к истинности или ложности факта, выраженного в высказывании: что «должно быть» и что «может быть». Для этого вводят дополнительные операторы: ð - необходимо (º обязательно) и à - возможно (º допустимо)[7]. Тогда запись ðА читается как «необходимо А», àА читается как «возможно А». Следует отметить, что оператор ð «похож» на квантор всеобщности, а à - на квантор существования.

Например, в классической логике высказывание А:=«Существуют внеземные цивилизации» можно оценить как ложное или истинное. Однако модальная логика требует интерпретировать это высказывание многозначно: как высказывание «Необходимо существуют внеземные цивилизации», если речь идет об утверждении этого факта как доказанной закономерности, или «Необходимо не существуют внеземные цивилизации», если речь идет об отрицании; однако поскольку данный факт пока не доказан, можно сказать уклончиво: «Возможно, существуют внеземные цивилизации».

Понятно, что в основе модальных высказываний лежат обычные высказывания, которые в логике высказываний мы называли пропозициональными переменными (атомами). Определим синтаксис модальной логики:

1) каждый атом является формулой,

2) символ «истина» (и) является формулой,

3) если А и В – формулы, то ØА, А&В, ðА, àА – формулы,

4) других формул нет.

Возможны дополнительные логические связки и символы для сокращения записи формул: «ложь» (л)=Øи; АÚВ=Ø(ØА&ØВ); А®В=Ø(А&ØВ); А«В=(А®В)&(В®А). Кроме того, следует иметь в виду, что àА=ØðØА, т.е. оператор à является производным в модальной логике. Приоритеты связок (упорядочены по убыванию): Ø, ð, à, &, Ú, ®, «.

Можно по-разному интерпретировать слова из высказываний (это свойство естественного языка определяет его неоднозначность), т.е. каждая формула может быть истинной или ложной в зависимости от такой интерпретации. Поэтому выделяют группы правил интерпретации формул в зависимости от дополнительных условий. Одним из таких условий является выполнение формулы: ð(p®q)®(ðp®ðq). Правила интерпретации (семантики), удовлетворяющие этому условию, называют нормальными. Одной из таких семантик является семантика, предложенная Сеулом Крипке (семантика Крипке).

В семантике Крипке вводятся понятия: Мир – w как набор некоторых данных и условий (т.е. фактов) и множество Миров - W ={w} - для множества фактов. Модальное высказывание àА считается истинным, если А истинно в некоторых из возможных миров. Заметим, что истинность обычных формул измеряется по отношению к текущему миру.

На множестве миров W введем произвольное бинарное отношение R. Если предикат R(w₁,w)=и, где w₁,wÎW, то мир w называется возможным (доступным) миром для w₁. Пара множеств (W, R), где W – непустое множество, а RÍW´W – бинарное отношение на W, называется шкалой Крипке, а отношение R - отношением доступности (достижимости).

Например, пусть 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.

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

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

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

1) если А – атом, то (M, w|-А) тогда и только тогда, когда wÎh(А);

2) (M, w|-и) (всегда);

3) (M, w|- ØА) тогда и только тогда, когда утверждение (M, w|- А) ложно;

4) (M, w|- А&В) тогда и только тогда, когда (M, w|- А) и (M, w|- В);

5) (M, w|- ðА) тогда и только тогда, когда (М, w₁|- А) для всех таких w₁ÎW, что wRw₁.

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

6) (M, w|- АÚВ), если и только если (M, w|- А) или (M, w|- В);

7) (M, w|- (А®В)), если и только если из (M, w|- А) следует, что (M, w|- В);

8) (M, w|- àА), если и только если (M, w₁|= А) для некоторого w₁ÎW такого, что wRw₁;

9) (M, w|- Ø(АÚВ), если и только если (M, w|- ØА&ØВ);

10) (M, w|- ØðА), если и только если (M, w|- àØА);

11) (M, w|- ØàА), если и только если (M, w|- ðØА).

7. Темпоральная (или временнáя) логика

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

Тогда оператор необходимости можно интерпретировать как: «в следующий момент будет…», а оператор возможности как: «когда-то будет…».

Темпоральные формулы используют символы [F] – для обозначения будущего (future) и [Р] – для обозначения прошлого (past).

Вместо ðА применяется запись: [F]A или [P]A. Для образования темпоральных формул применяются правила:

1) каждый атом является формулой,

2) символ «истина» (и) является формулой,

3) если А и В – формулы, то ØA, A & B, [F]A и [P]A – формулы,

4) других формул нет.

Для построения сложных формул используют такие же логические связки, как и в модальной логике.

Введём сокращения: <F>A = Ø[F]ØА и <P>A = Ø[P]ØА. В некоторых случаях сокращения «л», Ú и à будут использоваться как самостоятельные символы.

Объединяя все введенные логические связки, определим их приоритеты (располагаются в порядке убывания): Ø, ð, à, [F], [P], <F>, <P>, &, Ú, ®, «.

Темпоральные связки в зависимости от области применения могут принимать значения:

[F]А = «А будет всегда верно»,

<F>А = «А будет верно в некоторый момент»,

[F]А = «А будет верно всегда, начиная с этого момента времени»,

<F>А = «А верно сейчас или будет верно потом».

Значения [P]А и <P>А определяются симметрично к [F]А и <F>А и относятся к прошедшему времени. Связки «завтра» и «вчера», «до тех пор, пока не» и «с тех пор, как» будут определены позже.

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

В модальной логике можно построить, например, следующие сложные формулы:

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

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

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

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

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

Если wRw₁, то говорят, что w – прошлое для w₁, а w₁ – будущее для w.

Обычно отношение R предполагается транзитивным в том смысле, что из wRw₁ и w₁Rw₂ следует: wRw₂. Утверждения для интерпретации ðА заменяются на следующие:

1) (M, w|- [F]А), если и только если (M, w₁|- А) для всех w₁ÎW таких, что wRw₁,

2) (M, w|- [P]А), если и только если (M, w₁|- А) для всех w₁ÎW таких, что w₁Rw,

3) (M, w|- <F>А), если и только если существует w₁ÎW такой, что wRw₁ и (M, w₁|- А),

4) (M, w|- <P>А), если и только если существует такой w₁ÎW, что w₁Rw и (M, w₁|- А).

В темпоральной логике используются нерефлексивные транзитивные шкалы Крипке. Шкала Крипке (W, <) называется потоком времени, если:

1) "_xÎW (Ø(x<x)),

2) "_{x, y, z}ÎW (x<y&y<z ® x<z).

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

Для того чтобы потоки времени были линейно упорядочены, т.е. удовлетворяли условию "_w"_w1 (w<w₁Úw=w₁Úw₁<w), добавляется аксиома:

<F>A&<F>B ® <F>(A&B)Ú<F>(A&<F>B)Ú(B&<F>A)

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

Для этого добавляются одноместные операции T(завтра) и Y(вчера), и новое правило для построения формул: если А – формула, то TA и YA – формулы. Семантика в модели M=(Z, <, h):

· (M, w|-TA), если и только если (M, w+1|-A);

· M, w |= YA, если и только если (M, w-1|-A).

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

Дата добавления: 2014-01-04