Семантика Крипке

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

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

Рассмотрим одномодальные пропозициональные логики.

Шкалой Крипке $F$ с одним отношением называется пара $(W,R)$, где $W$ — это произвольное множество (часто говорят множество возможных миров), а $R\subset W\times W$ — отношение на $W$ (множество стрелок или упорядоченных пар).

Моделью Крипке $M$ называется пара $(F,V)$, где $V$ — это оценка на шкале, которая каждой переменной ставит в соответствие множество миров, в которых эта переменная считается истинной. Формально оценку представляют, как функцию из множества переменных $PL$ в множество всех подмножеств $W$. Истинность в точке в модели Крипке обозначается с помощью знака $\models$ и определяется индукцией по длине формулы:

$M, x\models p$, если  $x\in V(p)$
$M, x\not\models \perp$
$M, x\models A \to B$, если $M x\not\models A$ или $M, x\models B$
$M, x\models \Box A$, если $\forall y:(x R y \Rightarrow M, y\models A)$

Другие логические связки, такие как $\lor$, $\land$ и $\lnot$ можно выразить через $\to$ и $\perp$. Дуальный модальный оператор $\Diamond$ выражается так $\Diamond A\; \stackrel{def}{=}\; \lnot\Box\lnot A$.

Аналогично можно определить семантику для многомодальных логик, для этого в шкале Крипке должно быть столько отношений, сколько есть модальностей в логике.