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

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

Семантика Крипке является распространенной семантикой для неклассических логик, таких как интуиционистская логика и модальная логика. Она была создана Солом Крипке в конце 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.

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