Gödel–McKinsey–Tarski Translation
Let A be a propositional intuitionistic formula. A modal formula T(A) is defined by induction on the complexity of A:
- for any propositional variable ,
As negation is in intuitionistic logic defined by, we also have
T is called the Gödel translation or Gödel–McKinsey–Tarski translation. The translation is sometimes presented in slightly different ways: for example, one may insert before every subformula. All such variants are provably equivalent in S4.
Read more about this topic: Modal Companion
Famous quotes containing the word translation:
“To translate, one must have a style of his own, for otherwise the translation will have no rhythm or nuance, which come from the process of artistically thinking through and molding the sentences; they cannot be reconstituted by piecemeal imitation. The problem of translation is to retreat to a simpler tenor of one’s own style and creatively adjust this to one’s author.”
—Paul Goodman (1911–1972)