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

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

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

Определение

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

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

Примеры формул Сальквиста

$p\rightarrow \Diamond p$

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

$p\rightarrow \Box \Diamond p$

Соответствующая ему формула первого порядка: $\forall x\forall y[Rxy\rightarrow Ryx]$, и он определяет все симметричные кадры

$\Diamond \Diamond p\rightarrow \Diamond p$ или $\Box p\rightarrow \Box \Box p$

Соответствующая ему формула первого порядка: $\forall x\forall y\forall z[(Rxy\land Ryz)\rightarrow Rxz]$, и он определяет все транзитивные кадры

$\Diamond p\rightarrow \Diamond \Diamond p$ или $\Box \Box p\rightarrow \Box p$

Соответствующая ему формула первого порядка: $\forall x\forall y[Rxy\rightarrow \exists z(Rxz\land Rzy)]$, и он определяет все плотные кадры

$\Box p\rightarrow \Diamond p$

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

$\Diamond \Box p\rightarrow \Box \Diamond p$

Соответствующая ему формула первого порядка: $\forall x\forall x_{1}\forall z_{0}[Rxx_{1}\land Rxz_{0}\rightarrow \exists z_{1}(Rx_{1}z_{1}\land Rz_{0}z_{1})]$, и это собственность Чёрча-Россера .

Примеры формул, не относящихся к Салквисту

$\Box \Diamond p\rightarrow \Diamond \Box p$

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

$\Box (\Box p\rightarrow p)\rightarrow \Box p$

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

$(\Box \Diamond p\rightarrow \Diamond \Box p)\land (\Diamond \Diamond q\rightarrow \Diamond q)$

Соединение формулы МакКинси и аксиомы (4) имеет условие фрейма первого порядка (сопряжение свойства транзитивности со свойством $\forall x[\forall y(Rxy\rightarrow \exists z[Ryz])\rightarrow \exists y(Rxy\wedge \forall z[Ryz\rightarrow z=y])]$), но не эквивалентно какой-либо формуле Сальквиста.

Теорема Форса

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

Ссылки

• Л. А. Чагрова, 1991. Неразрешимая задача теории корреспонденции. Журнал символической логики 56: 1261–1272.
• Маркус Крахт, 1993. Как поженились теория полноты и соответствия. Ин де Рийке, редактор, «Бриллианты и дефолты» , страницы 175–214. Клювер.
• Хенрик Сальквист, 1975. Соответствие и полнота семантики первого и второго порядка модальной логики. В материалах Третьего скандинавского логического симпозиума . Северная Голландия, Амстердам.