Введение

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

Определение

Формулы Сальквиста строятся из импликаций, где следствие положительное, а антецедент имеет ограниченную форму. Атомарная формула в рамке – это пропозициональный атом, которому предшествует некоторое (возможно, 0) количество рамок, то есть формула вида (часто сокращаемая как для ). Антецедент Сальквиста – это формула, построенная с использованием ∧, ∨ и □ из атомарных формул в рамках и отрицательных формул (включая константы ⊥, ⊤). Импликация Сальквиста – это формула A → B, где A – антецедент Сальквиста, а B – положительная формула. Формула Сальквиста строится из импликаций Сальквиста с использованием ∧ и □ (неограниченно), а также с использованием ∨ для формул, не имеющих общих переменных.

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

Это формула Маккинзи; она не имеет условия рамки первого порядка. Аксиома Лёба не является аксиомой Сальквиста; опять же, она не имеет условия рамки первого порядка. Конъюнкция формулы Маккинзи и аксиомы (4) имеет условие рамки первого порядка (конъюнкция свойства транзитивности со свойством ), но не эквивалентна ни одной формуле Сальквиста.

Теорема Крахта

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