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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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