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

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

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

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

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

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

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

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

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