标准翻译

在模态逻辑中，标准翻译是将模态逻辑的公式转化为一阶逻辑的公式的一种方式，它可以捕捉模态公式的意义。标准翻译是在公式的结构上归纳定义的。简而言之，原子公式被映射到单数谓词上，一阶语言中的对象是可访问的世界。命题逻辑中的逻辑连接词保持不变，模态运算符根据其语义被转化为一阶公式。

标准翻译的定义如下。{displaystylex}是一个世界，在这个世界里，公式是由它产生的。是世界，公式就是从这里被评估的。最初，一个自由变量x{displaystylex}是一个自由变量。每当一个模态运算符需要被翻译时，就会引入一个新的变量，以表示公式的剩余部分需要从该世界进行评估。这里，下标m{displaystylem}指的是应该使用的可及性关系：通常情况下。指的是一种关系R{displaystyle/Diamond}指的是一个关系R的关系，但可以存在一个以上的可及性关系（多模态逻辑），在这种情况下要使用下标。

比如说而我们现在评估公式的剩余部分。◻p{displaystyleBoxp}的剩余部分。在这些可访问的世界中的每一个。这个例子的整个标准翻译成为这正好抓住了模态逻辑中两个盒子的语义。该公式{displaystyle盒子盒子p}在模态逻辑中成立。在以下情况下成立.请注意，当没有这样的可访问世界存在时，该公式也是真的。在这种情况下x{displaystylex}没有可访问的世界，那么没有可访问的世界，那么{displaystyleR(x,y)}是假的，但整个公式是空的。是假的，但是整个公式是空洞的：当前题是假的时候，一个蕴涵也是真的。

一个公式的模态深度在翻译成一阶逻辑时也变得很明显。当一个公式的模态深度为k时，那么一阶逻辑公式就包含了一个从起始世界开始的k个转换的"链"。.这些世界是'链式'的，即这些世界是通过从可访问世界到可访问世界来访问的。非正式地讲，一阶公式中'最长链'的过渡数量是该公式的模态深度。上面的例子中使用的公式的模态深度是2。一阶公式表明，从都需要验证该公式的有效性。这也是该公式的模态深度。