1.3 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. Canonical Kripke models play a similar rôle as the Lindenbaum-Tarski algebra construction in algebraic semantics.

A set X of formulas is L-consistent, if there does not exist a proof of contradiction using formulas from X, theorems of L, and Modus Ponens. A maximal L-consistent set (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,⊩>, where W is the set of all L-MCS, and the relations R and ⊩ are as follows:

iff for every formula A, if then ,

iff .

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, 3, 2 (and thus any combination of them) are canonical. GL and Grz are not canonical, because they are not compact. The axiom 1 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.

1.4 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 algebra s, 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.

1.5 Polymodal logics

Kripke semantics has a straightforward generalization to logics with more than one modality. A Kripke frame for a language with

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:

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

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.

2 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,≤,⊩>, where <W,≤> is a

transitive and reflexive Kripke frame (i.e., the accessibility relation is a preorder), and ⊩ satisfies the following conditions:

• if p is a propositional variable, w ≤ u, and w ⊩p, then u ⊩p (persistency condition),
• w ⊩A ∧ B if and only if w ⊩A and w ⊩B,
• w ⊩A ∨ B if and only if w ⊩A or w ⊩B,
• w ⊩A → B if and only if for all u ≥ w, u ⊩A implies u ⊩B,
• not w ⊩⊥.

Intuitionistic logic is sound and complete with respect to its Kripke semantics, and it has FMP.

2.1 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 ⊩A[e]:

• w ⊩P(t₁,...,t_n)[e] if and only if P(t₁[e],...,t_n[e]) holds in M_w,
• w ⊩(A ∧ B)[e] if and only if w ⊩A[e] and w ⊩B[e],
• w ⊩(A ∨ B)[e] if and only if w ⊩A[e] or w ⊩B[e],
• w ⊩(A → B)[e] if and only if for all u ≥ w, u ⊩A[e] implies u ⊩B[e],
• not w ⊩⊥[e],
• w ⊩(∃x A)[e] if and only if there exists an a ∈M_w such that w ⊩A[e(x→a)],
• w ⊩(∀x A)[e] if and only if for every u ≥ w and every a ∈M_u, u ⊩A[e(x→a)].

Here e(x→a) is the evaluation which gives x the value a, and otherwise agrees with e.

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

3 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 f(v)=v’.

A p-morphism of Kripke models <W,R,⊩> and <W’,R’,⊩’> is a p-morphism of their underlying frames f:W → W’, which satisfies

w ⊩p iff f(w) ⊩’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 ⊩p iff w’ ⊩’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,⊩> and a fixed node w₀ ∈ W, we define a model <W’,R’,⊩’>, 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 ⊩p iff w_n ⊩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,⊩> is a mapping f from W to a model <W’,R’,⊩’> 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 ⊩, where ∈X, then v ⊩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 iff for all A ∈X, u ⊩A iff v ⊩A.

As in the case of unravelling, the definition of the accessibility relation on the quotient varies.

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

• 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ónsson and Tarski give a presentation of an approach to semantics that is still influential in modern research on modal logic, namely the algebraic approach, which contains many of the key ideas of Kripke semantics. They apply the ideas to the semantics of intuitionistic logic, but fail to see the relationship to modal logic;
• 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, and so did not publish until after Kripke's papers had created a sensation in the logic community;
• Evert 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.

5 References

• Modal Logic. P. Blackburn, M. de Rijke, Y. Venema. Cambridge University Press, 2001.
• Basic Modal Logic. R. A. Bull and K. Segerberg. In The Handbook of Philosophical Logic, volume 2, pages 1--88. Kluwer, 1984.
• A New Introduction to Modal Logic. G. E. Hughes, M. J. Cresswell. Routledge, 1996.
• Modal Logic. A. Chagrov, M. Zakharyaschev. Oxford University Press, 1997.
• Modal Logic. J. Garson. In E. N. Zalta, editor, The Stanford Encyclopaedia of Philosophy
• Mathematical Modal Logic: a View of its Evolution. Robert Goldblatt. In Journal of Applied Logic, vol. 1(5-6):309-392, 2003.
• Intuitionistic Logic. D. van Dalen. In The Handbook of Philosophical Logic, volume 3, pages 225--339. Reidel, 1986.
• Elements of Intuitionism. M. Dummett. Clarendon Press, 1977.
• Intuitionistic Logic, Model Theory and Forcing. M. Fitting. North-Holland, 1969.
• Sheaves in Geometry and Logic. S. Mac Lane and I. Moerdijk. Springer-Verlag, 1991.

6 External links

• Introduction to Mathematical Logic by Drs. Detlovs and Podnieks. Chapter 4, Section 4: "Constructive Propositional Logic — Kripke Semantics".
• Kripke Models, a Word document by John P. Burgess.

Model theory Mathematical logic Sheaf theory

<Hide>