1、对应定理

框架条件

上面的x、y、z是可能世界集W上的元素。

定义  称模态命题A和一阶命题ψ对应：<W,R>⊨A ⇔ <W, R>⊨ψ

对应定理

（1）   D对应持续性

（2） T对应自返性

（3） B对应对称性

（4） 4对应传递性

（5） 5对应欧性

下面证明（4）。

即要证明：<W, R>⊨□A→□□A⇔<W, R>⊨∀x∀y∀z( Rxy∧Ryz→Rxz)

假设并非<W, R>⊨∀x∀y∀z(Rxy∧Ryz→Rxz)，那么存在w、u、v属于W，Rwu、Ruv、﹁Rwv。令V是<W,R>上的赋值函数，V(w, p)=1，V(u, p)=1，V(v, p)=0。可得：w⊨□p，但并非w⊨□□p，所以并非<W, R>⊨□p→□□p

假设并非<W, R>⊨□A→□□A，则存在<W, R, V>上的某个w，w⊨□p，且w⊨◇◇﹁p。所以存在u，Rwu且u⊨◇﹁p。所以存在v，Ruv且v⊨﹁p。如果Rwv，则并非w⊨□p。矛盾。所以﹁Rwv。

综合上面，（4）得到了证明。

其他的定理证明类似。

    2、可靠性定理

定理：K系统的推理都是有效的，即如果Γ⊢KA，那么Γ⊨A。

证明：在任一个可能世界w上，经典命题逻辑的公理和模态逻辑公理K都是永真的，分离规则MP具有保真性。在w上必然化规则不具有保真性，在模型或框架上它具有保真性，即如果⊨A，则⊨□A。容易证，如果⊢A则⊨A。这实际上是弱可靠性定理。

用归纳法对推理长度进行归纳。

当推理长度为1时，A只能是公理或前提。所以w⊨A。

假设当推理长度为n时，推理中的命题A1、A2、……An在w上真。An+1有几种可能：公理、前提、Ai(i小于等于n)、对Am和Am’(m和m’小于等于n)使用分离规则得到、使用必然化规则RN得到。很明显，前四种情况w⊨A。第五种情况A是□Am，m小于等于n。只有当⊢Am时，才能用RN得到□Am。当⊢Am时，有⊨Am，有⊨□Am，有w⊨□Am所以所以w⊨A。

上面的定理可以推广。

定理：S系统的推理都是有效的，即如果Γ⊢SA，那么Γ⊨ SA。

说明：S是系统K、D、T、B、S4、S5中的一个。Γ⊨sA，即在框架条件符合φ(S)的模型中（φ(S)表示S的模态公理对应的框架条件的合取），如果Γ在可能世界w中真，则A也在w中真。

也就是说系统S的推理不是普遍有效的，必须对框架进行限制。