- Семантика Крипке
-
Семантика Крипке является распространенной семантикой для неклассических логик, таких как интуиционистская логика и модальная логика. Она была создана Солом Крипке в конце 1950х — начале 1960х годов. Это было большим достижением для развития теории моделей для неклассических логик.
Семантика для модальной логики
Рассмотрим одномодальные пропозициональные логики.
Шкалой Крипке
с одним отношением называется пара
, где
— это произвольное множество (часто говорят множество возможных миров), а
— отношение на
(множество стрелок или упорядоченных пар).
Моделью Крипке
называется пара
, где
— это оценка на шкале, которая каждой переменной ставит в соответствие множество миров, в которых эта переменная считается истинной. Формально оценку представляют, как функцию из множества переменных
в множество всех подмножеств
. Истинность в точке в модели Крипке обозначается с помощью знака
и определяется индукцией по длине формулы:
, если
, если
или
, если
Другие логические связки, такие как
,
и
можно выразить через
и
. Дуальный модальный оператор
выражается так
.
Аналогично можно определить семантику для многомодальных логик, для этого в шкале Крипке должно быть столько отношений, сколько есть модальностей в логике.
В этой статье не хватает ссылок на источники информации. Информация должна быть проверяема, иначе она может быть поставлена под сомнение и удалена.
Вы можете отредактировать эту статью, добавив ссылки на авторитетные источники.
Эта отметка установлена 14 мая 2011.Категория:- Логика
Wikimedia Foundation. 2010.