В отличие от обычной модальной логики, гибридная логика позволяет ссылаться на состояния (возможные миры) в своих правильных формулах[англ.].
Это достигается за счёт класса формул, называемых номиналами, которые истинны ровно в одном состоянии, а также за счёт использования оператора @, который определяется следующим образом:
@i p истинно тогда и только тогда, когда p истинно в единственном состоянии, названном номиналом i (то есть в состоянии, в котором i истинно).
Существуют гибридные логики с другими операторами, но @ является наиболее используемым.
Гибридные логики имеют много общих черт с темпоральной логикой (в которой иногда используют конструкции, подобные номиналам для обозначения конкретных моментов времени), и они являются богатым источником идей для исследователей современной модальной логики. Они также находят применение в области логики признаков, теории моделей, теории доказательств и логического анализа естественного языка. Гибридная логика также тесно связана с дескрипционной логикой, поскольку использование номиналов позволяет проводить рассуждения над общими (TBox) и частными (ABox) утверждениями.
Гибридная логика может быть рассмотрена как частный случай логики первого порядка с двумя видами переменных: пропозициональными и индивидными. Пропозициональные переменные соответствуют обычным модальным переменным, а индивидные переменные соответствуют номиналам. Оператор @ может быть определён как квантор по индивидным переменным: @i p эквивалентно ∃x (i = x ∧ p), где i = x означает, что i и x обозначают одно и то же состояние. Таким образом, гибридная логика может быть понята как фрагмент логики первого порядка с ограниченным использованием кванторов и равенства[источник не указан 420 дней].
Однако гибридная логика не тождественна логике первого порядка, так как она сохраняет некоторые свойства модальной логики, такие как бисимуляционная инвариантность, локальность и компактность. Бисимуляционная инвариантность означает, что два состояния в разных моделях являются логически эквивалентными тогда и только тогда, когда они связаны бисимуляцией, то есть отношением эквивалентности, которое сохраняет модальную структуру моделей. Локальность означает, что истинность формулы в состоянии зависит только от информации в этом состоянии и его непосредственных соседей. Компактность означает, что если множество формул имеет модель, то у него есть конечная подмодель[источник не указан 420 дней].
Классификация
Гибридная логика может быть классифицирована в зависимости от того, какие виды номиналов и операторов она использует. Самая базовая гибридная логика называется H(@) и содержит только оператор @ и константные номиналы (то есть номиналы без кванторов). Более выразительные гибридные логики могут добавлять другие операторы, такие как ↓ (связывает пропозициональную переменную с текущим состоянием), ↑ (связывает индивидную переменную с текущим состоянием), E (проверяет существование состояния с заданным свойством) или D (проверяет различие между двумя состояниями). Также можно добавлять кванторы по номиналам или по модальностям[источник не указан 420 дней].
Одна из наиболее распространенных систем, реализующих метод аналитических таблиц для гибридной логики называется HTab. Она является обобщением метода аналитических таблиц для модальной логики. HTab использует специальные правила вывода для операторов гибридной логики, а также правила для управления наборами номиналов и пропозициональных переменных. HTab является полной и разрешимой для гибридной логики H(@, A), то есть, она может доказать или опровергнуть любую формулу гибридной логики H(@, A) за конечное время[источник не указан 420 дней]. HTab также может строить модели для выполнимых формул, используя соответствующую технику[какие?][неизвестный термин]. HTab написан на функциональном языке Haskell, используя компилятор GHC. Код распространяется под лицензией GNU GPL[источник не указан 420 дней].
Braüner, Torben (2022). Zalta, Edward N.; Nodelman, Uri (eds.). "Hybrid Logic". The Stanford Encyclopedia of Philosophy (Winter 2022 ed.). Metaphysics Research Lab, Stanford University.