Kripke semantics#Common modal axiom schemata

{{Main| 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 $\backslash to$ and $\backslash neg$), and the modal operator $\backslash Box$ ("necessarily"). The modal operator $\backslash Diamond$ ("possibly") is (classically) the dual of $\backslash Box$ and may be defined in terms of necessity like so: $\backslash Diamond\; A\; :=\; \backslash neg\backslash Box\backslash neg\; A$ ("possibly A" is defined as equivalent to "not necessarily not A").{{sfn|Shoham|Leyton-Brown|2008}}

A Kripke frame or modal frame is a pair $\backslash langle\; W,R\backslash rangle$, 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.{{sfn|Gasquet|Herzig|Said|Schwarzentruber|2013|pages=14–16}}

A Kripke model is a triple $\backslash langle\; W,R,\backslash Vdash\backslash rangle$,Note that the notion of 'model' in the Kripke semantics of modal logic differs from the notion of 'model' in classical non-modal logics: In classical logics we say that some formula F has a 'model' if there exists some 'interpretation' of the variables of F which makes the formula F true; this specific interpretation is then a model of the formula F. In the Kripke semantics of modal logic, by contrast, a 'model' is not a specific 'something' that makes a specific modal formula true; in Kripke semantics a 'model' must rather be understood as a larger universe of discourse within which any modal formulae can be meaningfully 'understood'. Thus: whereas the notion of 'has a model' in classical non-modal logic refers to some individual formula within that logic, the notion of 'has a model' in modal logic refers to the logic itself as a whole (i.e.: the entire system of its axioms and deduction rules). 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 for all w ∈ W and modal formulas A and B:

• $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\; \backslash in\; 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).

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).{{sfn|Giaquinto|2002}} 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 : $\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₁ ⊆ L₂ are normal modal logics that correspond to the same class of frames, but L₁ does not prove all theorems of L₂. Then L₁ is Kripke incomplete. For example, the schema $\backslash Box(A\backslash leftrightarrow\backslash Box$

A)\to\Box A 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 $\backslash Box$

A\to\Box\Box A.

The following table lists common modal axioms together with their corresponding classes. The naming of the axioms often varies; Here, axiom K is named after Saul Kripke; axiom T is named after the truth axiom in epistemic logic; axiom D is named after deontic logic; axiom B is named after L. E. J. Brouwer; and axioms 4 and 5 are named based on C. I. Lewis's numbering of symbolic logic systems.

Axiom K can also be rewritten as $\backslash Box\; [(A\backslash to\; B)\backslash land\; A]\backslash to\; \backslash Box\; B$, which logically establishes modus ponens as a rule of inference in every possible world.

Note that for axiom D, $\backslash Diamond\; A$ implicitly implies $\backslash Diamond\backslash top$, which means that for every possible world in the model, there is always at least one possible world accessible from it (which could be itself). This implicit implication $\backslash Diamond\; A\; \backslash rightarrow\; \backslash Diamond\backslash top$ is similar to the implicit implication by existential quantifier on the range of quantification.

{{:Normal modal logic}}

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

$\backslash langle\; W,R,\backslash Vdash\backslash rangle$, where W is the set of all L-MCS,

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 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

• X is valid in every frame that satisfies P,
• for any normal modal logic L that 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: Henrik 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 first-order definable,
• there is an algorithm that 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.

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.

{{See also|Multimodal logic}}

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 non-empty 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.

Kripke semantics for intuitionistic logic follows the same principles as the semantics of modal logic, but it uses a different definition of satisfaction.{{sfn|Troelstra|van Dalen|1988|loc=5. Kripke semantics|pages=75-87}}

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:{{sfn|Simpson|1994|page=20|loc=2.2 The semantics of intuitionistic logic}}

• if p is a propositional variable, $w\backslash le\; u$, and $w\backslash Vdash\; p$, then $u\backslash Vdash\; p$ (persistency condition (cf. monotonicity)),
• $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 the finite model property.

Let L be a first-order 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) 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\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.{{refn|See a slightly different formalization in {{harvtxt|Moschovakis|2022}}}}

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.{{sfn|Goldblatt|2006b}} 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.

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

$\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 p-morphism 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 p-morphism 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.

P-morphisms 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 “zig-zag” 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 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 $\backslash langle\; W,R,\backslash Vdash\backslash rangle$ and a fixed

node w₀ ∈ 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 one can use to prove FMP for many logics. Let X be a set of

formulas closed under taking subformulas. An X-filtration 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.

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.

{{main|Kripke structure|state transition system|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)

{{Unreferenced section|date=October 2009}}

Similar work that predated Kripke's revolutionary semantic breakthroughs:{{sfn|Stokhof|2008|loc=See the last two paragraphs in Section 3 Quasi-historical Interlude: the Road from Vienna to Los Angeles.}}

• 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.

• Alexandrov topology
• Normal modal logic
• Two-dimensionalism
• Muddy Children Puzzle

• {{cite book |first1=P. |last1=Blackburn |author2-link=Maarten de Rijke |first2=M. |last2=de Rijke |first3=Yde |last3=Venema |title=Modal Logic |url=https://books.google.com/books?id=-n7uBgAAQBAJ |date=2002 |publisher=Cambridge University Press |isbn=978-1-316-10195-7}}
• {{cite book |last1=Bull |first1=Robert A. |first2=K. |last2=Segerberg |chapter=Basic Modal Logic |editor-first=D.M. |editor-last=Gabbay |editor2-first=F. |editor2-last=Guenthner |series=Handbook of Philosophical Logic |volume=2 |title=Extensions of Classical Logic |chapter-url=https://books.google.com/books?id=IoTtCAAAQBAJ&pg=PA1 |date=2012 |publisher=Springer |isbn=978-94-009-6259-0 |pages=1–88 |orig-year=1984}}
• {{cite book |first1=A. |last1=Chagrov |first2=M. |last2=Zakharyaschev |title=Modal Logic |url=https://books.google.com/books?id=dhgi5NF4RtcC |year=1997 |publisher=Clarendon Press |isbn=978-0-19-853779-3}}
• {{cite book |first1=M.J. |last1=Cresswell |author1-link=Max Cresswell|first2=G.E. |last2=Hughes |author2-link=George Edward Hughes|title=A New Introduction to Modal Logic |url=https://books.google.com/books?id=TkwrBgAAQBAJ |year=2012 |orig-year=1996 |publisher=Routledge |isbn=978-1-134-80028-5}}
• {{cite book |last=Van Dalen |first=Dirk |author-link=Dirk van Dalen|orig-year=1986 |chapter=Intuitionistic Logic |editor-first=Dov M. |editor-last=Gabbay |editor2-first=Franz |editor2-last=Guenthner |series=Handbook of Philosophical Logic |title=Alternatives to Classical Logic |chapter-url=https://books.google.com/books?id=NwDwCAAAQBAJ&pg=PA225 |year=2013 |publisher=Springer |isbn=978-94-009-5203-4 |pages=225–339 |volume=3}}
• {{cite book |author-link=Michael Dummett |first=Michael A. E. |last=Dummett |title=Elements of Intuitionism |url=https://books.google.com/books?id=JVFzknbGBVAC |year=2000 |publisher=Clarendon Press |isbn=978-0-19-850524-2 |edition=2nd}}
• {{cite book |first=Melvin |last=Fitting |authorlink = Melvin Fitting|title=Intuitionistic Logic, Model Theory and Forcing |url=https://archive.org/details/intuitionisticlo0000fitt |url-access=registration |year=1969 |publisher=North-Holland |isbn=978-0-444-53418-7}}
• {{cite book|last1=Gasquet|first1=Olivier|last2=Herzig|first2=Andreas|last3=Said|first3=Bilal|last4=Schwarzentruber|first4=François|title=Kripke's Worlds: An Introduction to Modal Logics via Tableaux|date=2013|publisher=Springer |isbn=978-3764385033|pages=XV, 198|url=https://books.google.com/books?id=qFS-BAAAQBAJ|access-date=24 December 2014}}
• {{cite book|last=Giaquinto|first=Marcus|title=The Search for Certainty : A Philosophical Account of Foundations of Mathematics: A Philosophical Account of Foundations of Mathematics|date=2002|publisher=Oxford University Press|isbn=019875244X|page=256|url=https://books.google.com/books?id=gyNbrpYXzxoC|access-date=24 December 2014}}
• {{cite book |author-link=Robert Goldblatt |first=Robert |last=Goldblatt |chapter=Mathematical Modal Logic: a View of its Evolution |chapter-url=http://www.msor.vuw.ac.nz/~rob/papers/modalhist.pdf |format=PDF |editor-first=Dov M. |editor-last=Gabbay |editor2-first=John |editor2-last=Woods |title=Logic and the Modalities in the Twentieth Century |url=https://books.google.com/books?id=gpwZYXsomEsC&pg=PP1 |date=2006a|publisher=Elsevier |isbn=978-0-08-046303-2 |pages=1–98 |series=Handbook of the History of Logic |volume=7}}
• {{cite book |author-link=Robert Goldblatt |first=Robert |last=Goldblatt |chapter=A Kripke-Joyal Semantics for Noncommutative Logic in Quantales |chapter-url=http://homepages.ecs.vuw.ac.nz/~rob/papers/aiml11printed.pdf |editor-first=G.|editor-last=Governatori|editor2-first=I. |editor2-last=Hodkinson|editor3-first=Y. |editor3-last=Venema |title=Advances in Modal Logic |publisher=College Publications |location=London |year=2006b|isbn=1904987206 |pages=209–225 |volume=6}}
• {{cite book |author-link=Saunders Mac Lane |author2-link=Ieke Moerdijk |first1=Saunders |last1=Mac Lane |first2=Ieke |last2=Moerdijk |title=Sheaves in Geometry and Logic: A First Introduction to Topos Theory |url=https://books.google.com/books?id=LZWLBAAAQBAJ |year=2012 |orig-year=1991 |publisher=Springer |isbn=978-1-4612-0927-0 }}
• {{cite book |last1=Shoham |first1=Yoav |first2=Kevin |last2=Leyton-Brown |title=Multiagent Systems: Algorithmic, Game-Theoretic, and Logical Foundations |date=2008 |publisher=Cambridge University Press |isbn=978-0521899437 |page=397|url=https://books.google.com/books?id=bMR_qScakukC}}
• {{cite thesis|last=Simpson|first=Alex K.|date=1994|title=The Proof Theory and Semantics of Intuitionistic Modal Logic|url=https://era.ed.ac.uk/handle/1842/407|hdl=1842/407|publisher=Edinburgh Research Archive (ERA)}}
• {{cite book|last=Stokhof|first=Martin|year=2008|editor1-last=Zamuner|editor1-first=Edoardo|editor2-last=Levy|editor2-first=David K.|title=Wittgenstein's Enduring Arguments|publisher=Routledge|location=London|chapter=The architecture of meaning: Wittgenstein’s Tractatus and formal semantics|pages=211–244|isbn=9781134107070|chapter-url=https://books.google.com/books?id=MUp8AgAAQBAJ&pg=PA211}}
• {{cite book | last1 = Troelstra | first1 = A. S. | author-link1 = Anne Sjerp Troelstra | last2 = van Dalen | first2 = D. | author-link2 = Dirk van Dalen | title = Constructivism in Mathematics: An Introduction, Volume 1 | url = https://archive.org/details/StudiesInLogicAndTheFoundationsOfMathematics121AnneS.TroelstraDirkVanDalenConstr | series = Studies in Logic and the Foundations of Mathematics | language = en | volume = 121 | year = 1988 | publisher = North-Holland | location = Amsterdam | isbn = 9780444702661 }}

{{Commons category|Kripke models}}

• {{cite web|first=John P.|last=Burgess|title=Kripke Models|url=http://www.princeton.edu/~jburgess/Kripke1.doc|url-status=dead|archive-url=https://web.archive.org/web/20041020014707/http://www.princeton.edu/~jburgess/Kripke1.doc|archive-date=2004-10-20}}
• {{cite book |first1=V. |last1=Detlovs |last2=Podnieks |first2=K. |chapter=4.4 Constructive Propositional Logic — Kripke Semantics |chapter-url=http://www.ltn.lv/~podnieks/mlog/ml4a.htm#s44 |title=Introduction to Mathematical Logic |publisher=University of Latvia |url=https://dspace.lu.lv/dspace/handle/7/34986}} N.B: Constructive = intuitionistic.
• {{cite SEP|last=Garson|first=James|date=23 January 2023|title=Modal Logic|url-id=logic-modal}}
• {{springer|title=Kripke models|id=p/k055850}}
• {{cite SEP|last=Moschovakis|first=Joan|date=16 December 2022|title=Intuitionistic Logic|url-id=logic-intuitionistic}}

{{DEFAULTSORT:Kripke Semantics}}

Category:Modal logic

Category:Model theory

Category:Mathematical logic

Category:Philosophical logic

Category:Sheaf theory

Category:Non-classical logic

de:Kripke-Semantik