В логике , общие кадры (или просто кадры ) являются Крипка кадров с дополнительной структурой, которые используются для моделирования модальных и промежуточных логиков. Общая семантика фреймов сочетает в себе основные достоинства семантики Крипке и алгебраической семантики : она разделяет прозрачную геометрическую проницательность первой и надежную полноту второй.
Определение
Модальная общая рама является тройной, где является фреймом Крипке (т. е. R - бинарным отношением на множестве F ), а V - множеством подмножеств F , которое замкнуто при следующих условиях:
- булевы операции (бинарного) пересечения , объединения и дополнения ,
- операция , определяется .
Таким образом, они являются частным случаем полей множеств с дополнительной структурой . Цель V - ограничить допустимые оценки во фрейме: модель на основе рамы Крипке является допустимым в целом кадра F , если
- для каждой пропозициональной переменной p .
Условия замыкания на V тогда гарантируют, чтопринадлежит V для каждой формулы A (не только переменной).
Формула является действительным в F , если для всех допустимых оценок , и все точки . Нормальный модальная логика L является действительным в кадре F , если все аксиомы (или , что эквивалентно, все теоремы ) из L справедливы в F . В этом случае мы называем F L - рамка .
Рамка Крипке можно отождествить с общей системой отсчета, в которой допустимы все оценки: т. е. , где обозначает мощность набор из F .
Типы оправ
В общем, обычные рамы - это не более чем причудливое название для моделей Крипке ; в частности, теряется соответствие модальных аксиом свойствам отношения доступности. Это можно исправить, наложив дополнительные условия на множество допустимых оценок.
Рамка называется
- дифференцированный , если подразумевает ,
- туго , если подразумевает ,
- компактный , если каждое подмножество V со свойством конечного пересечения имеет непустое пересечение,
- атомарный , если V содержит все синглтоны,
- утонченный , если дифференцированный и плотный,
- описательный , если он изысканный и компактный.
Рамы Крипке изящны и атомарны. Однако бесконечные рамки Крипке никогда не бывают компактными. Каждая конечная дифференцированная или атомарная система отсчета является шкалой Крипке.
Описательные фреймы являются наиболее важным классом фреймов из-за теории двойственности (см. Ниже). Уточненные фреймы полезны как общее обобщение описательных фреймов и фреймов Крипке.
Операции и морфизмы на фреймах
Каждая модель Крипке индуцирует общий каркас, где V определяется как
Фундаментальные операции сохранения истинности порожденных подкадров, p-морфических образов и непересекающихся объединений фреймов Крипке имеют аналоги на общих фреймах. Рамкаэто сгенерированный подкадр кадра, если рамка Крипке является сгенерированным подкадром кадра Крипке (т.е. это подмножество закрыто вверх под , а также ), а также
Р-морфизм (или ограниченный морфизм )- функция из F в G , являющаяся p-морфизмом шкал Крипке а также , и удовлетворяет дополнительному ограничению
- для каждого .
Несвязная индексированного множества кадров, , это рамка , где F - несвязное объединение, R - объединение, а также
Уточнение кадра это изысканная рама определяется следующим образом. Рассмотрим отношение эквивалентности
и разреши - множество классов эквивалентности . Затем мы положили
Полнота
В отличие от фреймов Крипке, любая нормальная модальная логика L завершена по отношению к классу общих фреймов. Это следствие полноты L относительно класса моделей Крипке: поскольку L замкнута относительно подстановки, общий репер, индуцированныйявляется L- образной рамой. Более того, каждая логика L полна по отношению к одному описательному фрейму. В самом деле, L полно относительно своей канонической модели, а общая рама , индуцированное канонической модели ( так называемый канонический кадр из L ) является описательным.
Двойственность Йонссона-Тарского
Общие шкалы тесно связаны с модальными алгебрами . Позволятьбыть общим фреймом. Множество V замкнуто относительно булевых операций, поэтому оно является подалгеброй булевой алгебры множеств степеней . Он также выполняет дополнительную унарную операцию,. Комбинированная структураявляется модальной алгеброй, которая называется двойственной алгеброй к F и обозначается.
В обратном направлении можно построить сдвоенный каркас. к любой модальной алгебре . Булева алгебраимеет пространство для камней , чье основное множество Р есть множество всех ультрафильтров из A . Множество V допустимых оценок всостоит из открыто-замкнутых подмножеств F , а отношение доступности R определяется формулой
для всех ультрафильтров x и y .
Фрейм и его двойник проверяют одни и те же формулы, поэтому общая семантика фрейма и алгебраическая семантика в некотором смысле эквивалентны. Двойной дуал любой модальной алгебры изоморфна сам. В общем случае это неверно для двойных двойников фреймов, поскольку двойственные к каждой алгебре описательны. Фактически рама описательна тогда и только тогда, когда она изоморфна своему двойному двойственному .
Также возможно определить двойники p-морфизмов, с одной стороны, и гомоморфизмы модальной алгебры, с другой стороны. Таким образом, операторы а также становятся парой контравариантных функторов между категорией общих шкал и категорией модальных алгебр. Эти функторы обеспечивают двойственность (названную двойственностью Йонссона – Тарского в честь Бьярни Йонссона и Альфреда Тарски ) между категориями описательных фреймов и модальными алгебрами. Это частный случай более общей двойственности между комплексными алгебрами и полями множеств на реляционных структурах .
Интуиционистские рамки
Семантика фрейма для интуиционистской и промежуточной логик может развиваться параллельно с семантикой для модальных логик. Интуиционистская общая рама является тройной, где является частичным порядком на F , а V - это множество верхних подмножеств ( конусов ) в F , содержащее пустое множество и замкнутое относительно
- пересечение и союз,
- операция .
Затем вводятся валидность и другие концепции аналогично модальным фреймам с небольшими изменениями, необходимыми для учета более слабых закрывающих свойств множества допустимых оценок. В частности, интуиционистский фрейм называется
- туго , если подразумевает ,
- компактный , если каждое подмножество со свойством конечного пересечения имеет непустое пересечение.
Тесные интуиционистские рамки автоматически различаются и, следовательно, уточняются.
Двойник интуиционистского фрейма является алгебра гейтингова . Двойственная алгебра Гейтинга интуиционистский фрейм , Где F является множество всех простых фильтров из А , упорядочиваниеявляется включением , а V состоит из всех подмножеств F вида
где . Как и в модальном случае, а также являются парой контравариантных функторов, которые делают категорию алгебр Гейтинга двойственно эквивалентной категории описательных интуиционистских фреймов.
Можно построить интуиционистские общие фреймы из транзитивных рефлексивных модальных фреймов и наоборот, см. Модальный компаньон .
Рекомендации
- Александр Чагров и Михаил Захарящев, Модальная логика , т. 35 из Oxford Logic Guides, Oxford University Press, 1997.
- Патрик Блэкберн, Маартен де Рийке и Иде Венема, Модальная логика , т. 53 Кембриджских трактатов по теоретической информатике, Cambridge University Press, 2001.