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

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

Семантика для интуиционистской логики

Неформальное описание

Неформально в классической логике любое утверждение либо истинно, либо ложно. Это обуславливается законом исключённого третьего. В интуиционисткой логике это не так: утверждение может быть истинным, может быть ложным, а может быть невозможно установить, истинно оно или ложно. Последний случай можно интерпретировать так: можно допустить как мир, где это утверждение верно, так и мир, где оно неверно. На этом и основывается идея семантики Крипке.

В семантике Крипке рассматривается несколько миров, в каждом из которых истинность определена по разному. Утверждение истинное в одном мире может быть не истинно в другом. Между этими мирами задаётся отношение достижимости: некий мир считается достижимым из другого, если истинные утверждения базового мира сохраняются и в достижимом из него. То есть при переходе из мира в другой, но достижимый из данного, истинные утверждения сохраняются (однако могут появиться новые, которые в изначальном мире не были истинными). Это отношение предполагается рефлексивным и транзитивным. Такая структура называется шкалой (структурой) Крипке.

Модель Крипке получается, если для каждой пропозициональной переменной задать, в каких мирах она истинна, а в каких нет (то есть по сути выполнить подстановку конкретных значений для переменных).

Формальное определение

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

Моделью Крипке $M$ называется пара $(F,v)$, где $F$ — шкала Крипке, $v:X\to {\mathcal {P}}(W)$ — функция из множества пропозициональных переменных в множество всех подмножеств миров, называемая оценкой, удовлетворяющее следующему условию:

$\forall x\in X\ \forall w\in W\ \forall w'\in W,wRw':w\in v(x)\Rightarrow w'\in v(x)$ — монотонность оценки.

Оценка задаёт для каждой переменной в каких мирах она истинна, а в каких нет: если мир $w\in v(p)$, то переменная $p$ истинна в мире $w$, если $w\notin v(p)$, то переменная $p$ не истинна в мире $w$. Оценку иногда определяют и как функцию $v:W\to {\mathcal {P}}(X)$ или даже отношение $v\subseteq W\times X$. Важно лишь то, что оценка для каждой переменной и каждого мира задаёт, истинна ли она в этом мире или нет. Истинность переменной $x$ в мире $w$ модели $M$ обозначается как $M,w\models x$, не истинность — $M,w\not \models x$.

Монотонность оценки формализует требование, что истинность утверждений должна сохраняться в достижимых мирах. Если переменная истинна в каком-то мире, то она будет истинна и в любом достижимом из него мире.

Истинность формул в моделях Крипке задаётся следующим образом. Истинность формулы в мире $w$ из одной переменной равна истинности этой переменной в мире $w$ модели Крипке. Истинность логической связки в мире $w$ определяется следующим образом:

1. Для каждого мира, достижимого из $w$, считается результат по таблице истинности связки: причём если аргумент истинен в мире, он считается равным $1$, а если не истинен, то $0$;
2. Если во всех мирах, достижимых из $w$, получилось $1$, то формула считается истинной в мире $w$ модели $M$; если же хоть где-то получился $0$, то не истинной.

Истинность формулы $\varphi$ в мире $w$ модели $M$ обозначается как $M,w\models \varphi$, не истинность — $M,w\not \models \varphi$.

Частные случаи для конкретных логических связок:

$M,w\models \lnot \varphi$ если для любого мира $w'$ достижимого из $w$ выполнено $M,w\not \models \varphi$.

Если $\lnot \varphi$ истинна в мире $w$ модели $M$, то говорят, что формула $\varphi$ ложна в мире $w$ модели $M$. Как можно видеть, не истинность и ложность в семантике Крипке — это не одно и то же. Истинность в семантике Крипке — истинность во всех достижимых мирах, ложность — не истинность во всех достижимых мирах, но есть также третий случай, когда в одном из достижимых миров формула истинна, а в каком-то другом — не истинна. Тогда формула не истинна и не ложна одновременно. Закон исключённого третьего не работает.

$M,w\models \varphi \to \psi$ если для любого мира $w'$ достижимого из $w$ выполнено хотя бы одно из следующих утверждений: $M,w\not \models \varphi$ или $M,w\models \psi$.

Определение конъюнкции и дизъюнкции можно ограничить только проверкой в данном мире, так как если $\varphi$/$\psi$ будет истинны в данном мире, то оно будет истинно и в любом достижимом.

$M,w\models \varphi \land \psi$ если $M,w\models \varphi$ и $M,w\models \psi$.

$M,w\models \varphi \lor \psi$ если $M,w\models \varphi$ или $M,w\models \psi$.

Формулы также обладают свойством монотонности: если формула истинна в каком-то мире модели, то она истинна и в любом достижимом мире. Формулы бывают либо истинны, либо ложны, либо не истинны и не ложны одновременно; случай истинности и ложности одновременно в семантике Крипке невозможен.

Говорят, что формула истинна в модели Крипке $M$, если она истинна во всех мирах этой модели. Говорят, что формула истинна в шкале Крипке $F$, если она истинна в любой модели Крипке со шкалой $F$.

Семантика Крипке для интуиционисткой логики обладает следующими свойствами:

• Корректность: любая выводимая в интуиционистской логике формула будет истинна в любой модели Крипке.
• Полнота: если формула не выводится в интуиционистской логике, то существует модель Крипке, в которой она не истинна.

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

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

Шкалой (структурой) Крипке $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$.

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