模态深度

在模态逻辑中，一个公式的模态深度是模态运算符的最深嵌套（通常为).没有模态运算符的模态公式的模态深度为零。

模态深度可以被定义如下。让MD(ϕ){displaystyleMD(phi)}是一个计算模态深度的函数。是一个计算模态公式的模态深度的函数

一个公式的模态深度表明在检查该公式的有效性时需要在克里普克模型中寻找"多远"。对于每个模态算子，人们需要从模型中的一个世界过渡到一个可以通过可及性关系访问的世界。模态深度表示验证一个公式的有效性所需的从一个世界到下一个世界的最长的过渡"链"。例如，要检查是否M,w⊨◊◊φ{displaystyleM,wmodelsDiamondDiamondvarphi}，我们需要检查是否存在着"M"和"w"。

我们需要检查是否存在一个可访问的世界{displaystyleu}）在模型中确定公式是否成立；这就是该公式的模态深度。)来确定该公式是否成立；根据定义，这就是该公式的模态深度。模态深度是对转换数量的一个上限（包括），因为对于盒子来说，只要一个世界没有可访问的世界，模态公式也是真的（即。，可能需要在模型中采取两个步骤，但也可能更少，这取决于模型的结构。假设没有世界可以在w{displaystylew}中没有世界可以进入。；根据之前对以盒子为外部算子的公式的有效性的观察，该公式现在琐碎地成立。