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

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

Інші логічні зв'язки, такі як $\vee$, $\wedge$ і $\mathrm{\neg }$ можна виразити через $\to$ і $\perp$. Дуальний модальний оператор $◊$ виражається так: $◊A\stackrel{def}{=}\mathrm{\neg }◻\mathrm{\neg }A$.

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