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

Семантика Кріпке є поширеною семантикою для некласичних логік, таких як інтуїціоністська логіка і модальна логіка. Її створив Саул Кріпке в кінці 1950-х — початку 1960-х років. Це було значним досягненням у розвитку теорії моделей для некласичних логік.

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

Розглянемо одномодальні пропозиціональні логіки.

Шкалою (структурою) Кріпке ${\displaystyle F}$ з одним відношенням називається пара ${\displaystyle (W,R)}$, де ${\displaystyle W}$ — це довільна множина (часто кажуть, множина можливих світів), а ${\displaystyle R\subset W\times W}$ — відношення на ${\displaystyle W}$ (множина стрілок або впорядкованих пар), що визначає досяжність одного світу з іншого.

Моделлю Кріпке ${\displaystyle M}$ називається пара ${\displaystyle (F,V)}$, де ${\displaystyle V}$ — це оцінка на шкалі, яка кожній змінній ставить у відповідність множину світів, у яких ця змінна вважається істинною. Формально оцінку подають, як функцію з множини змінних ${\displaystyle PL}$ у множину всіх підмножин ${\displaystyle W}$. Істинність у точці в моделі Кріпке позначається знаком ${\displaystyle \models }$ і визначається індукцією за довжиною формули:

${\displaystyle M,x\models p}$, якщо ${\displaystyle x\in V(p)}$
${\displaystyle M,x\not \models \perp }$
${\displaystyle M,x\models A\to B}$, якщо ${\displaystyle M,x\not \models A}$ або ${\displaystyle M,x\models B}$
${\displaystyle M,x\models \Box A}$, якщо ${\displaystyle \forall y:(xRy\Rightarrow M,y\models A)}$

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

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