Kripke semantics

Kripke semantics (also known as relational semantics or frame semantics, and often confused with possible world semantics) is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke and André Joyal. It was first conceived for modal logics, and later adapted to intuitionistic logic and other non-classical systems. The development of Kripke semantics was a breakthrough in the theory of non-classical logics, because the model theory of such logics was almost non-existent before Kripke (algebraic semantics existed, but were considered 'syntax in disguise').
Semantics of modal logic.
The language of propositional modal logic consists of a countably infinite set of propositional variables, a set of truth-functional connectives (in this article formula_1 and formula_2), and the modal operator formula_3 ("necessarily"). The modal operator formula_4 ("possibly") is (classically) the dual of formula_3 and may be defined in terms of necessity like so: formula_6 ("possibly A" is defined as equivalent to "not necessarily not A").
Basic definitions.
A Kripke frame or modal frame is a pair formula_7, where "W" is a (possibly empty) 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 formula_8, where
formula_7 is a Kripke frame, and formula_10 is a relation between nodes of "W" and modal formulas, such that for all "w" ∈ "W" and modal formulas A and B:
We read formula_20 as “"w" satisfies
"A"”, “"A" is satisfied in "w"”, or
“"w" forces "A"”. The relation formula_10 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:
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: while most of the modal systems studied are complete of classes of frames described by simple conditions, 
Kripke incomplete normal modal logics do exist. A natural example of such a system is Japaridze's Polymodal Logic.
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 : formula_27.
T is valid in any reflexive frame formula_7: if
formula_29, then formula_20
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:
formula_31 if and only if "w" "R" "u". Then
formula_32, thus formula_33
by T, which means "w" "R" "w" using the definition of
formula_10. 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 formula_35 generates an incomplete logic, as it
corresponds to the same class of frames as GL (viz. transitive and
converse well-founded frames), but does not prove the GL-tautology formula_36.
Common modal axiom schemata.
The following table lists common modal axioms together with their corresponding classes. The naming of the axioms often varies.
Canonical models.
For any normal modal logic, "L", a Kripke model (called the canonical model) can be constructed that refutes precisely the non-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 "L"-"consistent" if no contradiction can be derived from it using the theorems of "L", and Modus Ponens. A "maximal L-consistent set" (an "L"-"MCS"
for short) is an "L"-consistent set that has no proper "L"-consistent superset.
The canonical model of "L" is a Kripke model
formula_8, where "W" is the set of all "L"-"MCS",
and the relations "R" and formula_10 are as follows:
The canonical model is a model of "L", as every "L"-"MCS" contains
all theorems of "L". By Zorn's lemma, each "L"-consistent set
is contained in an "L"-"MCS", 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
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: Henrik Sahlqvist identified a broad class of formulas (now called
Sahlqvist formulas) such that
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 cut-free
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
formula_45 as the set of its necessity operators
consists of a non-empty set "W" equipped with binary relations
"Ri" for each "i" ∈ "I". The definition of a
satisfaction relation is modified as follows:
A simplified semantics, discovered by Tim Carlson, is often used for
polymodal provability logics. A Carlson model is a structure
formula_48
with a single accessibility relation "R", and subsets
"Di" ⊆ "W" for each modality. Satisfaction is
defined as
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
formula_51, where formula_52 is a preordered Kripke frame, and formula_10 satisfies the following conditions:
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 the finite model property.
Intuitionistic first-order logic.
Let "L" be a first-order language. A Kripke
model of "L" is a triple
formula_68, where
formula_52 is an intuitionistic Kripke frame, "Mw" is a
(classical) "L"-structure for each node "w" ∈ "W", and
the following compatibility conditions hold whenever "u" ≤ "v":
Given an evaluation "e" of variables by elements of "Mw", we
define the satisfaction relation formula_70:
Here "e"("x"→"a") is the evaluation which gives "x" the
value "a", and otherwise agrees with "e".
See a slightly different formalization in.
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. 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 classical model theory, there are methods for
constructing a new Kripke model from other models.
The natural homomorphisms in Kripke semantics are called
p-morphisms (which is short for "pseudo-epimorphism", but the
latter term is rarely used). A p-morphism of Kripke frames
formula_7 and formula_92 is a mapping
formula_93 such that
A p-morphism of Kripke models formula_8 and
formula_95 is a p-morphism of their
underlying frames formula_93, which
satisfies
P-morphisms are a special kind of bisimulations. In general, a
bisimulation between frames formula_7 and
formula_92 is a relation
"B ⊆ W × W’", which satisfies
the following “zig-zag” property:
A bisimulation of models is additionally required to preserve forcing
of atomic formulas:
The key property which follows from this definition is that
bisimulations (hence also p-morphisms) 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 formula_8 and a fixed
node "w"0 ∈ "W", we define a model
formula_95, where "W’" is the
set of all finite sequences
formula_105 such
that "wi R wi+1" for all
"i" < "n", and formula_106 if and only if
formula_107 for a propositional variable
"p". The definition of the accessibility relation "R’"
varies; in the simplest case we put
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 "X"-filtration of a
model formula_8 is a mapping "f" from "W" to a model
formula_95 such that
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
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.
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.
Similar work that predated Kripke's revolutionary semantic breakthroughs: