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

---

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

Неформально в классической логике любое утверждение либо истинно, либо ложно. Это обуславливается законом исключённого третьего. В интуиционисткой логике это не так: утверждение может быть истинным, может быть ложным, а может быть невозможно установить, истинно оно или ложно. Последний случай можно интерпретировать так: можно допустить как мир, где это утверждение верно, так и мир, где оно неверно. На этом и основывается идея семантики Крипке.

В семантике Крипке рассматривается несколько миров, в каждом из которых истинность определена по разному. Утверждение истинное в одном мире может быть не истинно в другом. Между этими мирами задаётся отношение достижимости: некий мир считается достижимым из другого, если истинные утверждения базового мира сохраняются и в достижимом из него. То есть при переходе из мира в другой, но достижимый из данного, истинные утверждения сохраняются (однако могут появиться новые, которые в изначальном мире не были истинными). Это отношение предполагается рефлексивным и транзитивным. Такая структура называется шкалой (структурой) Крипке.

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

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

Моделью Крипке ${\displaystyle M}$ называется пара ${\displaystyle (F,v)}$, где ${\displaystyle F}$ — шкала Крипке, ${\displaystyle v:X\to {\mathcal {P}}(W)}$ — функция из множества пропозициональных переменных в множество всех подмножеств миров, называемая оценкой, удовлетворяющее следующему условию:

---