Standard translation

In modal logic, standard translation is a way of transforming formulas of modal logic into formulas of first-order logic which capture the meaning of the modal formulas. Standard translation is defined inductively on the structure of the formula. In short, atomic formulas are mapped onto unary predicates and the objects in the first-order language are the accessible worlds. The logical connectives from propositional logic remain untouched and the modal operators are transformed into first-order formulas according to their semantics.
Definition.
Standard translation is defined as follows:
In the above, formula_4 is the world from which the formula is evaluated. Initially, a free variable formula_4 is used and whenever a modal operator needs to be translated, a fresh variable is introduced to indicate that the remainder of the formula needs to be evaluated from that world. Here, the subscript formula_15 refers to the accessibility relation that should be used: normally, formula_16 and formula_17 refer to a relation formula_18 of the Kripke model but more than one accessibility relation can exist (a multimodal logic) in which case subscripts are used. For example, formula_19 and formula_20 refer to an accessibility relation formula_21 and formula_22 and formula_23 to formula_24 in the model. Alternatively, it can also be placed inside the modal symbol.
Example.
As an example, when standard translation is applied to formula_25, we expand the outer box to get
meaning that we have now moved from formula_4 to an accessible world formula_28 and we now evaluate the remainder of the formula, formula_29, in each of those accessible worlds.
The whole standard translation of this example becomes
which precisely captures the semantics of two boxes in modal logic. The formula formula_25 holds in formula_4 when for all accessible worlds formula_28 from formula_4 and for all accessible worlds formula_35 from formula_28, the predicate formula_37 is true for formula_35. Note that the formula is also true when no such accessible worlds exist. In case formula_4 has no accessible worlds then formula_40 is false but the whole formula is vacuously true: an implication is also true when the antecedent is false.
Standard translation and modal depth.
The modal depth of a formula also becomes apparent in the translation to first-order logic. When the modal depth of a formula is "k", then the first-order logic formula contains a 'chain' of "k" transitions from the starting world formula_4. The worlds are 'chained' in the sense that these worlds are visited by going from accessible to accessible world. Informally, the number of transitions in the 'longest chain' of transitions in the first-order formula is the modal depth of the formula.
The modal depth of the formula used in the example above is two. The first-order formula indicates that the transitions from formula_4 to formula_28 and from formula_28 to formula_35 are needed to verify the validity of the formula. This is also the modal depth of the formula as each modal operator increases the modal depth by one.