在模態邏輯中，標準翻譯是將模態邏輯的公式轉化為一階邏輯的公式的一種方式，它可以捕捉模態公式的意義。標準翻譯是在公式的結構上歸納定義的。簡而言之，原子公式被映射到單數謂詞上，一階語言中的對象是可訪問的世界。命題邏輯中的邏輯連接詞保持不變，模態運算符根據其語義被轉化為一階公式。

標準翻譯的定義如下。{displaystylex}是一個世界，在這個世界里，公式是由它產生的。是世界，公式就是從這里被評估的。最初，一個自由變量x{displaystylex}是一個自由變量。每當一個模態運算符需要被翻譯時，就會引入一個新的變量，以表示公式的剩余部分需要從該世界進行評估。這里，下標m{displaystylem}指的是應該使用的可及性關系：通常情況下。指的是一種關系R{displaystyle/Diamond}指的是一個關系R的關系，但可以存在一個以上的可及性關系（多模態邏輯），在這種情況下要使用下標。

比如說而我們現在評估公式的剩余部分。?p{displaystyleBoxp}的剩余部分。在這些可訪問的世界中的每一個。這個例子的整個標準翻譯成為這正好抓住了模態邏輯中兩個盒子的語義。該公式{displaystyle盒子盒子p}在模態邏輯中成立。在以下情況下成立.請注意，當沒有這樣的可訪問世界存在時，該公式也是真的。在這種情況下x{displaystylex}沒有可訪問的世界，那么沒有可訪問的世界，那么{displaystyleR(x,y)}是假的，但整個公式是空的。是假的，但是整個公式是空洞的：當前題是假的時候，一個蘊涵也是真的。

一個公式的模態深度在翻譯成一階邏輯時也變得很明顯。當一個公式的模態深度為k時，那么一階邏輯公式就包含了一個從起始世界開始的k個轉換的"鏈"。.這些世界是'鏈式'的，即這些世界是通過從可訪問世界到可訪問世界來訪問的。非正式地講，一階公式中'最長鏈'的過渡數量是該公式的模態深度。上面的例子中使用的公式的模態深度是2。一階公式表明，從都需要驗證該公式的有效性。這也是該公式的模態深度。