Editing Kripke semantics (section)

==== 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]].