# 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 Π2-theorems of various first-order theories of classical mathematics are also theorems of intuitionistic mathematics.

It is named after its discoverer, Harvey Friedman.

## Definition

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.

## Application

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.

## See also

Credits to the contents of this page go to the authors of the corresponding Wikipedia page: en.wikipedia.org/wiki/Friedman translation.