In mathematical logic, the Friedman translation is a certain transformation of intuitionistic formulas.
The translation AB is defined by replacing each atomic subformula C of A by C ∨ B.
For purposes of the translation, ⊥ is considered to be an atomic formula as well; hence it is replaced with ⊥ ∨ B (which is equivalent to B).
The Friedman translation can be used to show the closure of many intuitionistic theories under the Markov rule, and to obtain partial conservativity results.
-sentences of the logic be decidable, allowing the unquantified theorems of the intuitionistic and classical theories to coincide.