Формула Сахлквиста

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

Определение Сахлквиста характеризует разрешимый набор модальных формул с корреспондентами первого порядка. Поскольку по теореме Чагровы неразрешимо, имеет ли произвольная модальная формула корреспондент первого порядка, существуют формулы с фреймовыми условиями первого порядка, которые не являются Сахлквистскими [Чагрова, 1991] (см. Примеры ниже). Следовательно, формулы Сахлквиста определяют только (разрешимое) подмножество модальных формул с корреспондентами первого порядка.

• 1 Определение
• 2 Примеры формул Сахлквиста
• 3 Примеры формул Сахлквиста
• 4 Теорема Крахта
• 5 Ссылки

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

• Атом в прямоугольной рамке - это пропозициональный атом, которому предшествует количество (возможно, 0) прямоугольников, то есть формула вида $◻\; \cdots \; ◻\; p\; \{\backslash \; displaystyle\; \backslash \; Box\; \backslash \; cdots\; \backslash \; Box\; p\}$(часто сокращенно $◻\; ip\; \{\backslash \; displaystyle\; \backslash \; Box\; ^\; \{i\}\; p\}$для ).
• антецедент Сахлквиста - это формула, построенная с использованием ∧, ∨ и $◊\; \{\backslash \; displaystyle\; \backslash \; Diamond\}$из атомов в рамке и отрицательных формул (включая константы ⊥, ⊤).
• Импликация Сахлквиста - это формула A → B, где A является антецедентом Сахлквиста, а B - положительной формулой.
• Формула Сахлквиста строится из значений Сахлквиста с использованием ∧ и $◻\; \{\backslash \; displaystyle\; \backslash \; Box\}$(неограниченно), и использование ∨ в формулах без общих переменных.

$p\; \to \; ◊\; p\; \{\backslash \; displaystyle\; p\; \backslash \; rightarrow\; \backslash \; Diamond\; p\}$

Соответствующая формула первого порядка $\forall \; x\; R\; xx\; \{\backslash \; displaystyle\; \backslash \; forall\; x\; \backslash ;\; Rxx\}$, и он определяет все рефлексивные фреймы

$p\; \to \; ◻\; ◊\; p\; \{\backslash \; displaystyle\; p\; \backslash \; rightar\; row\; \backslash \; Box\; \backslash \; Diamond\; p\}$

Соответствующая формула первого порядка: $\forall \; x\; \forall \; y\; [R\; xy\; \to \; R\; yx]\; \{\backslash \; displaystyle\; \backslash \; forall\; x\; \backslash \; forall\; y\; [Rxy\; \backslash \; rightarrow\; Ryx]\}$, и он определяет все симметричные кадры

$◊\; ◊\; p\; \to \; ◊\; p\; \{\backslash \; displaystyle\; \backslash \; Diamond\; \backslash \; Diamond\; p\; \backslash \; rightarrow\; \backslash \; Diamond\; p\}$или $p\; \to \; ◻\; ◻\; p\; \{\backslash \; displaystyle\; \backslash \; Box\; p\; \backslash \; rightarrow\; \backslash \; Box\; \backslash \; Box\; p\}$

Соответствующая формула первого порядка: $\forall \; x\; \forall \; y\; \forall \; z\; [(R\; xy\; \wedge \; R\; yz)\; \to \; R\; xz]\; \{\backslash \; displaystyle\; \backslash \; forall\; x\; \backslash \; forall\; y\; \backslash \; forall\; z\; [(Rxy\; \backslash \; land\; Ryz)\; \backslash \; rightarrow\; Rxz]\}$, и он определяет все транзитивные фреймы

$◊\; p\; \to \; ◊\; ◊\; п\; \{\backslash \; displaystyle\; \backslash \; Diamond\; p\; \backslash \; rightarrow\; \backslash \; Diamond\; \backslash \; Diamond\; p\}$или $◻\; ◻\; p\; \to \; ◻\; p\; \{\backslash \; displaystyle\; \backslash \; Box\; \backslash \; Box\; p\; \backslash \; rightarrow\; \backslash \; Box\; p\}$

его Соответствующая формула первого порядка: $\forall \; Икс\; \forall \; Y\; [R\; xy\; \to \; \exists \; Z\; (R\; xz\; \wedge \; R\; zy)]\; \{\backslash \; displaystyle\; \backslash \; forall\; x\; \backslash \; forall\; y\; [Rxy\; \backslash \; rightarrow\; \backslash \; exists\; z\; (Rxz\; \backslash \; land\; Rzy)]\; \}$, и он определяет все плотные фреймы

$◻\; p\; \to \; ◊\; p\; \{\backslash \; displaystyle\; \backslash \; Box\; p\; \backslash \; rightarrow\; \backslash \; Diamond\; p\}$

Соответствующая формула первого порядка: $\forall \; x\; \exists \; y\; R\; xy\; \{\backslash \; displaystyle\; \backslash \; forall\; x\; \backslash \; exists\; y\; \backslash ;\; Rxy\}$, и она определяет все неограниченные вправо фреймы (также называется серийным)

$◊\; ◻\; p\; \to \; ◻\; ◊\; p\; \{\backslash \; displaystyle\; \backslash \; Diamond\; \backslash \; Box\; p\; \backslash \; rightarrow\; \backslash \; Box\; \backslash \; Diamond\; p\}$

Соответствующая формула первого порядка $\forall \; x\; \forall \; x\; 1\; \forall \; Z\; 0\; [R\; xx\; 1\; \wedge \; R\; xz\; 0\; \to \; \exists \; z\; 1\; (R\; x\; 1\; z\; 1\; \wedge \; R\; z\; 0\; z\; 1)]\; \{\backslash \; displaystyle\; \backslash \; forall\; x\; \backslash \; forall\; x\_\; \{1\}\; \backslash \; forall\; z\_\; \{0\}\; [Rxx\_\; \{1\}\; \backslash \; land\; Rxz\_\; \{0\}\; \backslash \; rightarrow\; \backslash \; exists\; z\_\; \{1\}\; (Rx\_\; \{1\}\; z\_\; \{1\}\; \backslash \; land\; Rz\_\; \{0\}\; z\_\; \{1\})]\}$, и это Свойство Черча-Россера.

$◻\; ◊\; p\; \to \; ◊\; ◻\; p\; \{\backslash \; displaystyle\; \backslash \; Box\; \backslash \; Diamond\; p\; \backslash \; rightarrow\; \backslash \; Diamond\; \backslash \; Box\; p\}$

Это формула Маккинси ; он не имеет условия фрейма первого порядка.

$◻\; (◻\; p\; \to \; p)\; \to \; ◻\; p\; \{\backslash \; displaystyle\; \backslash \; Box\; (\backslash \; Box\; p\; \backslash \; rightarrow\; p)\; \backslash \; rightarrow\; \backslash \; Box\; p\}$

Аксиома Лёба не Сахлквист; опять же, у него нет условия фрейма первого порядка.

$(◻\; ◊\; p\; \to \; ◊\; ◻\; p)\; \wedge \; (◊\; ◊\; q\; \to \; ◊\; q)\; \{\backslash \; displaystyle\; (\backslash \; Box\; \backslash \; Diamond\; p\; \backslash \; rightarrow\; \backslash \; Diamond\; \backslash \; Box\; p)\; \backslash \; land\; (\backslash \; Diamond\; \backslash \; Diamond\; q\; \backslash \; rightarrow\; \backslash \; Diamond\; q)\}$

Конъюнкция формулы Мак-Кинси и аксиомы (4) имеет фрейм-условие первого порядка (конъюнкция свойства транзитивности со свойством $\forall \; Икс\; [\forall \; Y\; (R\; xy\; \to \; \exists \; Z\; [R\; yz])\; \to \; \exists \; Y\; (R\; xy\; \wedge \; \forall \; Z\; [R\; yz\; \to \; z\; =\; y])]\; \{\backslash \; displaystyle\; \backslash \; forall\; x\; [\backslash \; forall\; y\; (Rxy\; \backslash \; rightarrow\; \backslash \; exists\; z\; [Ryz])\; \backslash \; rightarrow\; \backslash \; exists\; y\; (Rxy\; \backslash \; wedge\; \backslash \; forall\; z\; [Ryz\; \backslash \; rightarrow\; z\; =\; y])]\}$), но не эквивалентен какой-либо формуле Сахлквиста.

Когда формула Сахлквиста используется в качестве аксиомы в нормальной модальной логике, логика гарантированно полна по отношению к элементарному классу фреймов, определяемых аксиомой. Этот результат исходит из теоремы Сальквиста о полноте [Модальная логика, Блэкберн и др., Теорема 4.42]. Но есть и обратная теорема, а именно теорема, которая утверждает, какие условия первого порядка соответствуют формулам Сахлквиста. Теорема Крахта утверждает, что любая формула Сальквиста локально соответствует формуле Крахта; и наоборот, каждая формула Крахта является локальным корреспондентом первого порядка некоторой формулы Сахлквиста, которая может быть эффективно получена из формулы Крахта [Модальная логика, Блэкберн и др., теорема 3.59].

• L. А. Чагрова, 1991. Неразрешимая проблема теории соответствий. Journal of Symbolic Logic 56: 1261–1272.
• Маркус Крахт, 1993. Как сошлись воедино теории полноты и соответствия. Ин де Рийке, редактор, Diamonds and Defaults, стр. 175–214. Kluwer.
• Хенрик Сальквист, 1975. Соответствие и полнота в семантике первого и второго порядка для модальной логики. В материалах Третьего симпозиума по скандинавской логике. Северная Голландия, Амстердам.