Kripke semantics


A Kripke frame (or simply a frame) is a pair (W,R) where W is a non-empty set whose elements are called worlds or possible worlds, R is a binary relationMathworldPlanetmath on W called the accessibility relation. When vRw, we say that w is accessible from v. A Kripke frame is said to have property P if R has the property P. For example, a symmetricPlanetmathPlanetmath frame is a frame whose accessibility relation is symmetric.

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 wV(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 wV(p). In this sense, the Kripke semantics can be thought of as a generalizationPlanetmathPlanetmath 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 collectionMathworldPlanetmath of valuations {VwwW}, we have model (,V) where wV(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 classical propositional logicPlanetmathPlanetmath PLc, V(AB):=V(A)cV(B), where Sc:=W-S,

  • in the modal propositional logic K, V(A):=V(A), where S:={uuS}, and u:={wuRw}, and

  • in intuitionistic propositional logic PLi, V(AB):=(V(A)-V(B))#, where S#:=(S)c, and S:={uuRw,wS}.

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

MwA  or  wA

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

  • wAB means wA implies wB in PLc,

  • wA means for all worlds v with wRv, we have vA in K, and

  • wAB means for all worlds v with wRv, 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

MA,A,or  𝒞A

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

A logic Λ, equipped with a deductive system, is sound in 𝒞 if

A  implies  𝒞A.

Here, A means that wff A is a theoremMathworldPlanetmath deducibleMathworldPlanetmath from the deductive system of Λ. Conversely, if

𝒞A  implies  A,

we say that Λ is completePlanetmathPlanetmathPlanetmathPlanetmath in 𝒞.

Title Kripke semantics
Canonical name KripkeSemantics
Date of creation 2013-03-22 19:31:15
Last modified on 2013-03-22 19:31:15
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 25
Author CWoo (3771)
Entry type Definition
Classification msc 03B48
Classification msc 03B20
Classification msc 03B45
Defines Kripke frame
Defines possible world
Defines accessibility relation
Defines accessible
Defines valid
Defines sound
Defines complete