AA3-4(Posets) (1127142), страница 4
Текст из файла (страница 4)
Часть IV: Частично упорядоченные множестваМодели КрипкеШкалы Крипке: интерпретация порядка и формальноеопределениеНеформально порядок u 6 v между мирами интерпретируетсякак то, что мир v есть состояние мира u в следующий моментвремени, понимая время не в физическом, а в логическомсмысле: каждый мир описывается состоянием знаний в данныймомент и однажды установленная истинность или доказанныйфакт остаётся таковым и впоследствии.Логическое время не обязательно обладает линейнымпорядком.ОпределениеШкала Крипке есть тройка h W, 6, i, где редукт h W, 6 i —ч.у. множество, а ⊆ W ×V ar — соответствие «один комногим», ставящее каждому миру совокупность истинных внём логических переменных и удовлетворяющее условиюнаследования истинности.61 / 76ПРИКЛАДНАЯ АЛГЕБРА.
Часть IV: Частично упорядоченные множестваМодели КрипкеШкалы Крипке: истинность формулы в мирахДля построенной шкалы Крипке определим истинность даннойформулы A в любом мире w:w AN B ⇔ w A и w B;w A ∨ B ⇔ w A или w B;w A B ⇔ ∀(u > w) u B или u 6 A;w ¬A ⇔ ∀(u > w) u 6 A.Данные правила обеспечивают условие наследованияистинности.Введённые шкалы Крипке задают семантику ИИВ, придаваясмысл формулам — разделяя их на истинные и ложные вданном мире.62 / 76ПРИКЛАДНАЯ АЛГЕБРА. Часть IV: Частично упорядоченные множестваМодели КрипкеШкалы Крипке: теорема корректностиТеорема (корректности ИИВ относительно шкал Крипке)Формула, выводимая в ИИВ, истина во всех мирах всех шкалКрипке.ДоказательствоПокажем, что все аксиомы истины во всех мирах, а правилоMP сохраняет истинность.Второе очевидно: если и A, и A B истины во всех мирах, тоB будет также истина во всех мирах.Чтобы в мире w проверитьистинность импликации A B надо удостовериться, чтоw A ⇒ w B ( w 6 A эта импликация подавно истина);ложность импликации A B надо удостовериться, чтоw A ⇒ w 6 B.63 / 76ПРИКЛАДНАЯ АЛГЕБРА.
Часть IV: Частично упорядоченные множестваМодели КрипкеШкалы Крипке: теорема корректности...Доказательство (продолжение)Проверим 1-ю аксиому A (B A).Если в некотором мире u имеет место u A, то во всех мирахv > u (в том числе и в u) справедливо v B A.Проверим 2-ю аксиому (A (B C)) ((A B) (A C)).Пусть существует мир u, где она ложна и тогда в нём должныбыть истины формулы A (B C), A B и A, а C — ложна.Но из u A и u A B следует v B во всех мирах v > u.При u A (B C) это означает справедливость w C вовсех мирах w > v.Отсюда следует справедливость u C — противоречие.Остальные аксиомы проверяются аналогично и ещё проще.64 / 76ПРИКЛАДНАЯ АЛГЕБРА.
Часть IV: Частично упорядоченные множестваМодели КрипкеШкалы Крипке: теорема корректности — важное ...СледствиеДля доказательства невыводимости формулы в ИИВдостаточно указать шкалу Крипке, в одном из миров которойона ложна.Такая шкала называется контрмоделью для данной формулы.Существует контрмодель, являющаяся корневым деревом, вкоторой мир с ложной формулой — его корнем.ПримерПостоим шкалу Крипке, содержащую мир, в котором формулаx ∨ ¬x ложна.Возьмём два мира u и v такие, что u 6 v, u 6 x и v x.Тогда v 6 ¬x, откуда u 6 ¬x, что, в свою очередь даётu 6 x ∨ ¬x (но v x ∨ ¬x).65 / 76ПРИКЛАДНАЯ АЛГЕБРА. Часть IV: Частично упорядоченные множестваМодели КрипкеКонтрмодель для x ∨ ¬x (1)66 / 76ПРИКЛАДНАЯ АЛГЕБРА.
Часть IV: Частично упорядоченные множестваМодели КрипкеКонтрмодель для x ∨ ¬x (2)67 / 76ПРИКЛАДНАЯ АЛГЕБРА. Часть IV: Частично упорядоченные множестваМодели КрипкеВизуализация контрмодели для x ∨ ¬x (3)68 / 76ПРИКЛАДНАЯ АЛГЕБРА. Часть IV: Частично упорядоченные множестваМодели КрипкеКонтрмодель для x ∨ ¬x (4)69 / 76ПРИКЛАДНАЯ АЛГЕБРА. Часть IV: Частично упорядоченные множестваМодели КрипкеКонтрмодель для x ∨ ¬x (5)70 / 76ПРИКЛАДНАЯ АЛГЕБРА. Часть IV: Частично упорядоченные множестваМодели КрипкеКонтрмодель для ¬ x ∨ ¬¬ xПусть в некотором мире u данная формула ложна, т.е.u 6 ¬ x ∨ ¬¬ x.Тогда u 6 ¬ x и u 6 ¬¬ x.Построим два несравнимых между собой мира v и w, бо́льшиеu, в которых:v 6 ¬ x и v ¬¬ x ;w 6 ¬¬ x w ¬¬ x.Искомая контрмодель получена:правила истинности и ложности формул в моделисоблюдены;формула x будет истинна только в мире v.71 / 76ПРИКЛАДНАЯ АЛГЕБРА.
Часть IV: Частично упорядоченные множестваМодели КрипкеКонтрмодель для ¬ x ∨ ¬¬ x...72 / 76ПРИКЛАДНАЯ АЛГЕБРА. Часть IV: Частично упорядоченные множестваМодели КрипкеШкалы Крипке: применениеМетод автоматической верификации параллельныхвычислительных систем (англ. model checking), позволяетпроверить, удовлетворяет ли заданная модель системыформальным спецификациям. В качестве модели обычноиспользуют шкалы Крипке, а для спецификацииаппаратного и программного обеспечения — темпоральную(временную) логику.Модальные логики формализуют сильные и слабыемодальные выражения вида «необходимо/возможно»,«всегда/иногда», «здесь/где-то» и т.д.
Заменив вопределении шкалы Крипке частичный порядок наотношение толерантности — получим семантику длябрауэровой логики B;аморфное отношение — семантику для логики S5;диагональное — модель для модальной логики M.73 / 76ПРИКЛАДНАЯ АЛГЕБРА. Часть IV: Частично упорядоченные множестваЧто надо знатьРазделы1Основные понятия теории ч.у. множеств2Операции над ч.у. множествами3Линеаризация4Задачи c решениями5Модели Крипке6Что надо знать74 / 76ПРИКЛАДНАЯ АЛГЕБРА.
Часть IV: Частично упорядоченные множестваЧто надо знатьЧастично упорядоченные (ч.у.) множества: определение,примеры, основные понятия. Диаграммы Хассе и особыеэлементы ч.у. множеств.Ранжированные ч.у. множества. Цепное условиеЖордана-Дедекинда. Порядковые гомоморфизмыИдеалы и фильтры ч.у. множеств.
Конусы. Точные грани.Операции над ч.у. множествами.Теорема Шпильрайна. Линейное продолжение ч.у.множества и топологическая сортировка.Линеаризации и вероятностное пространство над ними.XYZ-теорема. Проблема сортировки и «1/3 – 2/3предположение».Спектр и размерность ч.у.
множеств. Свойстваразмерности, d-несводимые множества и проблема Ногина.75 / 76ПРИКЛАДНАЯ АЛГЕБРА. Часть IV: Частично упорядоченные множестваЧто надо знатьМодели Крипке для интуиционистской логикивысказываний.76 / 76.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
