Standard translation
Encyclopedia
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 formula
s are mapped onto unary predicates and the objects in the first-order language are the accessible worlds
. The logical connective
s from propositional logic remain untouched and the modal operators are transformed into first-order formulas according to their semantics
.
In the above,
is the world from which the formula is evaluated. Initially, a free variable
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 
refers to the accessibility relation
that should be used: normally,
and 
refer to a relation 
of the Kripke model
but more than one accessibility relation can exist (a multimodal logic
) in which case subscripts are used. For example,
and 
refer to an accessibility relation 
and 
and 
to 
in the model. Alternatively, it can also be placed inside the modal symbol.
, we expand the outer box to get
meaning that we have now moved from
to an accessible world 
and we now evaluate the remainder of the formula, 
, 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
holds in 
when for all accessible worlds 
from 
and for all accessible worlds 
from 
, the predicate 
is true for 
. Note that the formula is also true when no such accessible worlds exist. In case 
has no accessible worlds then 
is false but the whole formula is vacuously true
: an implication is also true when the antecedent
is false.
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
. 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
to 
and from 
to 
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.
Modal logic
Modal logic is a type of formal logic that extends classical propositional and predicate logic to include operators expressing modality. Modals — words that express modalities — qualify a statement. For example, the statement "John is happy" might be qualified by saying that John is...
, standard translation is a way of transforming formulas of modal logic into formulas of first-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
which capture the meaning of the modal formulas. Standard translation is defined inductively
Recursive definition
In mathematical logic and computer science, a recursive definition is used to define an object in terms of itself ....
on the structure of the formula. In short, atomic formula
Atomic formula
In mathematical logic, an atomic formula is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformulas. Atoms are thus the simplest well-formed formulas of the logic...
s are mapped onto unary predicates and the objects in the first-order language are the accessible worlds
Accessibility relation
In modal logic, an accessibility relation is a binary relation, written as R\,\! between possible worlds.-Description of terms:A statement in logic refers to a sentence that can be true or false...
. The logical connective
Logical connective
In logic, a logical connective is a symbol or word used to connect two or more sentences in a grammatically valid way, such that the compound sentence produced has a truth value dependent on the respective truth values of the original sentences.Each logical connective can be expressed as a...
s from propositional logic remain untouched and the modal operators are transformed into first-order formulas according to their semantics
Kripke semantics
Kripke semantics is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke. It was first made for modal logics, and later adapted to intuitionistic logic and other non-classical systems...
.
Definition
Standard translation is defined as follows:
, where 
is an atomic formulaAtomic formulaIn mathematical logic, an atomic formula is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformulas. Atoms are thus the simplest well-formed formulas of the logic...
; P(x) is true when
holds in world 
.
In the above,
is the world from which the formula is evaluated. Initially, a free variableFree variables and bound variables
In mathematics, and in other disciplines involving formal languages, including mathematical logic and computer science, a free variable is a notation that specifies places in an expression where substitution may take place...
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 refers to the accessibility relationAccessibility relation
In modal logic, an accessibility relation is a binary relation, written as R\,\! between possible worlds.-Description of terms:A statement in logic refers to a sentence that can be true or false...
that should be used: normally,
and refer to a relation of the Kripke modelKripke semantics
Kripke semantics is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke. It was first made for modal logics, and later adapted to intuitionistic logic and other non-classical systems...
but more than one accessibility relation can exist (a multimodal logic
Multimodal logic
A multimodal logic is a modal logic that has more than one primitive modal operator. They find substantial applications in theoretical computer science....
) in which case subscripts are used. For example,
and refer to an accessibility relation and and to in the model. Alternatively, it can also be placed inside the modal symbol.Example
As an example, when standard translation is applied to, we expand the outer box to get
meaning that we have now moved from
to an accessible world and we now evaluate the remainder of the formula, , 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
holds in when for all accessible worlds from and for all accessible worlds from , the predicate is true for . Note that the formula is also true when no such accessible worlds exist. In case has no accessible worlds then is false but the whole formula is vacuously trueVacuous truth
A vacuous truth is a truth that is devoid of content because it asserts something about all members of a class that is empty or because it says "If A then B" when in fact A is inherently false. For example, the statement "all cell phones in the room are turned off" may be true...
: an implication is also true when the antecedent
Antecedent (logic)
An antecedent is the first half of a hypothetical proposition.Examples:* If P, then Q.This is a nonlogical formulation of a hypothetical proposition...
is false.
Standard translation and modal depth
The modal depthModal depth
In modal logic, the modal depth of a formula is the deepest nesting of modal operators . Modal formulas without modal operators have a modal depth of zero.- Definition :Modal depth can be defined as follows...
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
. 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
to and from to 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.