Семантика Крипке модальной логики.

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

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

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

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

Моделью Крипке называется пара , где — это оценка на шкале, которая каждой переменной ставит в соответствие множество миров, в которых эта переменная считается истинной. Формально оценку представляют, как функцию из множества переменных в множество всех подмножеств . Истинность в точке в модели Крипке обозначается с помощью знака и определяется индукцией по длине формулы:

, если  , если  или , если 

Другие логические связки, такие как , и можно выразить через и . Дуальный модальный оператор выражается так .

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

Из документа

W – множество возможных «миров»

R – двуместное отношение на W(отношение достижимости)

w₁Rw₂ .

v(w, Ф) – значение истинности

v(w, Ф) = 1, либо w |= Ф

v(w, Ф) = 0, либо w |¹ Ф

w |= ФÙY Û w |= Ф и w |= Y

w |= ФÚY Û w |= Ф или w |= Y

w |= ØФ Û w |¹ Ф

w |= Ф Û "w’ : wRw’  w’ |= Ф

w |= àФ Û $w’ : wRw’  w’ |= Ф

G – начальный мир G € W

K = <W, R, v, G>

Формула, называется истинной в семантике Крипке, если она истина в начальном мире.

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