Kripke semantics (also known as relational semantics or frame semantics, and often confused with possible world semantics) is a formal semantics for nonclassical logic systems created in the late 1950s and early 1960s by Saul Kripke. It was first made for modal logics, and later adapted to intuitionistic logic and other nonclassical systems. The discovery of Kripke semantics was a breakthrough in the theory of nonclassical logics, because the model theory of such logics was nonexistent before Kripke.
Semantics of modal logic
Main article:
modal logic
The language of propositional modal logic consists of a countably infinite set of propositional variables, a set of truthfunctional connectives (in this article $\backslash to$ and $\backslash neg$), and the modal operator $\backslash Box$ ("necessarily"). The modal operator $\backslash Diamond$ ("possibly") is the dual of $\backslash Box$ and may be defined in terms of it like so: $\backslash Diamond\; A:=\; \backslash neg\backslash Box\backslash neg\; A$ ("possibly A" is defined as equivalent to "not necessarily not A").
Basic definitions
A Kripke frame or modal frame is a pair $\backslash langle\; W,R\backslash rangle$, where W is a
nonempty set, and R is a binary relation on W. Elements
of W are called nodes or worlds, and R is known as the accessibility relation.
A Kripke model is a triple $\backslash langle\; W,R,\backslash Vdash\backslash rangle$, where
$\backslash langle\; W,R\backslash rangle$ is a Kripke frame, and $\backslash Vdash$ is a relation between
nodes of W and modal formulas, such that:
 $w\backslash Vdash\backslash neg\; A$ if and only if $w\backslash nVdash\; A$,
 $w\backslash Vdash\; A\backslash to\; B$ if and only if $w\backslash nVdash\; A$ or $w\backslash Vdash\; B$,
 $w\backslash Vdash\backslash Box\; A$ if and only if $u\backslash Vdash\; A$ for all $u$ such that $w\backslash ;\; R\backslash ;\; u$.
We read $w\backslash Vdash\; A$ as “w satisfies
A”, “A is satisfied in w”, or
“w forces A”. The relation $\backslash Vdash$ is called the
satisfaction relation, evaluation, or forcing relation.
The satisfaction relation is uniquely determined by its
value on propositional variables.
A formula A is valid in:
 a model $\backslash langle\; W,R,\backslash Vdash\backslash rangle$, if $w\backslash Vdash\; A$ for all w ∈ W,
 a frame $\backslash langle\; W,R\backslash rangle$, if it is valid in $\backslash langle\; W,R,\backslash Vdash\backslash rangle$ for all possible choices of $\backslash Vdash$,
 a class C of frames or models, if it is valid in every member of C.
We define Thm(C) to be the set of all formulas that are valid in
C. Conversely, if X is a set of formulas, let Mod(X) be the
class of all frames which validate every formula from X.
A modal logic (i.e., a set of formulas) L is sound with
respect to a class of frames C, if L ⊆ Thm(C). L is
complete wrt C if L ⊇ Thm(C).
Correspondence and completeness
Semantics is useful for investigating a logic (i.e. a derivation system) only if the semantic consequence relation reflects its syntactical counterpart, the syntactic consequence relation (derivability). It is vital to know which modal logics are sound and complete with respect to a class of Kripke frames, and to determine also which class that is.
For any class C of Kripke frames, Thm(C) is a normal modal logic (in particular, theorems of the minimal normal modal logic, K, are valid in every Kripke model). However, the converse does not hold in general. There are Kripke incomplete normal modal logics, which is not a problem, because most of the modal systems studied are complete of classes of frames described by simple conditions.
A normal modal logic L corresponds to a class of frames C, if C = Mod(L). In other words, C is the largest class of frames such that L is sound wrt C. It follows that L is Kripke complete if and only if it is complete of its corresponding class.
Consider the schema T : $\backslash Box\; A\backslash to\; A$.
T is valid in any reflexive frame $\backslash langle\; W,R\backslash rangle$: if
$w\backslash Vdash\; \backslash Box\; A$, then $w\backslash Vdash\; A$
since w R w. On the other hand, a frame which
validates T has to be reflexive: fix w ∈ W, and
define satisfaction of a propositional variable p as follows:
$u\backslash Vdash\; p$ if and only if w R u. Then
$w\backslash Vdash\; \backslash Box\; p$, thus $w\backslash Vdash\; p$
by T, which means w R w using the definition of
$\backslash Vdash$. T corresponds to the class of reflexive
Kripke frames.
It is often much easier to characterize the corresponding class of
L than to prove its completeness, thus correspondence serves as a
guide to completeness proofs. Correspondence is also used to show
incompleteness of modal logics: suppose
L_{1} ⊆ L_{2} are normal modal logics that
correspond to the same class of frames, but L_{1} does not
prove all theorems of L_{2}. Then L_{1} is
Kripke incomplete. For example, the schema $\backslash Box(A\backslash equiv\backslash Box\; A)\backslash to\backslash Box\; A$ generates an incomplete logic, as it
corresponds to the same class of frames as GL (viz. transitive and
converse wellfounded frames), but does not prove the GLtautology $\backslash Box\; A\backslash to\backslash Box\backslash Box\; A$.
The table below is a list of common modal axioms together with their
corresponding classes. The naming of the axioms often varies.
Common modal axiom schemata
Name 
Axiom 
Frame condition

K

$\backslash Box\; (A\backslash to\; B)\backslash to(\backslash Box\; A\backslash to\; \backslash Box\; B)$

N/A

T

$\backslash Box\; A\backslash to\; A$

reflexive: $w\backslash ,R\backslash ,w$

4

$\backslash Box\; A\backslash to\backslash Box\backslash Box\; A$

transitive: $w\backslash ,R\backslash ,v\; \backslash wedge\; v\backslash ,R\backslash ,u\; \backslash Rightarrow\; w\backslash ,R\backslash ,u$


$\backslash Box\backslash Box\; A\backslash to\backslash Box\; A$

dense: $w\backslash ,R\backslash ,u\backslash Rightarrow\; \backslash exists\; v\backslash ,(w\backslash ,R\backslash ,v\; \backslash land\; v\backslash ,R\backslash ,u)$

D

$\backslash Box\; A\backslash to\backslash Diamond\; A$ or $\backslash Diamond\backslash top$

serial: $\backslash forall\; w\backslash ,\backslash exists\; v\backslash ,(w\backslash ,R\backslash ,v)$

B

$A\backslash to\backslash Box\backslash Diamond\; A$

symmetric : $w\backslash ,R\backslash ,v\; \backslash Rightarrow\; v\backslash ,R\backslash ,w$

5

$\backslash Diamond\; A\backslash to\backslash Box\backslash Diamond\; A$

Euclidean: $w\backslash ,R\backslash ,u\backslash land\; w\backslash ,R\backslash ,v\backslash Rightarrow\; u\backslash ,R\backslash ,v$

GL

$\backslash Box(\backslash Box\; A\backslash to\; A)\backslash to\backslash Box\; A$

R transitive, R^{−1} wellfounded

Grz

$\backslash Box(\backslash Box(A\backslash to\backslash Box\; A)\backslash to\; A)\backslash to\; A$

R reflexive and transitive, R^{−1}−Id wellfounded

H

$\backslash Box(\backslash Box\; A\backslash to\; B)\backslash lor\backslash Box(\backslash Box\; B\backslash to\; A)$

$w\backslash ,R\backslash ,u\backslash land\; w\backslash ,R\backslash ,v\backslash Rightarrow\; u\backslash ,R\backslash ,v\backslash lor\; v\backslash ,R\backslash ,u$

M

$\backslash Box\backslash Diamond\; A\backslash to\backslash Diamond\backslash Box\; A$

(a complicated secondorder property)

G

$\backslash Diamond\backslash Box\; A\backslash to\backslash Box\backslash Diamond\; A$

$w\backslash ,R\backslash ,u\backslash land\; w\backslash ,R\backslash ,v\backslash Rightarrow\backslash exists\; x\backslash ,(u\backslash ,R\backslash ,x\backslash land\; v\backslash ,R\backslash ,x)$


$A\backslash to\backslash Box\; A$

$w\backslash ,R\backslash ,v\backslash Rightarrow\; w=v$


$\backslash Diamond\; A\backslash to\backslash Box\; A$

partial function: $w\backslash ,R\backslash ,u\backslash land\; w\backslash ,R\backslash ,v\backslash Rightarrow\; u=v$


$\backslash Diamond\; A\backslash leftrightarrow\backslash Box\; A$

function: $\backslash forall\; w\backslash ,\backslash exists!u\backslash ,\; w\backslash ,R\backslash ,u$


$\backslash Box\; A$ or $\backslash Box\; \backslash bot$

empty: $\backslash forall\; w\backslash ,\backslash forall\; u\backslash ,\; \backslash neg\; (\; w\backslash ,\; R\backslash ,u)$

Here is a list of several common modal systems. Frame conditions for
some of them were simplified: the logics are
complete with respect to the frame classes given in the table, but
they may correspond to a larger class of frames.
Common normal modal logics
name 
axioms 
frame condition

K

—

all frames

T

T

reflexive

K4

4

transitive

S4

T, 4

preorder

S5

T, 5 or D, B, 4

equivalence relation

S4.3

T, 4, H

total preorder

S4.1

T, 4, M

preorder, $\backslash forall\; w\backslash ,\backslash exists\; u\backslash ,(w\backslash ,R\backslash ,u\backslash land\backslash forall\; v\backslash ,(u\backslash ,R\backslash ,v\backslash Rightarrow\; u=v))$

S4.2

T, 4, G

directed preorder

GL

GL or 4, GL

finite strict partial order

Grz, S4Grz

Grz or T, 4, Grz

finite partial order

D

D

serial

D45

D, 4, 5

transitive, serial, and Euclidean

Canonical models
For any normal modal logic L, a Kripke model (called the canonical model) can be constructed, which validates precisely the theorems of
L, by an adaptation of the standard technique of using maximal consistent sets as models. Canonical Kripke models play a
role similar to the Lindenbaum–Tarski algebra construction in algebraic
semantics.
A set of formulas is Lconsistent if no contradiction can be derived from it using the theorems of L, and Modus Ponens. A maximal Lconsistent set (an LMCS
for short) is an Lconsistent set which has no proper Lconsistent superset.
The canonical model of L is a Kripke model
$\backslash langle\; W,R,\backslash Vdash\backslash rangle$, where W is the set of all LMCS,
and the relations R and $\backslash Vdash$ are as follows:
 $X\backslash ;R\backslash ;Y$ if and only if for every formula $A$, if $\backslash Box\; A\backslash in\; X$ then $A\backslash in\; Y$,
 $X\backslash Vdash\; A$ if and only if $A\backslash in\; X$.
The canonical model is a model of L, as every LMCS contains
all theorems of L. By Zorn's lemma, each Lconsistent set
is contained in an LMCS, in particular every formula
unprovable in L has a counterexample in the canonical model.
The main application of canonical models are completeness proofs. Properties of the canonical model of K immediately imply completeness of K with respect to the class of all Kripke frames.
This argument does not work for arbitrary L, because there is no guarantee that the underlying frame of the canonical model satisfies the frame conditions of L.
We say that a formula or a set X of formulas is canonical
with respect to a property P of Kripke frames, if
 X is valid in every frame which satisfies P,
 for any normal modal logic L which contains X, the underlying frame of the canonical model of L satisfies P.
A union of canonical sets of formulas is itself canonical.
It follows from the preceding discussion that any logic axiomatized by
a canonical set of formulas is Kripke complete, and
compact.
The axioms T, 4, D, B, 5, H, G (and thus
any combination of them) are canonical. GL and Grz are not
canonical, because they are not compact. The axiom M by itself is
not canonical (Goldblatt, 1991), but the combined logic S4.1 (in
fact, even K4.1) is canonical.
In general, it is undecidable whether a given axiom is
canonical. We know a nice sufficient condition: H.
Sahlqvist identified a broad class of formulas (now called
Sahlqvist formulas) such that
 a Sahlqvist formula is canonical,
 the class of frames corresponding to a Sahlqvist formula is firstorder definable,
 there is an algorithm which computes the corresponding frame condition to a given Sahlqvist formula.
This is a powerful criterion: for example, all axioms
listed above as canonical are (equivalent to) Sahlqvist formulas.
Finite model property
A logic has the finite model property (FMP) if it is complete
with respect to a class of finite frames. An application of this
notion is the decidability question: it
follows from
Post's theorem that a recursively axiomatized modal logic L
which has FMP is decidable, provided it is decidable whether a given
finite frame is a model of L. In particular, every finitely
axiomatizable logic with FMP is decidable.
There are various methods for establishing FMP for a given logic.
Refinements and extensions of the canonical model construction often
work, using tools such as filtration or
unravelling. As another possibility,
completeness proofs based on cutfree
sequent calculi usually produce finite models
directly.
Most of the modal systems used in practice (including all listed
above) have FMP.
In some cases, we can use FMP to prove Kripke completeness of a logic:
every normal modal logic is complete with respect to a class of
modal algebras, and a finite modal algebra can be transformed
into a Kripke frame. As an example, Robert Bull proved using this method
that every normal extension of S4.3 has FMP, and is Kripke
complete.
Multimodal logics
Kripke semantics has a straightforward generalization to logics with
more than one modality. A Kripke frame for a language with
$\backslash \{\backslash Box\_i\backslash mid\backslash ,i\backslash in\; I\backslash \}$ as the set of its necessity operators
consists of a nonempty set W equipped with binary relations
R_{i} for each i ∈ I. The definition of a
satisfaction relation is modified as follows:
 $w\backslash Vdash\backslash Box\_i\; A$ if and only if $\backslash forall\; u\backslash ,(w\backslash ;R\_i\backslash ;u\backslash Rightarrow\; u\backslash Vdash\; A).$
A simplified semantics, discovered by Tim Carlson, is often used for
polymodal provability logics. A Carlson model is a structure
$\backslash langle\; W,R,\backslash \{D\_i\backslash \}\_\{i\backslash in\; I\},\backslash Vdash\backslash rangle$
with a single accessibility relation R, and subsets
D_{i} ⊆ W for each modality. Satisfaction is
defined as
 $w\backslash Vdash\backslash Box\_i\; A$ if and only if $\backslash forall\; u\backslash in\; D\_i\backslash ,(w\backslash ;R\backslash ;u\backslash Rightarrow\; u\backslash Vdash\; A).$
Carlson models are easier to visualize and to work with than usual
polymodal Kripke models; there are, however, Kripke complete polymodal
logics which are Carlson incomplete.
Semantics of intuitionistic logic
Kripke semantics for the intuitionistic logic follows the same
principles as the semantics of modal logic, but it uses a different
definition of satisfaction.
An intuitionistic Kripke model is a triple
$\backslash langle\; W,\backslash le,\backslash Vdash\backslash rangle$, where $\backslash langle\; W,\backslash le\backslash rangle$ is a preordered Kripke frame, and $\backslash Vdash$ satisfies the following conditions:
 if p is a propositional variable, $w\backslash le\; u$, and $w\backslash Vdash\; p$, then $u\backslash Vdash\; p$ (persistency condition),
 $w\backslash Vdash\; A\backslash land\; B$ if and only if $w\backslash Vdash\; A$ and $w\backslash Vdash\; B$,
 $w\backslash Vdash\; A\backslash lor\; B$ if and only if $w\backslash Vdash\; A$ or $w\backslash Vdash\; B$,
 $w\backslash Vdash\; A\backslash to\; B$ if and only if for all $u\backslash ge\; w$, $u\backslash Vdash\; A$ implies $u\backslash Vdash\; B$,
 not $w\backslash Vdash\backslash bot$.
The negation of A, ¬A, could be defined as an abbreviation for A → ⊥. If for all u such that w ≤ u, not u ⊩ A, then w ⊩ A → ⊥ is vacuously true, so w ⊩ ¬A.
Intuitionistic logic is sound and complete with respect to its Kripke
semantics, and it has FMP.
Intuitionistic firstorder logic
Let L be a firstorder language. A Kripke
model of L is a triple
$\backslash langle\; W,\backslash le,\backslash \{M\_w\backslash \}\_\{w\backslash in\; W\}\backslash rangle$, where
$\backslash langle\; W,\backslash le\backslash rangle$ is an intuitionistic Kripke frame, M_{w} is a
(classical) Lstructure for each node w ∈ W, and
the following compatibility conditions hold whenever u ≤ v:
 the domain of M_{u} is included in the domain of M_{v},
 realizations of function symbols in M_{u} and M_{v} agree on elements of M_{u},
 for each nary predicate P and elements a_{1},…,a_{n} ∈ M_{u}: if P(a_{1},…,a_{n}) holds in M_{u}, then it holds in M_{v}.
Given an evaluation e of variables by elements of M_{w}, we
define the satisfaction relation $w\backslash Vdash\; A[e]$:
 $w\backslash Vdash\; P(t\_1,\backslash dots,t\_n)[e]$ if and only if $P(t\_1[e],\backslash dots,t\_n[e])$ holds in M_{w},
 $w\backslash Vdash(A\backslash land\; B)[e]$ if and only if $w\backslash Vdash\; A[e]$ and $w\backslash Vdash\; B[e]$,
 $w\backslash Vdash(A\backslash lor\; B)[e]$ if and only if $w\backslash Vdash\; A[e]$ or $w\backslash Vdash\; B[e]$,
 $w\backslash Vdash(A\backslash to\; B)[e]$ if and only if for all $u\backslash ge\; w$, $u\backslash Vdash\; A[e]$ implies $u\backslash Vdash\; B[e]$,
 not $w\backslash Vdash\backslash bot[e]$,
 $w\backslash Vdash(\backslash exists\; x\backslash ,A)[e]$ if and only if there exists an $a\backslash in\; M\_w$ such that $w\backslash Vdash\; A[e(x\backslash to\; a)]$,
 $w\backslash Vdash(\backslash forall\; x\backslash ,A)[e]$ if and only if for every $u\backslash ge\; w$ and every $a\backslash in\; M\_u$, $u\backslash Vdash\; A[e(x\backslash to\; a)]$.
Here e(x→a) is the evaluation which gives x the
value a, and otherwise agrees with e.
See a slightly different formalization in.^{[1]}
Kripke–Joyal semantics
As part of the independent development of sheaf theory, it was realised around 1965 that Kripke semantics was intimately related to the treatment of existential quantification in topos theory.^{[2]} That is, the 'local' aspect of existence for sections of a sheaf was a kind of logic of the 'possible'. Though this development was the work of a number of people, the name Kripke–Joyal semantics is often used in this connection.
Model constructions
As in the classical model theory, there are methods for
constructing a new Kripke model from other models.
The natural homomorphisms in Kripke semantics are called
pmorphisms (which is short for pseudoepimorphism, but the
latter term is rarely used). A pmorphism of Kripke frames
$\backslash langle\; W,R\backslash rangle$ and $\backslash langle\; W\text{'},R\text{'}\backslash rangle$ is a mapping
$f\backslash colon\; W\backslash to\; W\text{'}$ such that
 f preserves the accessibility relation, i.e., u R v implies f(u) R’ f(v),
 whenever f(u) R’ v’, there is a v ∈ W such that u R v and f(v) = v’.
A pmorphism of Kripke models $\backslash langle\; W,R,\backslash Vdash\backslash rangle$ and
$\backslash langle\; W\text{'},R\text{'},\backslash Vdash\text{'}\backslash rangle$ is a pmorphism of their
underlying frames $f\backslash colon\; W\backslash to\; W\text{'}$, which
satisfies
 $w\backslash Vdash\; p$ if and only if $f(w)\backslash Vdash\text{'}p$, for any propositional variable p.
Pmorphisms are a special kind of bisimulations. In general, a
bisimulation between frames $\backslash langle\; W,R\backslash rangle$ and
$\backslash langle\; W\text{'},R\text{'}\backslash rangle$ is a relation
B ⊆ W × W’, which satisfies
the following “zigzag” property:
 if u B u’ and u R v, there exists v’ ∈ W’ such that v B v’ and u’ R’ v’,
 if u B u’ and u’ R’ v’, there exists v ∈ W such that v B v’ and u R v.
A bisimulation of models is additionally required to preserve forcing
of atomic formulas:
 if w B w’, then $w\backslash Vdash\; p$ if and only if $w\text{'}\backslash Vdash\text{'}p$, for any propositional variable p.
The key property which follows from this definition is that
bisimulations (hence also pmorphisms) of models preserve the
satisfaction of all formulas, not only propositional variables.
We can transform a Kripke model into a tree using
unravelling. Given a model $\backslash langle\; W,R,\backslash Vdash\backslash rangle$ and a fixed
node w_{0} ∈ W, we define a model
$\backslash langle\; W\text{'},R\text{'},\backslash Vdash\text{'}\backslash rangle$, where W’ is the
set of all finite sequences
$s=\backslash langle\; w\_0,w\_1,\backslash dots,w\_n\backslash rangle$ such
that w_{i} R w_{i+1} for all
i < n, and $s\backslash Vdash\; p$ if and only if
$w\_n\backslash Vdash\; p$ for a propositional variable
p. The definition of the accessibility relation R’
varies; in the simplest case we put
 $\backslash langle\; w\_0,w\_1,\backslash dots,w\_n\backslash rangle\backslash ;R\text{'}\backslash ;\backslash langle\; w\_0,w\_1,\backslash dots,w\_n,w\_\{n+1\}\backslash rangle$,
but many applications need the reflexive and/or transitive closure of
this relation, or similar modifications.
Filtration is a useful construction which uses to prove FMP for many logics. Let X be a set of
formulas closed under taking subformulas. An Xfiltration of a
model $\backslash langle\; W,R,\backslash Vdash\backslash rangle$ is a mapping f from W to a model
$\backslash langle\; W\text{'},R\text{'},\backslash Vdash\text{'}\backslash rangle$ such that
 f is a surjection,
 f preserves the accessibility relation, and (in both directions) satisfaction of variables p ∈ X,
 if f(u) R’ f(v) and $u\backslash Vdash\backslash Box\; A$, where $\backslash Box\; A\backslash in\; X$, then $v\backslash Vdash\; A$.
It follows that f preserves satisfaction of all formulas from
X. In typical applications, we take f as the projection
onto the quotient of W over the relation
 u ≡_{X} v if and only if for all A ∈ X, $u\backslash Vdash\; A$ if and only if $v\backslash Vdash\; A$.
As in the case of unravelling, the definition of the accessibility
relation on the quotient varies.
General frame semantics
The main defect of Kripke semantics is the existence of Kripke incomplete logics, and logics which are complete but not compact. It can be remedied by equipping Kripke frames with extra structure which restricts the set of possible valuations, using ideas from algebraic semantics. This gives rise to the general frame semantics.
Computer science applications
Main articles:
Kripke structure,
state transition system and
model checking
Blackburn et al. (2001) point out that because a relational structure is simply a set together with a collection of relations on that set, it is unsurprising that relational structures are to be found just about everywhere. As an example from theoretical computer science, they give labeled transition systems, which model program execution. Blackburn et al. thus claim because of this connection that modal languages are ideally suited in providing "internal, local perspective on relational structures." (p. xii)
History and terminology
Kripke semantics does not originate with Kripke, but instead the idea of giving semantics in the style given above, that is based on valuations made that are relative to nodes, predates Kripke by a long margin:
 Rudolf Carnap seems to have been the first to have the idea that one can give a possible world semantics for the modalities of necessity and possibility by means of giving the valuation function a parameter that ranges over Leibnizian possible worlds. Bayart develops this idea further, but neither gave recursive definitions of satisfaction in the style introduced by Tarski;
 J.C.C. McKinsey and Alfred Tarski developed an approach to modeling modal logics that is still influential in modern research, namely the algebraic approach, in which Boolean algebras with operators are used as models. Bjarni Jónsson and Tarski established the representability of Boolean algebras with operators in terms of frames. If the two ideas had been put together, the result would have been precisely frame models, which is to say Kripke models, years before Kripke. But no one (not even Tarski) saw the connection at the time.
 Arthur Prior, building on unpublished work of C. A. Meredith, developed a translation of sentential modal logic into classical predicate logic that, if he had combined it with the usual model theory for the latter, would have produced a model theory equivalent to Kripke models for the former. But his approach was resolutely syntactic and antimodeltheoretic.
 Stig Kanger gave a rather more complex approach to the interpretation of modal logic, but one that contains many of the key ideas of Kripke's approach. He first noted the relationship between conditions on accessibility relations and Lewisstyle axioms for modal logic. Kanger failed, however, to give a completeness proof for his system;
 Jaakko Hintikka gave a semantics in his papers introducing epistemic logic that is a simple variation of Kripke's semantics, equivalent to the characterisation of valuations by means of maximal consistent sets. He doesn't give inference rules for epistemic logic, and so cannot give a completeness proof;
 Richard Montague had many of the key ideas contained in Kripke's work, but he did not regard them as significant, because he had no completeness proof, and so did not publish until after Kripke's papers had created a sensation in the logic community;
 Evert Willem Beth presented a semantics of intuitionistic logic based on trees, which closely resembles Kripke semantics, except for using a more cumbersome definition of satisfaction.
Though the essential ideas of Kripke semantics were very much in the air by the time Kripke first published, Saul Kripke's work on modal logic is rightly regarded as groundbreaking. Most importantly, it was Kripke who proved the completeness theorems for modal logic, and Kripke who identified the weakest normal modal logic.
Despite the seminal contribution of Kripke's work, many modal logicians deprecate the term Kripke semantics as disrespectful of the important contributions these other pioneers made. The other most widely used term possible world semantics is deprecated as inappropriate when applied to modalities other than possibility and necessity, such as in epistemic or deontic logic. Instead they prefer the terms relational semantics or frame semantics. The use of "semantics" for "model theory" has been objected to as well, on the grounds that it invites confusion with linguistic semantics: whether the apparatus of "possible worlds" that appears in models has anything to do with the linguistic meaning of modal constructions in natural language is a contentious issue.
Notes
See also
References
 Blackburn, P., M. de Rijke, and Y. Venema, 2001. Modal Logic. Cambridge University Press.
 Bull, Robert. A., and K. Segerberg, 1984, "Basic Modal Logic" in The Handbook of Philosophical Logic, vol. 2. Kluwer: 1–88.
 Chagrov, A, and Zakharyaschev, M., 1997. Modal Logic. Oxford University Press.
 Michael Dummett, 1977. Elements of Intuitionism. Oxford Univ. Press.
 Fitting, Melvin, 1969. Intuitionistic Logic, Model Theory and Forcing. North Holland.
 Robert Goldblatt Mathematical Modal Logic: a View of its Evolution", In Logic & the Modalities in the Twentieth Century, volume 7 of the Handbook of the History of Logic, edited by Dov M. Gabbay and John Woods, Elsevier, 2006, 198.
 Hughes, G. E., and M. J. Cresswell, 1996. A New Introduction to Modal Logic. Routledge.
 Saunders Mac Lane and Moerdijk, I., 1991. Sheaves in Geometry and Logic. SpringerVerlag.
 van Dalen, Dirk, 1986, "Intuitionistic Logic" in The Handbook of Philosophical Logic, vol. 3. Reidel: 225–339.
External links
 Modal Logic" — by James Garson.
 Joan Moschovakis. Published in Stanford Encyclopedia of Philosophy.
 Detlovs and Podnieks, K., "Constructive Propositional Logic — Kripke Semantics." Chapter 4.4 of Introduction to Mathematical Logic. N.B: Constructive = intuitionistic.
 Burgess, John P., "Kripke Models."
 Template:Springerde:KripkeSemantik
pt:Semânticas_de_Kripke
This article was sourced from Creative Commons AttributionShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and USA.gov, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for USA.gov and content contributors is made possible from the U.S. Congress, EGovernment Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a nonprofit organization.