This article includes a list of general references, but it lacks sufficient corresponding inline citations. Please help to improve this article by introducing more precise citations. (April 2013) (Learn how and when to remove this message)

Kripke semantics (also known as relational semantics or frame semantics, and often confused with possible world semantics)[1] 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

Main article: 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 and ), and the modal operator ("necessarily"). The modal operator ("possibly") is (classically) the dual of and may be defined in terms of necessity like so: ("possibly A" is defined as equivalent to "not necessarily not A").[2]

Basic definitions

A Kripke frame or modal frame is a pair , 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.[3]

A Kripke model is a triple ,[4] where is a Kripke frame, and is a relation between nodes of W and modal formulas, such that for all w ∈ W and modal formulas A and B:

We read as “w satisfies A”, “A is satisfied in w”, or “w forces A”. The relation 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).[5] 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 : . T is valid in any reflexive frame : if , then 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: if and only if w R u. Then , thus by T, which means w R w using the definition of . 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 L1 ⊆ L2 are normal modal logics that correspond to the same class of frames, but L1 does not prove all theorems of L2. Then L1 is Kripke incomplete. For example, the schema 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 .

Common modal axiom schemata

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.

Name Axiom Frame condition
K holds true for any frames
T reflexive:
- dense:
4 transitive:
D or or serial:
B or symmetric :
5 Euclidean:
GL R transitive, R−1 well-founded
Grz[6] R reflexive and transitive, R−1−Id well-founded
H
M (a complicated second-order property)
G convergent:
- discrete:
- partial function:
- function: ( is the uniqueness quantification)
- or empty:

Axiom K can also be rewritten as , which logically establishes modus ponens as a rule of inference in every possible world.

Note that for axiom D, implicitly implies , 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 is similar to the implicit implication by existential quantifier on the range of quantification.

Common modal systems

The following table lists several common normal modal systems. Frame conditions for some of the systems were simplified: the logics are sound and complete with respect to the frame classes given in the table, but they may correspond to a larger class of frames.

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, K4W 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 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 , where W is the set of all L-MCS, and the relations R and are as follows:

if and only if for every formula , if then ,
if and only if .

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

See also: Multimodal logic

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 Ri 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 with a single accessibility relation R, and subsets Di ⊆ 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.

Semantics of intuitionistic logic

Kripke semantics for 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 , where is a preordered Kripke frame, and satisfies the following conditions:[7]

The negation of A, ¬A, could be defined as an abbreviation for A → ⊥. If for all u such that wu, 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 , where 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 :

Here e(xa) is the evaluation which gives x the value a, and otherwise agrees with e.[8]

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.[9] 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 and is a mapping such that

A p-morphism of Kripke models and is a p-morphism of their underlying frames , which satisfies

if and only if , for any propositional variable p.

P-morphisms are a special kind of bisimulations. In general, a bisimulation between frames and 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:

if w B w’, then if and only if , 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 and a fixed node w0 ∈ W, we define a model , where W’ is the set of all finite sequences such that wi R wi+1 for all i < n, and if and only if 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 is a mapping f from W to a model 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

u ≡X v if and only if for all A ∈ X, if and only if .

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

This section does not cite any sources. Please help improve this section by adding citations to reliable sources. Unsourced material may be challenged and removed. (October 2009) (Learn how and when to remove this message)

Similar work that predated Kripke's revolutionary semantic breakthroughs:[10]

See also

Notes

  1. ^ Possible world semantics is a broader term encompassing various approaches, including Kripke semantics. It generally refers to the idea of analyzing modal statements by considering alternative possible worlds where different propositions are true or false. While Kripke semantics is a specific type of possible world semantics, there are other ways to model possible worlds and their relationships. Kripke semantics is a specific form of possible world semantics that employs relational structures to represent the relationships between possible worlds and propositions in modal logic.[citation needed]
  2. ^ Shoham & Leyton-Brown 2008.
  3. ^ Gasquet et al. 2013, pp. 14–16.
  4. ^ 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).
  5. ^ Giaquinto 2002.
  6. ^ After Andrzej Grzegorczyk.
  7. ^ Simpson 1994, p. 20, 2.2 The semantics of intuitionistic logic.
  8. ^ See a slightly different formalization in Moschovakis (2022)
  9. ^ Goldblatt 2006b.
  10. ^ Stokhof 2008, See the last two paragraphs in Section 3 Quasi-historical Interlude: the Road from Vienna to Los Angeles..

References