Xrthnty

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

The language of propositional modal logic consists of a countably infinite set of propositional variables, a set of truth-functional connectives (in this article $to$ and $neg$ ), and the modal operator $Box$ ("necessarily"). The modal operator $Diamond$ ("possibly") is (classically) the dual of $Box$ and may be defined in terms of necessity like so: $Diamond A:=neg Box neg A$ ("possibly A" is defined as equivalent to "not necessarily not A").^[1]

Basic definitions

A Kripke frame or modal frame is a pair $langle W,Rrangle$ , 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.^[2]

A Kripke model is a triple $langle W,R,Vdash rangle$ , where
$langle W,Rrangle$ is a Kripke frame, and $Vdash$ is a relation between
nodes of W and modal formulas, such that:

$wVdash neg A$ if and only if $wnVdash A$ ,

$wVdash Ato B$ if and only if $wnVdash A$ or $wVdash B$ ,

$wVdash Box A$ if and only if $uVdash A$ for all $u$ such that $w;R;u$ .

We read $wVdash 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.
The satisfaction relation is uniquely determined by its
value on propositional variables.

A formula A is valid in:

a model $langle W,R,Vdash rangle$ , if $wVdash A$ for all w ∈ W,

a frame $langle W,Rrangle$ , if it is valid in $langle W,R,Vdash rangle$ 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 semantic consequence relation reflects its syntactical counterpart, the syntactic consequence relation (derivability).^[3] 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 : $Box Ato A$ .
T is valid in any reflexive frame $langle W,Rrangle$ : if
$wVdash Box A$ , then $wVdash 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:
$uVdash p$ if and only if w R u. Then
$wVdash Box p$ , thus $wVdash 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 (Aleftrightarrow 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 Ato Box Box A$ .

Common modal axiom schemata

The following table lists common modal axioms together with their corresponding classes. The naming of the axioms often varies.

Name	Axiom	Frame condition
K	$Box (Ato B)to (Box Ato Box B)$	N/A
T	$Box Ato A$	reflexive: $w,R,w$
4	$Box Ato Box Box A$	transitive: $w,R,vwedge v,R,uRightarrow w,R,u$
	$Box Box Ato Box A$	dense: $w,R,uRightarrow exists v,(w,R,vland v,R,u)$
D	$Box Ato Diamond A$ or $Diamond top$	serial: $forall w,exists v,(w,R,v)$
B	$Ato Box Diamond A$	symmetric : $w,R,vRightarrow v,R,w$
5	$Diamond Ato Box Diamond A$	Euclidean: $w,R,uland w,R,vRightarrow u,R,v$
GL	$Box (Box Ato A)to Box A$	R transitive, R⁻¹well-founded
Grz	$Box (Box (Ato Box A)to A)to A$	R reflexive and transitive, R⁻¹−Id well-founded
H	$Box (Box Ato B)lor Box (Box Bto A)$	$w,R,uland w,R,vRightarrow u,R,vlor v,R,u$
M	$Box Diamond Ato Diamond Box A$	(a complicated second-order property)
G	$Diamond Box Ato Box Diamond A$	convergent: $w,R,uland w,R,vRightarrow exists x,(u,R,xland v,R,x)$
	$Ato Box A$	$w,R,vRightarrow w=v$
	$Diamond Ato Box A$	partial function: $w,R,uland w,R,vRightarrow u=v$
	$Diamond Aleftrightarrow Box A$	function: $forall w,exists !u,w,R,u$
	$Box A$ or $Box bot$	empty: $forall w,forall u,neg (w,R,u)$

Common modal systems

The following table lists several common normal modal systems. Frame conditions for some of the systems 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.

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, $forall w,exists u,(w,R,uland forall v,(u,R,vRightarrow u=v))$
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
$langle W,R,Vdash rangle$ , 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 Ain X

then

Ain Y

,

XVdash A

if and only if

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

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

Kripke semantics has a straightforward generalization to logics with
more than one modality. A Kripke frame for a language with
$Box _imid ,iin 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:

wVdash Box _iA

if and only if

forall u,(w;R_i;uRightarrow uVdash A).

A simplified semantics, discovered by Tim Carlson, is often used for
polymodal provability logics. A Carlson model is a structure
$langle W,R,D_i_iin I,Vdash rangle$
with a single accessibility relation R, and subsets
D_i ⊆ W for each modality. Satisfaction is
defined as

wVdash Box _iA

if and only if

forall uin D_i,(w;R;uRightarrow uVdash 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.

An intuitionistic Kripke model is a triple
$langle W,leq ,Vdash rangle$ , where $langle W,leq rangle$ is a preordered Kripke frame, and $Vdash$ satisfies the following conditions:

if p is a propositional variable, $wleq u$ , and $wVdash p$ , then $uVdash p$ (persistency condition (cf. monotonicity)),

$wVdash Aland B$ if and only if $wVdash A$ and $wVdash B$ ,

$wVdash Alor B$ if and only if $wVdash A$ or $wVdash B$ ,

$wVdash Ato B$ if and only if for all $ugeq w$ , $uVdash A$ implies $uVdash B$ ,

not $wVdash 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.

Intuitionistic first-order logic

Let L be a first-order language. A Kripke
model of L is a triple
$langle W,leq ,M_w_win Wrangle$ , where
$langle W,leq 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 $wVdash A[e]$ :

$wVdash P(t_1,dots ,t_n)[e]$ if and only if $P(t_1[e],dots ,t_n[e])$ holds in M_w,

$wVdash (Aland B)[e]$ if and only if $wVdash A[e]$ and $wVdash B[e]$ ,

$wVdash (Alor B)[e]$ if and only if $wVdash A[e]$ or $wVdash B[e]$ ,

$wVdash (Ato B)[e]$ if and only if for all $ugeq w$ , $uVdash A[e]$ implies $uVdash B[e]$ ,

not $wVdash bot [e]$ ,

$wVdash (exists x,A)[e]$ if and only if there exists an $ain M_w$ such that $wVdash A[e(xto a)]$ ,

$wVdash (forall x,A)[e]$ if and only if for every $ugeq w$ and every $ain M_u$ , $uVdash A[e(xto 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.^[4]

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.^[5] 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
$langle W,Rrangle$ and $langle W',R'rangle$ is a mapping
$fcolon Wto 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 $langle W,R,Vdash rangle$ and
$langle W',R',Vdash 'rangle$ is a p-morphism of their
underlying frames $fcolon Wto W'$ , which
satisfies

wVdash p

if and only if

f(w)Vdash 'p

, for any propositional variable p.

P-morphisms are a special kind of bisimulations. In general, a
bisimulation between frames $langle W,Rrangle$ and
$langle W',R'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

wVdash p

if and only if

w'Vdash '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 $langle W,R,Vdash rangle$ and a fixed
node w₀ ∈ W, we define a model
$langle W',R',Vdash 'rangle$ , where W’ is the
set of all finite sequences
$s=langle w_0,w_1,dots ,w_nrangle$ such
that w_i R w_i+1 for all
i < n, and $sVdash p$ if and only if
$w_nVdash p$ for a propositional variable
p. The definition of the accessibility relation R’
varies; in the simplest case we put

langle w_0,w_1,dots ,w_nrangle ;R';langle w_0,w_1,dots ,w_n,w_n+1rangle

,

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 $langle W,R,Vdash rangle$ is a mapping f from W to a model
$langle W',R',Vdash '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 $uVdash Box A$ , where $Box Ain X$ , then $vVdash 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,

uVdash A

if and only if

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

Computer science applications

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

Similar work that predated Kripke's revolutionary semantic breakthroughs:

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.

Notes

^ Shoham, Yoav; Leyton-Brown, Kevin (2008). Multiagent Systems: Algorithmic, Game-Theoretic, and Logical Foundations. Cambridge University Press. p. 397. ISBN 0521899435..mw-parser-output cite.citationfont-style:inherit.mw-parser-output qquotes:"""""""'""'".mw-parser-output code.cs1-codecolor:inherit;background:inherit;border:inherit;padding:inherit.mw-parser-output .cs1-lock-free abackground:url("//upload.wikimedia.org/wikipedia/commons/thumb/6/65/Lock-green.svg/9px-Lock-green.svg.png")no-repeat;background-position:right .1em center.mw-parser-output .cs1-lock-limited a,.mw-parser-output .cs1-lock-registration abackground:url("//upload.wikimedia.org/wikipedia/commons/thumb/d/d6/Lock-gray-alt-2.svg/9px-Lock-gray-alt-2.svg.png")no-repeat;background-position:right .1em center.mw-parser-output .cs1-lock-subscription abackground:url("//upload.wikimedia.org/wikipedia/commons/thumb/a/aa/Lock-red-alt-2.svg/9px-Lock-red-alt-2.svg.png")no-repeat;background-position:right .1em center.mw-parser-output .cs1-subscription,.mw-parser-output .cs1-registrationcolor:#555.mw-parser-output .cs1-subscription span,.mw-parser-output .cs1-registration spanborder-bottom:1px dotted;cursor:help.mw-parser-output .cs1-hidden-errordisplay:none;font-size:100%.mw-parser-output .cs1-visible-errorfont-size:100%.mw-parser-output .cs1-subscription,.mw-parser-output .cs1-registration,.mw-parser-output .cs1-formatfont-size:95%.mw-parser-output .cs1-kern-left,.mw-parser-output .cs1-kern-wl-leftpadding-left:0.2em.mw-parser-output .cs1-kern-right,.mw-parser-output .cs1-kern-wl-rightpadding-right:0.2em

^ Gasquet, Olivier; et al. (2013). Kripke’s Worlds: An Introduction to Modal Logics via Tableaux. Springer. pp. 14–16. ISBN 3764385030. Retrieved 24 December 2014.

^ Giaquinto, Marcus (2002). The Search for Certainty : A Philosophical Account of Foundations of Mathematics: A Philosophical Account of Foundations of Mathematics. Oxford University Press. p. 256. ISBN 019875244X. Retrieved 24 December 2014.

^ Intuitionistic Logic. Written by Joan Moschovakis. Published in Stanford Encyclopedia of Philosophy.

^ Goldblatt, Robert (2006). "A Kripke-Joyal Semantics for Noncommutative Logic in Quantales" (PDF). In Governatori, G.; Hodkinson, I.; Venema, Y. Advances in Modal Logic (PDF)|format= requires |url= (help). 6. London: College Publications. pp. 209–225. ISBN 1904987206.

References

Blackburn, P.; de Rijke, M.; Venema, Yde (2002). Modal Logic. Cambridge University Press. ISBN 978-1-316-10195-7.

Bull, Robert A.; Segerberg, K. (2012) [1984]. "Basic Modal Logic". In Gabbay, D.M.; Guenthner, F. Extensions of Classical Logic. Handbook of Philosophical Logic. 2. Springer. pp. 1–88. ISBN 978-94-009-6259-0.

Chagrov, A.; Zakharyaschev, M. (1997). Modal Logic. Clarendon Press. ISBN 978-0-19-853779-3.

Dummett, Michael A. E. (2000). Elements of Intuitionism (2nd ed.). Clarendon Press. ISBN 978-0-19-850524-2.

Fitting, Melvin (1969). Intuitionistic Logic, Model Theory and Forcing. North-Holland. ISBN 978-0-444-53418-7.

Goldblatt, Robert (2006). "Mathematical Modal Logic: a View of its Evolution" (PDF). In Gabbay, Dov M.; Woods, John. Logic and the Modalities in the Twentieth Century (PDF). Handbook of the History of Logic. 7. Elsevier. pp. 1–98. ISBN 978-0-08-046303-2.

Cresswell, M.J.; Hughes, G.E. (2012) [1996]. A New Introduction to Modal Logic. Routledge. ISBN 978-1-134-80028-5.

Mac Lane, Saunders; Moerdijk, Ieke (2012) [1991]. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer. ISBN 978-1-4612-0927-0.

van Dalen, Dirk (2013) [1986]. "Intuitionistic Logic". In Gabbay, Dov M.; Guenthner, Franz. Alternatives to Classical Logic. Handbook of Philosophical Logic. 3. Springer. pp. 225–339. ISBN 978-94-009-5203-4.

External links

Garson, James. "Modal Logic". The Stanford Encyclopedia of Philosophy.

Moschovakis, Joan. "Intuitionistic Logic". Stanford Encyclopedia of Philosophy.

Detlovs, V.; Podnieks, K. "4.4 Constructive Propositional Logic — Kripke Semantics". Introduction to Mathematical Logic. University of Latvia. N.B: Constructive = intuitionistic.

Burgess, John P. "Kripke Models". Archived from the original on 2004-10-20.

Hazewinkel, Michiel, ed. (2001) [1994], "Kripke models", Encyclopedia of Mathematics, Springer Science+Business Media B.V. / Kluwer Academic Publishers, ISBN 978-1-55608-010-4

[Shoham-1] Shoham, Yoav; Leyton-Brown, Kevin (2008). Multiagent Systems: Algorithmic, Game-Theoretic, and Logical Foundations. Cambridge University Press. p. 397. ISBN 0521899435..mw-parser-output cite.citationfont-style:inherit.mw-parser-output qquotes:"""""""'""'".mw-parser-output code.cs1-codecolor:inherit;background:inherit;border:inherit;padding:inherit.mw-parser-output .cs1-lock-free abackground:url("//upload.wikimedia.org/wikipedia/commons/thumb/6/65/Lock-green.svg/9px-Lock-green.svg.png")no-repeat;background-position:right .1em center.mw-parser-output .cs1-lock-limited a,.mw-parser-output .cs1-lock-registration abackground:url("//upload.wikimedia.org/wikipedia/commons/thumb/d/d6/Lock-gray-alt-2.svg/9px-Lock-gray-alt-2.svg.png")no-repeat;background-position:right .1em center.mw-parser-output .cs1-lock-subscription abackground:url("//upload.wikimedia.org/wikipedia/commons/thumb/a/aa/Lock-red-alt-2.svg/9px-Lock-red-alt-2.svg.png")no-repeat;background-position:right .1em center.mw-parser-output .cs1-subscription,.mw-parser-output .cs1-registrationcolor:#555.mw-parser-output .cs1-subscription span,.mw-parser-output .cs1-registration spanborder-bottom:1px dotted;cursor:help.mw-parser-output .cs1-hidden-errordisplay:none;font-size:100%.mw-parser-output .cs1-visible-errorfont-size:100%.mw-parser-output .cs1-subscription,.mw-parser-output .cs1-registration,.mw-parser-output .cs1-formatfont-size:95%.mw-parser-output .cs1-kern-left,.mw-parser-output .cs1-kern-wl-leftpadding-left:0.2em.mw-parser-output .cs1-kern-right,.mw-parser-output .cs1-kern-wl-rightpadding-right:0.2em

[Gasquet-2] Gasquet, Olivier; et al. (2013). Kripke’s Worlds: An Introduction to Modal Logics via Tableaux. Springer. pp. 14–16. ISBN 3764385030. Retrieved 24 December 2014.

[3] Giaquinto, Marcus (2002). The Search for Certainty : A Philosophical Account of Foundations of Mathematics: A Philosophical Account of Foundations of Mathematics. Oxford University Press. p. 256. ISBN 019875244X. Retrieved 24 December 2014.

[4] Intuitionistic Logic. Written by Joan Moschovakis. Published in Stanford Encyclopedia of Philosophy.

[5] Goldblatt, Robert (2006). "A Kripke-Joyal Semantics for Noncommutative Logic in Quantales" (PDF). In Governatori, G.; Hodkinson, I.; Venema, Y. Advances in Modal Logic (PDF)|format= requires |url= (help). 6. London: College Publications. pp. 209–225. ISBN 1904987206.

搜尋此網誌

Xrthnty

Kripke semantics

Contents

Semantics of modal logic

Basic definitions

Correspondence and completeness

Common modal axiom schemata

Common modal systems

Canonical models

Finite model property

Multimodal logics

Semantics of intuitionistic logic

Intuitionistic first-order logic

Kripke–Joyal semantics

Model constructions

General frame semantics

Computer science applications

History and terminology

See also

Notes

References

External links

Popular posts from this blog

California gubernatorial recall election

Telugu cinema

List of Pawn Stars episodes