Standard translation

In modal logic, standard translation is a logic translation that transforms formulas of modal logic into formulas of non-modal first-order logic that capture the meaning of the modal formulas. Standard translation is defined inductively on the structure of the formula. The logical connectives from propositional logic remain untouched and the modal operators are transformed into first-order formulas according to their semantics.

With normal modal logics, it is common to use Kripke semantics for the modal sentences. This involves defining a set of worlds and an accessibility relation on those worlds. ${\displaystyle \Diamond \varphi }$ holds at a world if there is an accessible world at which ${\displaystyle \varphi }$ holds; ${\displaystyle \Box \varphi }$ holds at a world if ${\displaystyle \varphi }$ holds at all accessible worlds. In the propositional fragment of modal logic, atomic formulas are mapped onto unary predicates and the objects in the first-order language are the accessible worlds.

Standard translation is defined as follows:

• ${\displaystyle ST_{x}(p)\equiv P(x)}$, where ${\displaystyle p}$ is an atomic formula; P(x) is true when ${\displaystyle p}$ holds in world ${\displaystyle x}$.
• ${\displaystyle ST_{x}(\top )\equiv \top }$
• ${\displaystyle ST_{x}(\bot )\equiv \bot }$
• ${\displaystyle ST_{x}(\neg \varphi )\equiv \neg ST_{x}(\varphi )}$
• ${\displaystyle ST_{x}(\varphi \wedge \psi )\equiv ST_{x}(\varphi )\wedge ST_{x}(\psi )}$
• ${\displaystyle ST_{x}(\varphi \vee \psi )\equiv ST_{x}(\varphi )\vee ST_{x}(\psi )}$
• ${\displaystyle ST_{x}(\varphi \rightarrow \psi )\equiv ST_{x}(\varphi )\rightarrow ST_{x}(\psi )}$
• ${\displaystyle ST_{x}(\Diamond _{m}\varphi )\equiv \exists y(R_{m}(x,y)\wedge ST_{y}(\varphi ))}$
• ${\displaystyle ST_{x}(\Box _{m}\varphi )\equiv \forall y(R_{m}(x,y)\rightarrow ST_{y}(\varphi ))}$

In the above, ${\displaystyle x}$ is the world from which the formula is evaluated. Initially, a free variable ${\displaystyle x}$ 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 ${\displaystyle m}$ refers to the accessibility relation that should be used: normally, ${\displaystyle \Box }$ and ${\displaystyle \Diamond }$ refer to a relation ${\displaystyle R}$ of the Kripke model but more than one accessibility relation can exist (a multimodal logic) in which case subscripts are used. For example, ${\displaystyle \Box _{a}}$ and ${\displaystyle \Diamond _{a}}$ refer to an accessibility relation ${\displaystyle R_{a}}$ and ${\displaystyle \Box _{b}}$ and ${\displaystyle \Diamond _{b}}$ to ${\displaystyle R_{b}}$ in the model. Alternatively, it can also be placed inside the modal symbol.

As an example, when standard translation is applied to ${\displaystyle \Box \Box p}$, we expand the outer box to get

${\displaystyle \forall y(R(x,y)\rightarrow ST_{y}(\Box p))}$

meaning that we have now moved from ${\displaystyle x}$ to an accessible world ${\displaystyle y}$ and we now evaluate the remainder of the formula, ${\displaystyle \Box p}$, in each of those accessible worlds.

The whole standard translation of this example becomes

${\displaystyle \forall y(R(x,y)\rightarrow (\forall z(R(y,z)\rightarrow P(z))))}$

which precisely captures the semantics of two boxes in modal logic. The formula ${\displaystyle \Box \Box p}$ holds in ${\displaystyle x}$ when for all accessible worlds ${\displaystyle y}$ from ${\displaystyle x}$ and for all accessible worlds ${\displaystyle z}$ from ${\displaystyle y}$, the predicate ${\displaystyle P}$ is true for ${\displaystyle z}$. Note that the formula is also true when no such accessible worlds exist. In case ${\displaystyle x}$ has no accessible worlds then ${\displaystyle R(x,y)}$ is false but the whole formula is vacuously true: an implication is also true when the antecedent is false.

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 ${\displaystyle x}$. 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 ${\displaystyle x}$ to ${\displaystyle y}$ and from ${\displaystyle y}$ to ${\displaystyle z}$ 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.

The standard translation given above can be extended to quantified modal logics. The translation is more complex because it needs to track individuals within worlds as well as the worlds themselves. Commonly, this involves using a two-sorted logic with separate quantifiers for the individuals and for the worlds. A predicate that is n-ary in the modal logic becomes (n+1)-ary in the translation. For example, ${\displaystyle F(x)}$ becomes ${\displaystyle F(w,x)}$.

An important source of additional complexity arises from the fact that quantifiers over individuals can be interpreted in different ways. They may be understood as quantifying over the individuals that exist within a given world, or as quantifying over everything that might possibly exist in all worlds. It is possible to think of each world as having its own domain of individuals, or alternatively to think of a global domain across all worlds containing all possible individuals. In the latter case, some kind of existence operator is needed to indicate that an individual exists at a given world. These different approaches are related to the philosophical distinction between actualism and possibilism.

Further complexity arises if it is accepted that there are rigid designators. These are terms that denote the same individual in all worlds in which that individual exists. This approach to the meaning and logic of names was championed by Saul Kripke in his book Naming and Necessity. An alternative is counterpart theory under which all individuals exist in only one world but they may have counterparts in other worlds.

Non-normal modal logics cannot be handled using the semantics given above because they allow for the accessibility of non-normal or impossible worlds at which contradictions may hold. In place of the Kripke semantics based on accessibility relations, the most common approach is to use neighborhood semantics. Each world has a defined neighborhood and each proposition has a truth set, which is the subset of worlds at which it is true. ${\displaystyle \Box \varphi }$ holds at a world if the truth set of ${\displaystyle \varphi }$ belongs to the neighborhood of that world.

• Patrick Blackburn and Johan van Benthem (1988), Modal Logic: A Semantic Perspective.