Kripke semantics (original) (raw)

A Kripke model (or simply a model) M for a propositional logical system (classical, intuitionistic, or modal) Λ is a pair (ℱ,V), where ℱ:=(W,R) is a Kripke frame, and V is a function that takes each atomic formula of Λ to a subset of W. If w∈V⁢(p), we say that p is true at world w. We say that M is a Λ-model based on the frame ℱ if M=(ℱ,V) is a model for the logic Λ.

Remark. Associated with each world w, we may also define a Boolean-valued valuation Vw on the set of all wff’s of Λ, so that Vw⁢(p)=1 iff w∈V⁢(p). In this sense, the Kripke semantics can be thought of as a generalization of the truth-value semantics for classical propositional logic. The truth-value semantics is just a Kripke model based on a frame with one world. Conversely, given a collection of valuations {Vw∣w∈W}, we have model (ℱ,V) where w∈V⁢(p) iff Vw⁢(p)=1.

Since the well-formed formulas (wff’s) of Λ are uniquely readable, V may be inductively extended so it is defined on all wff’s. The following are some examples:

• •
• •
  in the modal propositional logic K, V⁢(□⁢A):=V⁢(A)□, where S□:={u∣↑u⊆S}, and ↑u:={w∣u⁢R⁢w}, and
• •
  in intuitionistic propositional logic PLi, V(A→B):=(V(A)-V(B))#, where S#:=(↓S)c, and ↓S:={u∣u⁢R⁢w,w∈S}.

Truth at a world can now be defined for wff’s: a wff A is true at world w if w∈V⁢(A), and we write

if no confusion arises. If w∉V⁢(A), we write M⊧̸wA. The three examples above can be now interpreted as:

• •
  ⊧wA→B means ⊧wA implies ⊧wB in PLc,
• •
  ⊧w□⁢A means for all worlds v with w⁢R⁢v, we have ⊧vA in K, and
• •
  ⊧wA→B means for all worlds v with w⁢R⁢v, ⊧vA implies ⊧vB in PLi.

A wff A is said to be valid

• •
  in a model M if A in true at all possible worlds w in M,
• •
  in a frame if A is valid in all models M based on ℱ,
• •
  in a collection 𝒞 of frames if A is valid in all frames in 𝒞.

We denote

if A is valid in M,ℱ, or 𝒞 respectively.