Kripke semantics - Citizendia

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, beginning when he was a teenager. Semantics is the study of meaning in communication The word derives from Greek σημαντικός ( semantikos) "significant" from Saul Aaron Kripke (born on November 13, 1940 in Bay Shore New York) is an American philosopher and Logician now Emeritus It was first made for modal logics, and later adapted to intuitionistic logic and other non-classical systems. A modal logic is any system of formal logic that attempts to deal with modalities. Intuitionistic logic, or constructivist logic, is the Symbolic logic system originally developed by Arend Heyting to provide a formal basis for Brouwer The discovery of Kripke semantics was a breakthrough in the making of non-classical logics, because the model theory of such logics was nonexistent before Kripke. In Mathematics, model theory is the study of (classes of mathematical structures such as groups, Fields graphs or even models

1 Semantics of modal logic
2 Semantics of intuitionistic logic
- 2.1 Intuitionistic first-order logic
- 2.2 Kripke-Joyal semantics
3 Model constructions
4 General frame semantics
5 History and terminology
6 Notes
7 References
8 See also
9 External links

Semantics of 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 $\Box$ ("necessarily"). In Mathematical logic, a propositional variable (also called a sentential variable or sentential letter) is a Variable which can either be Table of logic symbolsIn Logic, two sentences (either in a formal language or a natural language may be joined by means of a logical connective to form a compound sentence The dual modal operator $\Diamond$ ("possibly") of $\Box$ is defined as $\Diamond A=_{df}\neg\Box\neg A$ . See the page on modal logic for more background. A modal logic is any system of formal logic that attempts to deal with modalities.

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. In Mathematics, a binary relation (or a dyadic or 2-place relation) is an arbitrary association of elements within a set or with elements of Elements of W are called nodes or worlds, and R is known as the accessibility relation. An accessibility relation is a binary relation R\\! between Possible worlds which has very powerful uses in both the formal/theoretical aspects of Modal logic

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:

$w\Vdash\neg A$ if and only if $w\not\Vdash A$ ,
$w\Vdash A\to B$ if and only if $w\not\Vdash A$ or $w\Vdash B$ ,
$w\Vdash\Box A$ if and only if $\forall u\,(w\; R\; u \to u\Vdash A)$ .

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. In the mathematical discipline of Set theory, forcing is a technique invented by Paul Cohen, for proving Consistency and independence results 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) 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 semantical entailment relation reflects its syntactical counterpart, the consequence relation (derivability). In Logic, entailment (or Logical implication) is a relation between sentences of a formal language such that if A is a set of sentences and B is a sentence It is 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). In Logic, a normal Modal logic is a set L of modal formulas such that L contains All propositional tautologies; However, the converse does not hold in general. There are Kripke incomplete normal modal logics, which is not a problem, because most of the modal systems studied are complete of 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 of its corresponding class.

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. In Set theory, a Binary relation can have among other properties reflexivity or irreflexivity. 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$ . 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 $\Box(A\equiv\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 $\Box A\to\Box\Box A$ .

The table below is a list of common modal axioms together with their corresponding classes. The naming of the axioms often varies.

**Common modal axiom schemata**
name	axiom	frame condition
K	$\Box (A\to B)\to(\Box A\to \Box B)$	N/A
T	$\Box A\to A$	reflexive : $\forall w\ (w\;R\;w)$
4	$\Box A\to\Box\Box A$	transitive : $\forall w\, \forall v\,\forall u ((w\;R\;v \wedge v\;R\;u) \Rightarrow w\;R\;u)$
D	$\Box A\to\Diamond A$	serial: $\forall w\,\exists v\,(w\;R\;v)$
B	$A\to\Box\Diamond A$	symmetric : $\forall w\, \forall v\, (w\;R\;v \Rightarrow v\;R\;w)$
5	$\Diamond A\to\Box\Diamond A$	Euclidean: $w\;R\;u\land w\;R\;v\Rightarrow u\;R\;v$
GL	$\Box(\Box A\to A)\to\Box A$	R transitive, R^-1 well-founded
Grz	$\Box(\Box(A\to\Box A)\to A)\to A$	R reflexive and transitive, R^-1−Id well-founded
H	$\Box(\Box A\to B)\lor\Box(\Box B\to A)$	$w\;R\;u\land w\;R\;v\Rightarrow u\;R\;v\lor v\;R\;u$
M	$\Box\Diamond A\to\Diamond\Box A$	(a complicated second-order property)
G	$\Diamond\Box A\to\Box\Diamond A$	$w\;R\;u\land w\;R\;v\Rightarrow\exists x\,(u\;R\;x\land v\;R\;x)$

Here is a list of several common modal systems. In Set theory, a Binary relation can have among other properties reflexivity or irreflexivity. In Mathematics, a Binary relation R over a set X is transitive if whenever an element a is related to an element b In Mathematics, a Binary relation R over a set X is symmetric if it holds for all a and b in X that In Mathematics, a Binary relation R over a set X is transitive if whenever an element a is related to an element b In Mathematics, a Binary relation, R, is well-founded (or wellfounded) on a class X if and only if every non- empty In Set theory, a Binary relation can have among other properties reflexivity or irreflexivity. In Mathematics, a Binary relation R over a set X is transitive if whenever an element a is related to an element b In Mathematics, a Binary relation, R, is well-founded (or wellfounded) on a class X if and only if every non- empty In Logic and Mathematics second-order logic is an extension of First-order logic, which itself is an extension of Propositional logic. 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. In Set theory, a Binary relation can have among other properties reflexivity or irreflexivity. In Mathematics, a Binary relation R over a set X is transitive if whenever an element a is related to an element b In Mathematics, especially in Order theory, preorders are Binary relations that satisfy certain conditions In Mathematics, an equivalence relation is a Binary relation between two elements of a set which groups them together as being "equivalent" 3	T, 4, H	total preorder
S4. In Mathematics, especially Order theory, a strict weak ordering is a Binary relation S that is a strict partial order 1	T, 4, M	preorder, $\forall w\,\exists u\,(w\;R\;u\land\forall v\,(u\;R\;v\Rightarrow u=v))$
S4. In Mathematics, especially in Order theory, preorders are Binary relations that satisfy certain conditions 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, a Kripke model (called the canonical model) can be constructed, which validates precisely the theorems of L, by an adaptation of the standard technique of using maximal consistent sets as models. In Mathematics, a directed set (or a directed preorder or a filtered set) is a nonempty set A together with a reflexive In Mathematics, especially in Order theory, preorders are Binary relations that satisfy certain conditions Provability logic is a Modal logic, in which the box (or "necessity" operator is interpreted as 'it is provable that' In Mathematics, especially Order theory, a partially ordered set (or poset) formalizes the intuitive concept of an ordering sequencing or arrangement In Mathematics, especially Order theory, a partially ordered set (or poset) formalizes the intuitive concept of an ordering sequencing or arrangement In Mathematics, a Binary relation R over a set X is transitive if whenever an element a is related to an element b In Mathematics, a maximal consistent set is a set of formulae belonging to some Formal language that satisfies the following constraints Canonical Kripke models play a role similar to the Lindenbaum-Tarski algebra construction in algebraic semantics. In Mathematical logic, the Lindenbaum-Tarski algebra A of a logical theory T consists of the Equivalence classes of sentences

A set of formulas is L-consistent if no contradiction can be derived from them using 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 A\in X$ then $A\in Y$ ,

$X\Vdash A$ if and only if $A\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. Zorn's lemma, also known as the Kuratowski-Zorn lemma, is a proposition of Set theory that states Every Partially ordered set in which

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 which satisfies P,
for any normal modal logic L which 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. In Mathematical logic, the compactness theorem states that a (possibly Infinite) set of first-order sentences has a model, Iff every

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. In Computability theory and Computational complexity theory, a decision problem is a question in some Formal system with a yes-or-no answer depending on We know a nice sufficient condition: H. 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 which computes the corresponding frame condition to a given Sahlqvist formula. In Modal logic, Sahlqvist formulae are a certain kind of modal formula with remarkable properties First-order logic (FOL is a formal Deductive system used in mathematics philosophy linguistics and computer science

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 Logic, the term decidable refers to the existence of an Effective method for determining membership in a set of formulas In computability theory Post's theorem, named after Emil Post, describes the connection between the Arithmetical hierarchy and the Turing degrees 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. The cut-elimination theorem is the central result establishing the significance of the Sequent calculus. In Proof theory and Mathematical logic, the sequent calculus is a widely known Proof calculus for First-order logic (and Propositional logic

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. In algebra and Logic, a modal algebra is a structure \langle A\land\lor-01\Box\rangle such that \langle A\land\lor-01\rangle 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 multimodal logic is a Modal logic that has more than one primitive Modal operator. A Kripke frame for a language with $\{\Box_i;\,i\in 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:

$w\Vdash\Box_i A$ if and only if $\forall u\,(w\;R_i\;u\Rightarrow u\Vdash A).$

A simplified semantics, discovered by Tim Carlson, is often used for polymodal provability logics. Provability logic is a Modal logic, in which the box (or "necessity" operator is interpreted as 'it is provable that' 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

$w\Vdash\Box_i A$ if and only if $\forall u\in D_i\,(w\;R\;u\Rightarrow u\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.

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. Intuitionistic logic, or constructivist logic, is the Symbolic logic system originally developed by Arend Heyting to provide a formal basis for Brouwer

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$ ⊥. In Mathematics, especially Order theory, a partially ordered set (or poset) formalizes the intuitive concept of an ordering sequencing or arrangement

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. First-order logic (FOL is a formal Deductive system used in mathematics philosophy linguistics and computer science 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. In Mathematics, a sheaf is a tool for systematically tracking locally defined data attached to the Open sets of a Topological space. In Predicate logic, an existential quantification is the predication of a property or relation to at least one member of the domain In Mathematics, a topos (plural "topoi" or "toposes" is a type of category that behaves like the category of sheaves of sets 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. In Mathematics, model theory is the study of (classes of mathematical structures such as groups, Fields graphs or even models

The natural homomorphisms in Kripke semantics are called p-morphisms (which is short for pseudo-epimorphism, but the latter term is rarely used). In Abstract algebra, a homomorphism is a structure-preserving map between two Algebraic structures (such as groups rings or Vector 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 Theoretical computer science a bisimulation is a Binary relation between State transition systems associating systems which behave in the same way in 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’ 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 $\Vdash$ p if and only if w’ $\Vdash$ ’p, for any propositional variable p. In Mathematical logic, an atomic formula (also known simply as an atom) is a formula with no deeper Propositional structure that is a formula

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. In Graph theory, a tree is a graph in which any two vertices are connected by exactly one path. 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. In Mathematics, a function f is said to be surjective or onto, if its values span its whole Codomain; that is for every

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. In Mathematics, given a set X and an Equivalence relation ~ on X, the equivalence class of an element a in X

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. In Logic, general frames (or simply frames) are Kripke frames with an additional structure which are used to model modal and intermediate

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. Rudolf Carnap ( May 18, 1891 &ndash September 14, 1970) was an influential German -born philosopher who was active in 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. Alfred Tarski ( January 14, 1901, Warsaw, Russian ruled Poland – October 26, 1983, Berkeley California Bjarni Jónsson and Tarski established the representability of Boolean algebras with operators in terms of frames. Bjarni Jónsson (born 1920 is an Icelandic Mathematician and Logician working in Universal algebra and Lattice theory. 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. Arthur Norman Prior (1914 Masterton, New Zealand – 1969 Trondheim, Norway) was a noted logician. 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. Jaakko Hintikka (born January 12 1929) is a Finnish Philosopher and Logician. 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. Richard Merett Montague (September 20 1930 Stockton California – March 7 1971 Los Angeles) was an American Mathematician and Evert Willem Beth ( July 7, 1908 &ndash April 12, 1964) was a Dutch Philosopher and Logician, whose work principally

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. Saul Aaron Kripke (born on November 13, 1940 in Bay Shore New York) is an American philosopher and Logician now Emeritus 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

^ 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. Sir Michael Anthony Eardley Dummett FBA DLitt (born 1925 is a leading British Philosopher. 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. Saunders Mac Lane ( 4 August 1909, Taftville, Connecticut – 14 April 2005, San Francisco) was an American , 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.

External links

The Stanford Encyclopedia of Philosophy: "Modal Logic" -- by James Garson. A modal logic is any system of formal logic that attempts to deal with modalities. In Logic, a normal Modal logic is a set L of modal formulas such that L contains All propositional tautologies; A Kripke structure is a type of Nondeterministic finite state machine used in Model checking to represent the behaviour of a system Two dimensionalism is an explanatory approach in analytic philosophy The Stanford Encyclopedia of Philosophy (SEP is a freely-accessible Online encyclopedia of Philosophy maintained by Stanford University.
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."

© 2009 citizendia.org; parts available under the terms of GNU Free Documentation License, from http://en.wikipedia.org
network: | |

Contents