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

Семантика Кріпке є поширеною семантикою для некласичних логік, таких як інтуїціоністська логіка і модальна логіка. Її створив Саул Кріпке в кінці 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:(xRy\Rightarrow M,y\models A)$

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

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