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

Семантика Крипке является распространенной семантикой для неклассических логик, таких как интуиционистская логика и модальная логика. Она была создана Солом Крипке в конце 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$, если $Mx\not \models A$ или $M,x\models B$
$M,x\models \Box A$, если $\forall y:(xRy\Rightarrow M,y\models A)$

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

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