Определение

Семантика Крипке для S4.

Интерпретация Крипке Kp=<W, w₀, R, φ>.

W={w₁,…, w_n,.. } – множество миров;

w₀ W – реальный мир;

R(u, v): u,v W – отношение достижимости;

(w, A_i) {0, 1} – функция означивания.

Дополнительные условия для S4

Рефлексивность и транзитивность отношения достижимости R:

- для любого мира u R(u, u), т.е. каждый мир достижим сам из себя

- .

Определение истинностного значения сложных формул

в каждом мире осуществляется по следующим правилам:

φ(w, f)= 0

φ(w, F₁&F₂)= φ(w, F₁)&φ(w, F₂),

φ(w, F₁ F₂)= φ(w, F₁) φ(w, F₂),

φ(w, F₁ F₂)= φ(w, F₁) φ(w, F₂),

φ(w, F)= φ(w, F),

т.е. пока все как в классическом исчислении высказываний,

φ(w, □ F)=1 u (R(w, u) φ(u, F)=1)

Определение.

Формула F формальной системы S4называется истинной в интерпретации Крипке для S4 K=<W, w₀, R, >, когда она принимает значение 1 в реальном мире w₀.