Editing Kripke semantics (section)

==Semantics of modal logic==
{{Main| Modal logic }}

The language of propositional  modal logic consists of a [[countable set|countably infinite set]] of [[propositional variable]]s, a set of truth-functional [[Logical connective|connectives]] (in this article <math>\to</math> and <math>\neg</math>), and the modal operator <math>\Box</math> ("necessarily"). The modal operator <math>\Diamond</math> ("possibly") is (classically) the [[duality (mathematics)#Duality in logic and set theory|dual]] of <math>\Box</math> and [[Classical modal logic|may be defined]] in terms of necessity like so: <math>\Diamond A := \neg\Box\neg A</math> ("possibly A" is defined as equivalent to "not necessarily not A").{{sfn|Shoham|Leyton-Brown|2008}}

===Basic definitions===
 
A '''Kripke frame''' or '''modal frame''' is a pair <math>\langle W,R\rangle</math>, 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]].{{sfn|Gasquet|Herzig|Said|Schwarzentruber|2013|pages=14–16}}

A '''Kripke model''' is a triple <math>\langle W,R,\Vdash\rangle</math>,<ref>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).</ref> where
<math>\langle W,R\rangle</math> is a Kripke frame, and <math>\Vdash</math> is a relation between nodes of ''W'' and modal formulas, such that for all ''w''&nbsp;∈&nbsp;''W'' and modal formulas ''A'' and ''B'':

* <math>w\Vdash\neg A</math> if and only if <math>w\nVdash A</math>,
* <math>w\Vdash A\to B</math> if and only if <math>w\nVdash A</math> or <math>w\Vdash B</math>,
* <math>w\Vdash\Box A</math> if and only if <math>u\Vdash A</math> for all <math>u</math> such that <math>w\; R\; u</math>.
We read <math>w\Vdash A</math> as “''w'' satisfies
''A''”, “''A'' is satisfied in ''w''”, or
“''w'' forces ''A''”. The relation <math>\Vdash</math> is called the
''satisfaction relation'', ''evaluation'', or ''[[Forcing (mathematics)|forcing]] relation''.
The satisfaction relation is uniquely determined by its
value on propositional variables.

A formula ''A'' is '''valid''' in:
* a model <math>\langle W,R,\Vdash\rangle</math>, if <math>w\Vdash A</math> for all <math>w \in W</math>,
* a frame <math>\langle W,R\rangle</math>, if it is valid in <math>\langle W,R,\Vdash\rangle</math> for all possible choices of <math>\Vdash</math>,
* 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 '''[[Soundness|sound]]''' with
respect to a class of frames ''C'', if ''L''&nbsp;⊆&nbsp;Thm(''C''). ''L'' is
'''[[Completeness (logic)|complete]]''' wrt ''C'' if ''L''&nbsp;⊇&nbsp;Thm(''C'').

=== Correspondence and completeness ===
Semantics is useful for investigating a logic (i.e. a [[Formal system|derivation system]]) only if the [[Logical consequence#Semantic consequence|semantic consequence]] relation reflects its syntactical counterpart, the ''[[Logical consequence#Syntactic consequence|syntactic consequence]]'' relation (''derivability'').{{sfn|Giaquinto|2002}} 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''&nbsp;=&nbsp;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''' : <math>\Box A\to A</math>.
'''T''' is valid in any [[reflexive relation|reflexive]] frame <math>\langle W,R\rangle</math>: if
<math>w\Vdash \Box A</math>, then <math>w\Vdash A</math>
since ''w''&nbsp;''R''&nbsp;''w''. On the other hand, a frame which
validates '''T''' has to be reflexive: fix ''w''&nbsp;∈&nbsp;''W'', and
define satisfaction of a propositional variable ''p'' as follows:
<math>u\Vdash p</math> if and only if ''w''&nbsp;''R''&nbsp;''u''. Then
<math>w\Vdash \Box p</math>, thus <math>w\Vdash p</math>
by '''T''', which means ''w''&nbsp;''R''&nbsp;''w'' using the definition of
<math>\Vdash</math>. '''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''<sub>1</sub>&nbsp;⊆&nbsp;''L''<sub>2</sub> are normal modal logics that correspond to the same class of frames, but ''L''<sub>1</sub> does not prove all theorems of ''L''<sub>2</sub>. Then ''L''<sub>1</sub> is Kripke incomplete. For example, the schema <math>\Box(A\leftrightarrow\Box
A)\to\Box A</math> 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 <math>\Box
A\to\Box\Box A</math>.

==== 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 [[Epistemic modal logic#The knowledge or truth axiom|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|symbolic logic systems]].

{| class="wikitable"
! Name !! Axiom !! Frame condition
|-
! K 
| <math>\Box (A\to B)\to(\Box A\to \Box B)</math> 
| holds true for any frames
|-
! T 
| <math>\Box A\to A</math> 
| [[reflexive relation|reflexive]]: <math>w\,R\,w</math>
|-
! Q
| <math>\Box\Box A\to\Box A</math>
| [[dense relation|dense]]: <math> w\,R\,u\Rightarrow \exists v\,(w\,R\,v \land v\,R\,u)</math>
|-
! 4 
| <math>\Box A\to\Box\Box A</math>
| [[transitive relation|transitive]]: <math>w\,R\,v \wedge v\,R\,u \Rightarrow w\,R\,u</math>
|-
! D 
| <math>\Box A\to\Diamond A</math>  or <math>\Diamond\top</math> or <math>\neg\Box\bot</math>
| [[serial relation|serial]]: <math>\forall w\,\exists v\,(w\,R\,v)</math>
|-
! B 
| <math>A\to\Box\Diamond A</math> or <math>\Diamond\Box A\to A</math>
| [[symmetric relation|symmetric]] :  <math>w\,R\,v \Rightarrow v\,R\,w</math>
|-
! 5 
| <math>\Diamond A\to\Box\Diamond A</math> 
| [[Euclidean relation|Euclidean]]: <math>w\,R\,u\land w\,R\,v\Rightarrow u\,R\,v</math>
|-
! GL
| <math>\Box(\Box A\to A)\to\Box A</math> 
| ''R'' transitive, ''R''<sup>−1</sup> [[well-founded]]
|-
! Grz<ref>After [[Andrzej Grzegorczyk]].</ref>
| <math>\Box(\Box(A\to\Box A)\to A)\to A</math> 
| ''R'' reflexive and transitive, ''R''<sup>−1</sup>−Id well-founded
|-
! H
| <math>\Box(\Box A\to B)\lor\Box(\Box B\to A)</math>
| <math>w\,R\,u\land w\,R\,v\Rightarrow u\,R\,v\lor v\,R\,u</math><ref>{{Cite book |last=Boolos |first=George |title=The Logic of Provability |publisher=Cambridge University Press |year=1993 |isbn=0-521-43342-8 |pages=148,149}}</ref>
|-
! M
| <math>\Box\Diamond A\to\Diamond\Box A</math>
| (a complicated [[second-order logic|second-order]] property)
|-
! G
| <math>\Diamond\Box A\to\Box\Diamond A</math>
| convergent: <math>w\,R\,u\land w\,R\,v\Rightarrow\exists x\,(u\,R\,x\land v\,R\,x)</math>
|-
! -
| <math> A\to\Box A</math> 
| discrete: <math>w\,R\,v\Rightarrow w=v</math>
|-
! -
| <math>\Diamond A\to\Box A</math>
| [[partial function]]:  <math> w\,R\,u\land w\,R\,v\Rightarrow u=v</math>
|-
! -
| <math>\Diamond A\leftrightarrow\Box A</math>
| function: <math> \forall w\,\exists!u\, w\,R\,u</math> (<math> \exists!</math> is the [[uniqueness quantification]])
|-
!-
| <math>\Box A</math> or <math>\Box \bot</math>
| empty: <math> \forall w\,\forall u\, \neg ( w\, R\,u)</math>
|-
|}
Axiom '''K''' can also be [[Rewriting|rewritten]] as <math>\Box [(A\to B)\land A]\to \Box B</math>, which logically establishes [[modus ponens]] as a [[rule of inference]] in every possible world.

Note that for axiom '''D''', <math>\Diamond A</math> implicitly implies <math>\Diamond\top</math>, 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 <math>\Diamond A \rightarrow \Diamond\top</math> is similar to the implicit implication by [[Quantifier (logic)#Range of quantification|existential quantifier on the range of quantification]].

==== Common modal systems ====
{{:Normal modal logic}}

===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 set]]s 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
<math>\langle W,R,\Vdash\rangle</math>, where ''W'' is the set of all ''L''-''MCS'',
and the relations ''R'' and <math>\Vdash</math> are as follows:
: <math>X\;R\;Y</math> if and only if for every formula <math>A</math>, if <math>\Box A\in X</math> then <math>A\in Y</math>,
: <math>X\Vdash A</math> if and only if <math>A\in X</math>.
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
[[compactness theorem|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 [[decision problem|undecidable]] whether a given axiom is
canonical. We know a nice sufficient condition: [[Henrik Sahlqvist]] identified a broad class of formulas (now called
[[Sahlqvist formula]]s) such that
* a Sahlqvist formula is canonical,
* the class of frames corresponding to a Sahlqvist formula is [[first-order logic|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 (logic)|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 [[#Model constructions|filtration]] or
[[#Model constructions|unravelling]]. As another possibility,
completeness proofs based on [[cut-elimination|cut-free]]
[[sequent calculus|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 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.

===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
<math>\{\Box_i\mid\,i\in I\}</math> as the set of its necessity operators
consists of a non-empty set ''W'' equipped with binary relations
''R<sub>i</sub>'' for each ''i''&nbsp;∈&nbsp;''I''. The definition of a
satisfaction relation is modified as follows:

: <math>w\Vdash\Box_i A</math> if and only if <math>\forall u\,(w\;R_i\;u\Rightarrow u\Vdash A).</math>

A simplified semantics, discovered by Tim Carlson, is often used for
polymodal [[provability logic]]s. A '''Carlson model''' is a structure
<math>\langle W,R,\{D_i\}_{i\in I},\Vdash\rangle</math>
with a single accessibility relation ''R'', and subsets
''D<sub>i</sub>''&nbsp;⊆&nbsp;''W'' for each modality. Satisfaction is
defined as

: <math>w\Vdash\Box_i A</math> if and only if <math>\forall u\in D_i\,(w\;R\;u\Rightarrow u\Vdash A).</math>

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.