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.
Propositional Normal Modal Logics 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.
Definition Standard translation is defined as follows:
S T x ( p ) ≡ P ( x ) {\displaystyle ST_{x}(p)\equiv P(x)} , where p {\displaystyle p} is an atomic formula; P(x) is true when p {\displaystyle p} holds in world x {\displaystyle x} .
S T x ( ⊤ ) ≡ ⊤ {\displaystyle ST_{x}(\top )\equiv \top }
S T x ( ⊥ ) ≡ ⊥ {\displaystyle ST_{x}(\bot )\equiv \bot }
S T x ( ¬ φ ) ≡ ¬ S T x ( φ ) {\displaystyle ST_{x}(\neg \varphi )\equiv \neg ST_{x}(\varphi )}
S T x ( φ ∧ ψ ) ≡ S T x ( φ ) ∧ S T x ( ψ ) {\displaystyle ST_{x}(\varphi \wedge \psi )\equiv ST_{x}(\varphi )\wedge ST_{x}(\psi )}
S T x ( φ ∨ ψ ) ≡ S T x ( φ ) ∨ S T x ( ψ ) {\displaystyle ST_{x}(\varphi \vee \psi )\equiv ST_{x}(\varphi )\vee ST_{x}(\psi )}
S T x ( φ → ψ ) ≡ S T x ( φ ) → S T x ( ψ ) {\displaystyle ST_{x}(\varphi \rightarrow \psi )\equiv ST_{x}(\varphi )\rightarrow ST_{x}(\psi )}
S T x ( ◊ m φ ) ≡ ∃ y ( R m ( x , y ) ∧ S T y ( φ ) ) {\displaystyle ST_{x}(\Diamond _{m}\varphi )\equiv \exists y(R_{m}(x,y)\wedge ST_{y}(\varphi ))}
S T x ( ◻ m φ ) ≡ ∀ y ( R m ( x , y ) → S T y ( φ ) ) {\displaystyle ST_{x}(\Box _{m}\varphi )\equiv \forall y(R_{m}(x,y)\rightarrow ST_{y}(\varphi ))}
… excerpt ends here. Continue reading the full article.
