In modal logic, standard translation is a way of transforming formulas of modal logic into formulas of firstorder 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 firstorder language are the accessible worlds. The logical connectives from propositional logic remain untouched and the modal operators are transformed into firstorder formulas according to their semantics.
Contents

Definition 1

Example 2

Standard translation and modal depth 3

References 4
Definition
Standard translation is defined as follows:

ST_x(p) \equiv P(x), where p is an atomic formula; P(x) is true when p holds in world x.

ST_x(\top) \equiv \top

ST_x(\bot) \equiv \bot

ST_x(\neg \varphi) \equiv \neg ST_x(\varphi)

ST_x(\varphi \wedge \psi) \equiv ST_x(\varphi) \wedge ST_x(\psi)

ST_x(\varphi \vee \psi) \equiv ST_x(\varphi) \vee ST_x(\psi)

ST_x(\varphi \rightarrow \psi) \equiv ST_x(\varphi) \rightarrow ST_x(\psi)

ST_x(\Diamond_m \varphi) \equiv \exists y ( R_m(x, y) \wedge ST_y(\varphi))

ST_x(\Box_m \varphi) \equiv \forall y ( R_m(x, y) \rightarrow ST_y(\varphi))
In the above, x is the world from which the formula is evaluated. Initially, a free variable 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 m refers to the accessibility relation that should be used: normally, \Box and \Diamond refer to a relation R of the Kripke model but more than one accessibility relation can exist (a multimodal logic) in which case subscripts are used. For example, \Box_a and \Diamond_a refer to an accessibility relation R_a and \Box_b and \Diamond_b to R_b in the model. Alternatively, it can also be placed inside the modal symbol.
Example
As an example, when standard translation is applied to \Box \Box p, we expand the outer box to get

\forall y ( R(x, y) \rightarrow ST_y(\Box p))
meaning that we have now moved from x to an accessible world y and we now evaluate the remainder of the formula, \Box p, in each of those accessible worlds.
The whole standard translation of this example becomes

\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 \Box \Box p holds in x when for all accessible worlds y from x and for all accessible worlds z from y, the predicate P is true for z. Note that the formula is also true when no such accessible worlds exist. In case x has no accessible worlds then R(x,y) 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 firstorder logic. When the modal depth of a formula is k, then the firstorder logic formula contains a 'chain' of k transitions from the starting world 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 firstorder formula is the modal depth of the formula.
The modal depth of the formula used in the example above is two. The firstorder formula indicates that the transitions from x to y and from y to 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.
References
This article was sourced from Creative Commons AttributionShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and USA.gov, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for USA.gov and content contributors is made possible from the U.S. Congress, EGovernment Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a nonprofit organization.