|
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 late 1950's and early 1960's by Saul Kripke. 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. Semantics of modal logic For our purposes, the language of modal logic consists of propositional variables, the reader's favorite complete set of Boolean connectives (such as , or ), and the modal operator (“necessity”). The dual modal operator (“possibility”) is defined as an abbreviation: . 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,>, where <W,R> is a Kripke frame, and is a relation between nodes of W and modal formulas, such that: A”, “A is satisfied in w”, or “w forces A”. The relation 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: 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 A → A. T is valid in any reflexive frame <W,R>: if w A, then w 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 p if and only if w R u. Then w p, thus w p by T, which means w R w using the definition of . 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 L1⊆L2 are normal modal logics which correspond to the same class of frames, such that L1 does not prove all theorems of L2. Then L1 is Kripke incomplete. For example, the schema 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 . A list of common modal axioms together with their corresponding classes is given in the table below. Beware: naming of the axioms often varies. 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. 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,>, 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. 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 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 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 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 <W,R,i∈I,⊩> 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 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 partially ordered Kripke frame, and satisfies the following conditions: 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,≤,w∈W>, where <W,≤> 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: define the satisfaction relation w A''e'': value a, and otherwise agrees with e. 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 <W’,R’,’> is a p-morphism of their underlying frames f:W → W’, which satisfies w p if and only if 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: of atomic formulas: if w B w’, then w p if and only if 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 w0 ∈ W, we define a model <W’,R’,’>, where W’ is the set of all finite sequences s=<w0,w1,...,wn> such that wi R wi+1 for all i<n, and s p if and only if wn p for a propositional variable p. The definition of the accessibility relation R’ varies; in the simplest case we put <w0,w1,...,wn> R’ <w0,w1,...,wn,wn+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 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 A if and only if v 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: 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. See also | |||||||
|
--> | ||||||||
 |
|
| |