Русская Википедия:Семантика Крипке

Содержание

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

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

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

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

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

Моделью Крипке <math>M</math> называется пара <math>(F,V)</math>, где <math>V</math> — это оценка на шкале, которая каждой переменной ставит в соответствие множество миров, в которых эта переменная считается истинной. Формально оценку представляют, как функцию из множества переменных <math>PL</math> в множество всех подмножеств <math>W</math>. Истинность в точке в модели Крипке обозначается с помощью знака <math>\models</math> и определяется индукцией по длине формулы:

<math>M, x\models p</math>, если  <math>x\in V(p)</math>
<math>M, x\not\models \perp</math>
<math>M, x\models A \to B</math>, если <math>M, x\not\models A</math> или <math>M, x\models B</math>
<math>M, x\models \Box A</math>, если <math>\forall y:(x R y \Rightarrow M, y\models A)</math>

Другие логические связки, такие как <math>\lor</math>, <math>\land</math> и <math>\lnot</math> можно выразить через <math>\to</math> и <math>\perp</math>. Дуальный модальный оператор <math>\Diamond</math> выражается так <math>\Diamond A\; \stackrel{def}{=}\; \lnot\Box\lnot A</math>.

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

Примечания

Шаблон:Logic-stub Шаблон:Нет ссылок