С.И. Гуров, Д.А. Кропотов - Конспект лекций по курсу Прикладная алгебра (1127136), страница 23
Текст из файла (страница 23)
множество ( W, ~), элементы носителя которого называ1от мирами;•для каждого мира указать,какие из логическихпеременных в нём являются истинныминые переменные в этом мире ложны).(осталь5.5.(IIIпоток)265Факт истинности переменной х в миревают символически w 1 ~ х, ложности - ww записыI,Yх.При формировании шкалы Крипке требуется, чтобыи ~vи и 1~ х::::} v1~ х,т. е .
, как говорят, <<область истинности переменной наследуется вверх>> или <<сохраняется в больших мирах>>.Н еформально порядок и ~претируется как то , что мирvvмежду мирами интересть состояние мираив следующий момент времени, понимая время не в физ ическом , а в логическом смысле: каждый мир описывается состоянием знаний в данный момент и однаждыустановленная истинность или доказанный факт оста••ется таковым и впоследствии.Логическое время не обязательно обладает линейным порядком .Опр еделение( W,~, 1~),а 1~ ~Wвящеех5.11 .Шrк;алагде редуктVar( W, ~) -естьч.у.тройкамножество ,-соответствие <<один ко многим>>, ста-каждомулогическихKpunrк;eмирусовокуп ностьпеременныхиистинныхудовлетворяющеев••немусловиюнаследования и стинности .Для построенной шкалы Крипке определим истин-ность данной q)ормулы А в л1обом миреw 1 ~ А & В {::} w 1~ А и w 1~ В;w 1~ Аwwv В {::}w:w 1~ А или w 1~ В;1~ А => В{::} V(и ~w)и 1 ~ В или иI,Y А;1~ 'А {::} V( и ~ w) и I,Y А(т.
е. если 1~ ,А, то не существует большего мира,в котором бы 1~ А).266Глава 5. Ч.у. множестваВ ведённые шкалы Крипке зада}ОТ се.мантиrх;у ИИВ ,придавая смысл фор муламразделяя их на истинные-и ложные в данн о м ми р е .• Истинная в данном мире формула остаётся истинной и в старших (больших) мирах.• Ложная в данном мире формула была ложной иво всех младших (меньших) мирах.•Если формула содержит только связки••&иV,••то ее истинность в данном мире не зависит от ееистинности в др угих ми р ах .•И ст инности импликации и отрицания используютпорядо к на множестве мир ов .• Следствием предыдущего является факт независимости импликации от других связок: в ИИВ , например , фор мулы А => В и -.АVВлогически неэквивале нтны .ААРи с.5.16.ААААШ калы Крипке : варианты истинности формулы в шкале из двух ми ров5.5.
(III поток)Тео ема2675.6 (корректности ИИВ относительно шкалКрипке). Формула, въtводи.ма.я в ИИВ, истина во всех.мирах всех шк;ал Крипк;е .Доказательство. П окажем, что(1)все аксиомы истины во всех мирах и(2) правило МР сохраняет истинность .Второе очевидно: если и А , и А => В истины во всехмир ах, то В будет также истина во всех мирах .Замечание: чтобы в мире•w проверить оценкуистинность импликацииА => Вриться, что w 1~ А =? w 1~ Внадо удостове( w l)fА эта импликация подавно истина);•ложность импликации А => В надо удостовериться, что w 1~ А =? wТео емаl)fВ.о5.7 (корректности ИИВ относительно шкалКрипке). Формула, выводимая в ИИВ, истина во всех.мирах всех шк;ал Крипк;е .Доказательство.
Покажем, что(1)все аксиомы истиныво всех мирах и (2) правило МР сохраняет истинность.Второе очевидно: если и А , и А=> В и стины во всехмирах, то В будет также истина во всех мирах .Замечание: чтобы в мире w проверить оценку•истинность импликацииА => Вриться , что w 1 ~ А =? w 1 ~ Внадо удостове( w l)fА эта импликация подавно истина);•ложность импликации А => В надо удостовериться, чтоw 1~ А =? w l)f В.268Глава 5. Ч.у. множестваПроверим l -Io аксиому А => ( В=> А) .Если в векотором мире и имеет место и 1 ~ А , тово всех мирахvv ):и (в том числе и в и) справедливо1~ В => А.Проверим 2 -ю аксиому(А => (В => С)) => ((А => В) => (А => С)) .Пусть существует мир и , где она ложна::::}в нёмдолжны быть истины формулы А => (В => С) , А => В и-А, а Сложна.Н о из и 1 ~ А и и 1~ А => В следуетмирахv ):ведливостьи. При и1=v 1=В во всехА => (В=> С) это означает спраw 1= С во всех мирах w ): v .
Отсюда следует справедливость и1=С-противоречие.Остальные аксиомы проверяются аналогич но.оСле ствие . Дл.я доrк;азателъства невыводимости формулы в ИИВ достаточно уrк;азатъ шrк;алу Крипrк;е, водном из миров rк;оторой она ложна .Такая шкала называется rк;онтрмоделъю для даннойформулы .
Существует контрмодель , являющаяся корневым деревом, в которой мир с ложной формулой-его корнем .При мер5.6. 1.Постоим шкалу Крипке , содержащуюмир, в котором формула хВ озьмём два мира и иV --,хvложна.такие, что и ~v,иIY: хv 1 ~ х . Тогда v IY: --,х, откуда и IY: --,х, что, в своюочередь даёт и IY: х V --,х (но v 1~ х V --,х) .и5.5.
(III поток)269vvхх-.хuuххvvх-.ххu-.хuхх-.хx v -.xvх-.хxV-.xuх2.Постоим шкалу Крипке , содержащуi{) мир, в котором формулаПустьив1хмиреIY ~х V 11х.V 11 хиТогда иложна .даннаяIY ~хфор мулаи иложна,IY 11х .Построим два несравнимых между собой мираw,большие и , в которых :• vIY1х и vlr-11х;т. е .vиГлава270• w IJL11х и w 1~115. Ч.у.
множествах.Искомая контрмодель получена:•правила истинности и ложности формул в моделисоблюдены;•формула х будет истинна только в мире v.vwххu-.-.х-.хРис.5.17.JV-.х-.-.хКонтрмодель для1хV 11 хШкалы Крипке: применение•Метод автоматической верификации параллельных вычислительных системing),(англ. model check-позволяет про верить, удовлетворяет ли заданная модель системы формальным спецификациям. В качестве модели обычно используют шкалы Крипке, а для спецификации аппаратного ипрограммнога обеспечения - те.мпоралъrну1о (временную) логику.5.5.
(III поток)•Модалъ'Ные271логиrх;иформализуютсилъ'Ныеислабъtе модалъ'Нъtе выражения вида << необходимо/ возможно>> , << всегда/ иногда>>, << здесь/ где-то >> ит. д. Заменив в определении шкалы Крипке частичный порядок наотношение толерантности-получим семантику для брауэравой логики В;аморфное отношениеки-семантику для логиSS;диагональноегики М.-модель для модальной ло.