Введение

Формальная семантика для неклассических логических систем

Семантика Крипке (также известная как реляционная семантика или семантика фреймов, и часто путаемая с возможной семантикой миров) — это формальная семантика для неклассических логических систем, разработанная в конце 1950-х и начале 1960-х годов Саулом Крипке и Андре Жуайялем. Изначально она была разработана для модальных логик, а затем адаптирована для интуиционистской логики и других неклассических систем. Разработка семантики Крипке стала прорывом в теории неклассических логик, поскольку до работ Крипке теория моделей для таких логик практически отсутствовала (алгебраическая семантика существовала, но считалась «синтаксисом под видом семантики»).

Семантика модальной логики

Язык пропозициональной модальной логики состоит из счетно бесконечного множества пропозициональных переменных, множества функциональных связок истинности (в данной статье ∧ и ∨), и модального оператора □ ("необходимо"). Модальный оператор ◇ ("возможно") является (классически) двойственным к □ и может быть определен через необходимость следующим образом: ◇A определяется как эквивалент ¬□¬A.

Семантика Крипке Джояля

В рамках независимого развития теории снопов, около 1965 года стало ясно, что семантика Крипке тесно связана с рассмотрением экзистенциальной квантификации в теории топосов. А именно, "локальный" аспект существования для сечений снопа представлял собой своего рода логику "возможного". Хотя это развитие было результатом работы многих исследователей, в этой связи часто используется термин "семантика Крипке — Жуайяля".

Семантика общего фрейма

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

Приложения в области информатики

Блэкберн и др. (2001) отмечают, что поскольку реляционная структура – это просто множество вместе с набором отношений на этом множестве, неудивительно, что реляционные структуры встречаются повсюду. В качестве примера из теоретической информатики они приводят системы с помеченными переходами, которые моделируют выполнение программ. Таким образом, Блэкберн и др. утверждают, что благодаря этой связи модальные языки идеально подходят для предоставления "внутренней, локальной перспективы на реляционные структуры" (с. xii).