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 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) = A → B.
For example, if A is provable in Heyting arithmetic (HA), then A is also provable in HA.
Moreover, if A is a Σ1-formula, then A is in HA equivalent to A ∨ B.
This implies that:
- Heyting arithmetic is closed under the primitive recursive Markov rule (MPPR): if the formula ¬¬A is provable in HA, where A is a Σ1-formula, then A is also provable in HA.
- Peano arithmetic is Π2-conservative over Heyting arithmetic: if Peano arithmetic proves a Π2-formula A, then A is already provable in HA.
Credits to the contents of this page go to the authors of the corresponding Wikipedia page: en.wikipedia.org/wiki/Friedman translation.