Friedman translation

In mathematical logic, the Friedman translation is a certain transformation of intuitionistic formulas. Friedman translation_sentence_0

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. Friedman translation_sentence_1

It is named after its discoverer, Harvey Friedman. Friedman translation_sentence_2

Definition Friedman translation_section_0

Let A and B be intuitionistic formulas, where no free variable of B is quantified in A. Friedman translation_sentence_3

The translation A is defined by replacing each atomic subformula C of A by C ∨ B. Friedman translation_sentence_4

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). Friedman translation_sentence_5

Note that ¬A is defined as an abbreviation for A → ⊥, hence (¬A) = A → B. Friedman translation_sentence_6

Application Friedman translation_section_1

For example, if A is provable in Heyting arithmetic (HA), then A is also provable in HA. Friedman translation_sentence_7

Moreover, if A is a Σ1-formula, then A is in HA equivalent to A ∨ B. Friedman translation_sentence_8

This implies that: Friedman translation_sentence_9

Friedman translation_unordered_list_0

• 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.Friedman translation_item_0_0
• Peano arithmetic is Π2-conservative over Heyting arithmetic: if Peano arithmetic proves a Π2-formula A, then A is already provable in HA.Friedman translation_item_0_1

See also Friedman translation_section_2

Friedman translation_unordered_list_1

• Gödel–Gentzen negative translationFriedman translation_item_1_2

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