查看“︁正规模态逻辑”︁的源代码

在[[逻辑]]中，'''正规[[模态逻辑]]'''是模态公式的集合 <math>L</math>，<math>L</math> 包含
* 所有命题[[重言式]]，
* 所有满足 Kripke 模式的实例: <math>\Box(A\to B)\to(\Box A\to\Box B)</math>，
并且 <math>L</math> 闭合于
* 分拆规则（[[肯定前件]]）:  <math>A\rightarrow B, A\vdash B</math>，
* 必然性规则: 从 <math>\vdash A</math> 推出 <math>\vdash\Box A</math>。

最小化的满足上述条件的逻辑叫做 '''K'''。大多数如今常用的模态逻辑（指有哲学动机的）如C. I. 刘易斯的S4与[[S5 (模态逻辑)|S5]]皆为在'''K'''基础之上的扩展。然而也有一部分如[[道义逻辑]]与[[认识逻辑]]是非正规的，因为它们舍弃了Kripke模式。

== 常见的模态逻辑 ==
<onlyinclude>
下表给出了一些常见的模态逻辑系统。</onlyinclude>表中的标记可参见 [[关系语义#模态逻辑的语义|Kripke 语义 § 常见模态公理模式]]。 <onlyinclude>某些系统的框架条件要求被简化了，它们在给定的框架类中完备，但是可能对应一个更大的框架类。

{| class="wikitable"
! 名称 !! 公理 !! 框架条件
|-
! id="K" | K
| —
| 所有框架
|-
! T
| T
| 自反
|-
! K4
| 4
| 传递
|-
! S4
| T, 4
| [[预序]]
|-
! [[S5 (模态逻辑)|S5]]
| T, 5 或 D, B, 4
| [[等价关系]]
|-
! S4.3
| T, 4, H
| 完全预序
|-
! S4.1
| T, 4, M
| 预序, <math>\forall w\,\exists u\,(w\,R\,u\land\forall v\,(u\,R\,v\Rightarrow u=v))</math>
|-
! S4.2
| T, 4, G
| [[有向集合|有向]]预序
|-
! GL
| GL or 4, GL
| 有穷[[偏序关系#非严格偏序，自反偏序|严格偏序]]
|-
! Grz, S4Grz
| Grz or T, 4, Grz
| 有穷[[偏序]]
|-
! D
| D
| serial
|- 
! D45
| D, 4, 5
| 传递，全序且欧拉
|}</onlyinclude>

==参见==
*Alexander Chagrov and Michael Zakharyaschev, ''Modal Logic'', vol. 35 of Oxford Logic Guides, Oxford University Press, 1997.

{{Logic-stub}}
[[Category:模态逻辑]]