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

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

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

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

Шкалой (структурой) Крипке [math]\displaystyle{ F }[/math] с одним отношением называется пара [math]\displaystyle{ (W,R) }[/math], где [math]\displaystyle{ W }[/math] — это произвольное множество (часто говорят множество возможных миров), а [math]\displaystyle{ R\subset W\times W }[/math] — отношение на [math]\displaystyle{ W }[/math] (множество стрелок или упорядоченных пар), определяющее достижимость одного мира из другого.

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

[math]\displaystyle{ M, x\models p }[/math], если  [math]\displaystyle{ x\in V(p) }[/math]
[math]\displaystyle{ M, x\not\models \perp }[/math]
[math]\displaystyle{ M, x\models A \to B }[/math], если [math]\displaystyle{ M, x\not\models A }[/math] или [math]\displaystyle{ M, x\models B }[/math]
[math]\displaystyle{ M, x\models \Box A }[/math], если [math]\displaystyle{ \forall y:(x R y \Rightarrow M, y\models A) }[/math]

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

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