Friedman translation

In mathematical logic, the Friedman translation is a certain transformation of intuitionistic formulas. Among other things it can be used to show that the Π⁰₂-theorems of various first-order theories of classical mathematics are also theorems of intuitionistic mathematics. It is named after its discoverer, Harvey Friedman.

Let A and B be intuitionistic formulas, where no free variable of B is quantified in A. The translation A^B 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). Note that ¬A is defined as an abbreviation for A → ⊥; hence (¬A)^B = A^B → 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. The key condition is that the ${\displaystyle \Delta _{0}^{0}}$-sentences of the logic be decidable, allowing the unquantified theorems of the intuitionistic and classical theories to coincide.

For example, if A is provable in Heyting arithmetic (HA), then A^B is also provable in HA.^[1] Moreover, if A is a Σ⁰₁-formula, then A^B is in HA equivalent to A ∨ B. By setting B = A, this implies that:

• Heyting arithmetic is closed under the primitive recursive Markov rule (MP_PR): if the formula ¬¬A is provable in HA, where A is a Σ⁰₁-formula, then A is also provable in HA.
• Peano arithmetic is Π⁰₂-conservative over Heyting arithmetic: if Peano arithmetic proves a Π⁰₂-formula A, then A is already provable in HA.

• Gödel–Gentzen negative translation