Editing Kripke semantics (section)

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