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 (starting when he was still a teenager). It was originally developed for modal logics, but it was subsequently adapted to
intuitionistic logic and some other non-classical systems.
The discovery of Kripke semantics was a major breakthrough in the
development of non-classical logics, as the model theory of such
logics was virtually nonexistent before Kripke.

Contents

Semantics of modal logic

Basic definitions

Correspondence and completeness

Canonical models

Finite model property

Polymodal logics

Semantics of intuitionistic logic

Intuitionistic first-order logic

Kripke-Joyal semantics

Model constructions

General frame semantics

History and terminology

Notes

References

See also

External links

Semantics of modal logic

A language of propositional modal logic consists of a set of
propositional variables or constants (exactly one of which may be empty), a set of truth functional
connectives (in our case →, and ¬), and the
modal operator $Box$ ("necessarily"). The dual
modal operator $Diamond$ ("possibly") of $Box$ is
defined as $Diamond\; A=\_\{df\}$
egBox
eg A.
See the page on modal logic for more background.

Basic definitions

A 'Kripke frame' or 'modal frame' is a pair <''W'',''R''>, where ''W'' is a
non-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 <''W'',''R'',$Vdash$>, where
<''W'',''R''> is a Kripke frame, and $Vdash$ is a relation between
nodes of ''W'' and modal formulas, such that:

★ $wVdash$
eg A if and only if $w$
otVdash A,

★ $wVdash\; A\; o\; B$ if and only if $w$
otVdash A or $wVdash\; B$,

★ $wVdashBox\; A$ if and only if .
We read ''w'' $Vdash$''A'' as “''w'' satisfies
''A''”, “''A'' is satisfied in ''w''”, or
“''w'' forces ''A''”. The relation $Vdash$ is called the
''satisfaction relation'', ''evaluation'', or ''forcing relation''.
Notice that the satisfaction relation is uniquely determined by its
value on propositional variables.
A formula ''A'' is 'valid' in:

★ a model <''W'',''R'',$Vdash$>, if ''w'' $Vdash$''A'' for all ''w'' ∈''W'',

★ a frame <''W'',''R''>, if it is valid in <''W'',''R'',$Vdash$> for all possible choices of $Vdash$,

★ a class ''C'' of frames or models, if it is valid in every member of ''C''.
We define ''Thm(C)'' as the set of all formulas which 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 investigation of a logic (i.e., a derivation
system) only if the semantical entailment relation faithfully
reflects its syntactical counterpart, the ''consequence'' relation
(''derivability''). It is thus vital to know which modal logics are
sound and complete with respect to a class of Kripke frames, and for them, to
determine which class it 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. Unfortunately,
the converse does not hold in general: there are normal modal logics
which are Kripke incomplete. In practice, this is not a problem, as
most of the modal systems which are actually studied are complete with respect to
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 with respect to its
corresponding class.
As an example, consider the schema ''T'' : $Box$''A'' → ''A''.
''T'' is valid in any reflexive frame <''W'',''R''>: if
''w'' $Vdash\; Box$''A'', then ''w'' $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'' $Vdash$''p'' if and only if ''w'' ''R'' ''u''. Then
''w'' $Vdash\; Box$''p'', thus ''w'' $Vdash$''p''
by ''T'', which means ''w'' ''R'' ''w'' using the definition of
$Vdash$. We see that ''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 that
''L''₁⊆''L''₂ are normal modal logics which
correspond to the same class of frames, such that ''L''₁ does not
prove all theorems of ''L''₂. Then ''L''₁ is
Kripke incomplete. For example, the schema $Box(AequivBox$
A) oBox A generates an incomplete logic, because it
corresponds to the same class of frames as ''GL'' (viz. transitive and
conversely well-founded frames), but it does not prove $Box$
A oBoxBox A.
A list of common modal axioms together with their
corresponding classes is given in the table below. Beware: naming of
the axioms often varies.

'Common modal axiom schemata'

name	axiom	frame condition
''K''	$Box\; (A\; o\; B)\; o(Box\; A\; o\; Box\; B)$	N/A
''T''	$Box\; A\; o\; A$	reflexive
''4''	$Box\; A\; oBoxBox\; A$	transitive
''D''	$Box\; A\; oDiamond\; A$	serial:
''B''	$A\; oBoxDiamond\; A$	symmetric
''5''	$Diamond\; A\; oBoxDiamond\; A$	Euclidean: $w;R;uland\; w;R;vRightarrow\; u;R;v$
''GL''	$Box(Box\; A\; o\; A)\; oBox\; A$	''R'' transitive, ''R''-1 well-founded
''Grz''	$Box(Box(A\; oBox\; A)\; o\; A)\; o\; A$	''R'' reflexive and transitive, ''R''-1−''Id'' well-founded
''H''	$Box(Box\; A\; o\; B)lorBox(Box\; B\; o\; A)$	$w;R;uland\; w;R;vRightarrow\; u;R;vlor\; v;R;u$
''M''	$BoxDiamond\; A\; oDiamondBox\; A$	(a complicated second-order property)
''G''	$DiamondBox\; A\; oBoxDiamond\; A$	$w;R;uland\; w;R;vRightarrowexists\; x,(u;R;xland\; v;R;x)$

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,
''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'', we can construct a Kripke model
(called the 'canonical model'), which validates the theorems of
''L'', and only them, 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 them, the axioms of ''L'',
and Modus Ponens. A ''maximal L-consistent set'' (an ''L''-''MCS''
for short) is an ''L''-consistent set which has no proper
''L''-consistent superset.
The 'canonical model' of ''L'' is a Kripke model
<''W'',''R'',$Vdash$>, where ''W'' is the set of all ''L''-''MCS'',
and the relations ''R'' and $Vdash$ are as follows:
: $X;R;Y$ if and only if for every formula $A$, if $Box\; Ain\; X$ then $Ain\; Y$,
: $XVdash\; A$ if and only if $Ain\; X$.
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. For
example, 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''.
Clearly, 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. Nevertheless, we know a nice sufficient condition: H.
Sahlqvist has 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 first-order definable,

★ there is an algorithm which computes the corresponding frame condition to a given Sahlqvist formula.
This is a very powerful criterion; for example, all axioms
listed above as canonical are in fact (equivalent to) Sahlqvist formulas.

Finite model property

A logic has the 'finite model property' (FMP) if it is complete
wrt a class of finite frames. One of the main applications 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 wrt 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.

Polymodal logics

Kripke semantics has a straightforward generalization to logics with
more than one modality. A Kripke frame for a language with
$\{Box\_i;,iin\; I\}$ as the set of its necessity operators
consists of a non-empty set ''W'' equipped with binary relations
''R_i'' for each ''i'' ∈''I''. The definition of a
satisfaction relation is modified as follows:
: $wVdashBox\_i\; A$ if and only if .
A simplified semantics, discovered by Tim Carlson, is often used for
polymodal provability logics. A 'Carlson model' is a structure
<''W'',''R'',{''D_i''}_{''i''∈''I''},⊩>
with a single accessibility relation ''R'', and subsets
''D_i'' ⊆ ''W'' for each modality. Satisfaction is
defined as
: $wVdashBox\_i\; A$ if and only if .
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
<''W'',≤,$Vdash$>, where <''W'',≤> is a partially ordered Kripke frame, and $Vdash$ satisfies the following conditions:

★ if ''p'' is a propositional variable, ''w'' ≤ ''u'', and ''w'' $Vdash$''p'', then ''u'' $Vdash$''p'' (''persistency'' condition),

★ ''w'' $Vdash$''A'' ∧ ''B'' if and only if ''w'' $Vdash$''A'' and ''w'' $Vdash$''B'',

★ ''w'' $Vdash$''A'' ∨ ''B'' if and only if ''w'' $Vdash$''A'' or ''w'' $Vdash$''B'',

★ ''w'' $Vdash$''A'' → ''B'' if and only if for all ''u'' ≥ ''w'', ''u'' $Vdash$''A'' implies ''u'' $Vdash$''B'',

★ not ''w'' $Vdash$⊥.
Intuitionistic logic is sound and complete with respect to its Kripke
semantics, and it has FMP.

Intuitionistic first-order logic

Let ''L'' be a first-order language. A Kripke
model of ''L'' is a triple
<''W'',≤,{''M_w''}_{''w''∈''W''}>, where
<''W'',≤> is an intuitionistic Kripke frame, ''M_w'' is a
(classical) ''L''-structure 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 ''n''-ary predicate ''P'' and elements ''a''₁,...,''a_n'' ∈''M_u'': if ''P''(''a''₁,...,''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'' $Vdash$''A''[''e'']:

★ ''w'' $Vdash$''P''(''t''₁,...,''t_n'')[''e''] if and only if ''P''(''t''₁[''e''],...,''t_n''[''e'']) holds in ''M_w'',

★ ''w'' $Vdash$(''A'' ∧ ''B'')[''e''] if and only if ''w'' $Vdash$''A''[''e''] and ''w'' $Vdash$''B''[''e''],

★ ''w'' $Vdash$(''A'' ∨ ''B'')[''e''] if and only if ''w'' $Vdash$''A''[''e''] or ''w'' $Vdash$''B''[''e''],

★ ''w'' $Vdash$(''A'' → ''B'')[''e''] if and only if for all ''u'' ≥ ''w'', ''u'' $Vdash$''A''[''e''] implies ''u'' $Vdash$''B''[''e''],

★ not ''w'' $Vdash$⊥[''e''],

★ ''w'' $Vdash$(∃''x'' ''A'')[''e''] if and only if there exists an ''a'' ∈''M_w'' such that ''w'' $Vdash$''A''[''e''(''x''→''a'')],

★ ''w'' $Vdash$(∀''x'' ''A'')[''e''] if and only if for every ''u'' ≥ ''w'' and every ''a'' ∈''M_u'', ''u'' $Vdash$''A''[''e''(''x''→''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 quite 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'. Since this development was the work of a number of people, and was more in the nature of a conceptual insight than a theorem, it is not so easy to attribute credit. 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
'p-morphisms' (which is short for ''pseudo-epimorphism'', but the
latter term is rarely used). A p-morphism of Kripke frames
<''W'',''R''> and <''W’'',''R’''> is a mapping
''f'':''W'' → ''W’'' 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 p-morphism of Kripke models <''W'',''R'',$Vdash$> and
<''W’'',''R’'',$Vdash$’> is a p-morphism of their
underlying frames ''f'':''W'' → ''W’'', which
satisfies
: ''w'' $Vdash$''p'' if and only if ''f(w)'' $Vdash$’''p'', for any propositional variable ''p''.
P-morphisms are a special kind of bisimulations. In general, a
'bisimulation' between frames <''W'',''R''> and
<''W’'',''R’''> is a relation
''B ⊆ W × W’'', which satisfies
the following “zig-zag” property:

★ if ''u B u’'' and ''u R v'', there exists ''v’'' ∈ ''W’'' such that ''v B v’'',

★ if ''u B u’'' and ''u’ R’ v’'', there exists ''v'' ∈ ''W'' such that ''v B v’''.
A bisimulation of models is additionally required to preserve forcing
of atomic formulas:
: if ''w B w’'', then ''w'' $Vdash$''p'' if and only if ''w’'' $Vdash$’''p'', for any propositional variable ''p''.
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 <''W'',''R'',$Vdash$> and a fixed
node ''w''₀ ∈ ''W'', we define a model
<''W’'',''R’'',$Vdash$’>, where ''W’'' is the
set of all finite sequences
''s''=<''w''₀,''w''₁,...,''w_n''> such
that ''w_i'' ''R'' ''w_i+1'' for all
''i''<''n'', and ''s'' $Vdash$''p'' if and only if
''w_n'' $Vdash$''p'' for a propositional variable
''p''. The definition of the accessibility relation ''R’''
varies; in the simplest case we put
: <''w''₀,''w''₁,...,''w_n''> ''R’'' <''w''₀,''w''₁,...,''w_n'',''w_n+1''>,
but many applications need the reflexive and/or transitive closure of
this relation, or similar modifications.
'Filtration' is a variant of a p-morphism. Let ''X'' be a set of
formulas closed under taking subformulas. An ''X''-filtration of a
model <''W'',''R'',$Vdash$> is a mapping ''f'' from ''W'' to a model
<''W’'',''R’'',$Vdash$’> 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'' $Vdash\; Box$''A'', where $Box$''A'' ∈''X'', then ''v'' $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'' $Vdash$''A'' if and only if ''v'' $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.

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 anti-model-theoretic.

★ 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 Lewis-style 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 ground-breaking. 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

1. Intuitionistic Logic. Written by Joan Moschovakis. Published in Stanford Encyclopedia of Philosophy.

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.

★ Goldblatt, Robert, 2003, "Mathematical Modal Logic: a View of its Evolution," ''Journal of Applied Logic 1'': 309-92.

★ 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''. Springer-Verlag.

★ van Dalen, Dirk, 1986, "Intuitionistic Logic" in ''The Handbook of Philosophical Logic,'' vol. 3. Reidel: 225--339.

See also

★ Modal logic

★ Normal modal logic

★ Kripke structure

★ Two dimensionalism

External links

★ The Stanford Encyclopedia of Philosophy: "Modal Logic" -- by James Garson.

★ Intuitionistic Logic. Written by 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."