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

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

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

Семантика для модальной логики[править | править вики-текст]

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

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

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

, если  

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

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

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