Общая рамка - General frame

В логика, общие рамки (или просто кадры) находятся Крипке кадры с дополнительной структурой, которые используются для моделирования модальный и средний логика. Общая семантика фрейма объединяет основные достоинства Семантика Крипке и алгебраическая семантика: он разделяет прозрачную геометрическую проницательность первого и надежную завершенность второго.

Определение

А модальный общий каркас это тройка ${displaystyle mathbf {F} =langle F,R,Vangle }$, куда ${displaystyle langle F,Rangle }$ является фреймом Крипке (т.е. р это бинарное отношение на съемочной площадке F), и V это набор подмножеств F который закрыт при следующих условиях:

• логические операции (двоичные) пересечение, союз, и дополнять,
• операция ${displaystyle Box }$, определяется ${displaystyle Box A={xin F;,forall yin F,(x,R,y o yin A)}}$.

Таким образом, они являются частным случаем поля наборов с дополнительной структурой. Цель V заключается в том, чтобы ограничить допустимые оценки в кадре: модель ${displaystyle langle F,R,Vdash angle }$ на основе рамы Крипке ${displaystyle langle F,Rangle }$ является допустимый в общем кадре F, если

${displaystyle {xin F;,xVdash p}in V}$ для каждого пропозициональная переменная п.

Условия закрытия на V затем убедитесь, что ${displaystyle {xin F;,xVdash A}}$ принадлежит V за каждый формула А (не только переменная).

Формула А является действительный в F, если ${displaystyle xVdash A}$ для всех допустимых оценок ${displaystyle Vdash }$, и все точки ${displaystyle xin F}$. А нормальная модальная логика L действительно в кадре F, если все аксиомы (или, что то же самое, все теоремы) L действительны в F. В этом случае мы называем F ан L-Рамка.

Рамка Крипке ${displaystyle langle F,Rangle }$ можно отождествить с общей системой отсчета, в которой допустимы все оценки: т. е. ${displaystyle langle F,R,{mathcal {P}}(F)angle }$, куда ${displaystyle {mathcal {P}}(F)}$ обозначает набор мощности из F.

Типы оправ

В общем, обычные рамки - не более чем причудливое имя для Крипке. модели; в частности, теряется соответствие модальных аксиом свойствам отношения доступности. Это можно исправить, наложив дополнительные условия на множество допустимых оценок.

Рама ${displaystyle mathbf {F} =langle F,R,Vangle }$ называется

• дифференцированный, если ${displaystyle forall Ain V,(xin ALeftrightarrow yin A)}$ подразумевает ${displaystyle x=y}$,
• в обтяжку, если ${displaystyle forall Ain V,(xin Box ARightarrow yin A)}$ подразумевает ${displaystyle x,R,y}$,
• компактный, если каждое подмножество V с свойство конечного пересечения имеет непустое пересечение,
• атомный, если V содержит все синглтоны,
• изысканный, если дифференцированно и плотно,
• описательный, если он изысканный и компактный.

Оправы Крипке изящны и атомарны. Однако бесконечные рамки Крипке никогда не бывают компактными. Каждая конечная дифференцированная или атомарная система отсчета является шкалой Крипке.

Описательные фреймы являются наиболее важным классом фреймов из-за теории двойственности (см. Ниже). Уточненные фреймы полезны как общее обобщение описательных фреймов и фреймов Крипке.

Операции и морфизмы на фреймах

Каждая модель Крипке ${displaystyle langle F,R,{Vdash }angle }$ побуждает общая рамка ${displaystyle langle F,R,Vangle }$, куда V определяется как

${displaystyle V={ig {}{xin F;,xVdash A};,A{hbox{ is a formula}}{ig }}.}$

Фундаментальные сохраняющие истину операции над порожденными подфреймами, p-морфическими изображениями и непересекающимися объединениями фреймов Крипке имеют аналоги на общих фреймах. Рама ${displaystyle mathbf {G} =langle G,S,Wangle }$ это сгенерированный подкадр кадра ${displaystyle mathbf {F} =langle F,R,Vangle }$, если рамка Крипке ${displaystyle langle G,Sangle }$ является сгенерированным подкадром кадра Крипке ${displaystyle langle F,Rangle }$ (т.е. ${displaystyle G}$ это подмножество ${displaystyle F}$ закрыто вверх под ${displaystyle R}$, и ${displaystyle S=Rcap G imes G}$), и

${displaystyle W={Acap G;,Ain V}.}$

А р-морфизм (или же ограниченный морфизм) ${displaystyle fcolon mathbf {F} o mathbf {G} }$ это функция от F к грамм который является p-морфизмом шкал Крипке ${displaystyle langle F,Rangle }$ и ${displaystyle langle G,Sangle }$, и удовлетворяет дополнительному ограничению

${displaystyle f^{-1}[A]in V}$ для каждого ${displaystyle Ain W}$.

В несвязный союз индексированного набора кадров ${displaystyle mathbf {F} _{i}=langle F_{i},R_{i},V_{i}angle }$, ${displaystyle iin I}$, это рамка ${displaystyle mathbf {F} =langle F,R,Vangle }$, куда F дизъюнктное объединение ${displaystyle {F_{i};,iin I}}$, р это союз ${displaystyle {R_{i};,iin I}}$, и

${displaystyle V={Asubseteq F;,forall iin I,(Acap F_{i}in V_{i})}.}$

В уточнение кадра ${displaystyle mathbf {F} =langle F,R,Vangle }$ это изысканная рама ${displaystyle mathbf {G} =langle G,S,Wangle }$ определяется следующим образом. Мы считаем отношение эквивалентности

${displaystyle xsim yiff forall Ain V,(xin ALeftrightarrow yin A),}$

и разреши ${displaystyle G=F/{sim }}$ - множество классов эквивалентности ${displaystyle sim }$. Затем мы положили

${displaystyle langle x/{sim },y/{sim }angle in Siff forall Ain V,(xin Box ARightarrow yin A),}$

${displaystyle A/{sim }in Wiff Ain V.}$

Полнота

В отличие от фреймов Крипке, каждая нормальная модальная логика L полна относительно класса общих шкал. Это следствие того, что L полна относительно класса моделей Крипке ${displaystyle langle F,R,{Vdash }angle }$: в качестве L замкнут относительно подстановки, общий репер, индуцированный ${displaystyle langle F,R,{Vdash }angle }$ является L-Рамка. Более того, каждая логика L является полным относительно одного описательный Рамка. В самом деле, L полна по отношению к своей канонической модели, а общий репер, индуцированный канонической моделью (называемый каноническая рамка из L) носит описательный характер.

Двойственность Йонссона-Тарского

Лестница Ригера – Нисимуры: универсальная интуиционистская система координат Крипке.

Его двойственная алгебра Гейтинга - решетка Ригера – Нисимуры. Это бесплатная алгебра Гейтинга над одним генератором.

Общие рамы имеют тесную связь с модальные алгебры. Позволять ${displaystyle mathbf {F} =langle F,R,Vangle }$ быть общим фреймом. Набор V замкнуто относительно булевых операций, поэтому является подалгебра силовой установки Булева алгебра ${displaystyle langle {mathcal {P}}(F),cap ,cup ,-angle }$. Он также выполняет дополнительную унарную операцию, ${displaystyle Box }$. Комбинированная структура ${displaystyle langle V,cap ,cup ,-,Box angle }$ является модальной алгеброй, которая называется двойственная алгебра из F, и обозначается ${displaystyle mathbf {F} ^{+}}$.

В обратном направлении можно построить двойная рама ${displaystyle mathbf {A} _{+}=langle F,R,Vangle }$ к любой модальной алгебре ${displaystyle mathbf {A} =langle A,wedge ,vee ,-,Box angle }$. Булева алгебра ${displaystyle langle A,wedge ,vee ,-angle }$ имеет Каменное пространство, чей базовый набор F это набор всех ультрафильтры из А. Набор V допустимых оценок в ${displaystyle mathbf {A} _{+}}$ состоит из прищемить подмножества F, и отношение доступности р определяется

${displaystyle x,R,yiff forall ain A,(Box ain xRightarrow ain y)}$

для всех ультрафильтров Икс и у.

Фрейм и его двойник проверяют одни и те же формулы, поэтому общая семантика фрейма и алгебраическая семантика в некотором смысле эквивалентны. Двойной дуал ${displaystyle (mathbf {A} _{+})^{+}}$ любой модальной алгебры изоморфна ${displaystyle mathbf {A} }$ сам. В общем случае это неверно для двойных двойников фреймов, поскольку двойственный к каждой алгебре описательный. Фактически рама ${displaystyle mathbf {F} }$ описательна тогда и только тогда, когда она изоморфна своему двойному двойственному ${displaystyle (mathbf {F} ^{+})_{+}}$.

Также возможно определить двойники p-морфизмов, с одной стороны, и гомоморфизмы модальной алгебры, с другой стороны. Таким образом, операторы ${displaystyle (cdot )^{+}}$ и ${displaystyle (cdot )_{+}}$ стать парой контравариантные функторы между категория общих шкал и категории модальных алгебр. Эти функторы обеспечивают двойственность (называется Двойственность Йонссона-Тарского после Бьярни Йонссон и Альфред Тарский ) между категориями описательных фреймов и модальных алгебр. Это частный случай более общей двойственности между комплексные алгебры и поля множеств на реляционных структурах.

Интуиционистские рамки

Семантика фрейма для интуиционистской и промежуточной логик может быть разработана параллельно семантике для модальных логик. An интуиционистский общий фрейм это тройка ${displaystyle langle F,leq ,Vangle }$, куда ${displaystyle leq }$ это частичный заказ на F, и V это набор верхние подмножества (шишки) из F который содержит пустое множество и закрывается при

• пересечение и союз,
• операция ${displaystyle A o B=Box (-Acup B)}$.

Затем вводятся валидность и другие концепции аналогично модальным фреймам с небольшими изменениями, необходимыми для учета более слабых закрывающих свойств множества допустимых оценок. В частности, интуиционистский фрейм ${displaystyle mathbf {F} =langle F,leq ,Vangle }$ называется

• в обтяжку, если ${displaystyle forall Ain V,(xin ALeftrightarrow yin A)}$ подразумевает ${displaystyle xleq y}$,
• компактный, если каждое подмножество ${displaystyle Vcup {F-A;,Ain V}}$ со свойством конечного пересечения имеет непустое пересечение.

Тесные интуиционистские рамки автоматически различаются и, следовательно, уточняются.

Двойник интуиционистского фрейма ${displaystyle mathbf {F} =langle F,leq ,Vangle }$ это Алгебра Гейтинга ${displaystyle mathbf {F} ^{+}=langle V,cap ,cup , o ,emptyset angle }$. Двойственная алгебра Гейтинга ${displaystyle mathbf {A} =langle A,wedge ,vee , o ,0angle }$ интуиционистский фрейм ${displaystyle mathbf {A} _{+}=langle F,leq ,Vangle }$, куда F это набор всех первичные фильтры из А, заказ ${displaystyle leq }$ является включение, и V состоит из всех подмножеств F формы

${displaystyle {xin F;,ain x},}$

куда ${displaystyle ain A}$. Как и в модальном случае, ${displaystyle (cdot )^{+}}$ и ${displaystyle (cdot )_{+}}$ являются парой контравариантных функторов, которые делают категорию алгебр Гейтинга двойственно эквивалентной категории описательных интуиционистских фреймов.

Можно построить интуиционистские общие фреймы из транзитивных рефлексивных модальных фреймов и наоборот, см. модальный компаньон.

Рекомендации

• Александр Чагров и Михаил Захарящев, Модальная логика, т. 35 из Oxford Logic Guides, Oxford University Press, 1997.
• Патрик Блэкберн, Maarten de Rijke, и Иде Венема, Модальная логика, т. 53 Кембриджских трактатов по теоретической информатике, Cambridge University Press, 2001.