Friedman translation

From Wikipedia, the free encyclopedia
Jump to: navigation, search

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

Definition[edit]

Let A and B be intuitionistic formulas, where no free variable of B is quantified in A. The translation AB is defined by replacing each atomic subformula C of A by CB. 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 = ABB.

Application[edit]

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 \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 AB is also provable in HA.[1] Moreover, if A is a Σ01-formula, then AB is in HA equivalent to AB. 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 Σ01-formula, then A is also provable in HA.
  • Peano arithmetic is Π02-conservative over Heyting arithmetic: if Peano arithmetic proves a Π02-formula A, then A is already provable in HA.

See also[edit]

Notes[edit]

  1. ^ Harvey Friedman. Classically and Intuitionistically Provably Recursive Functions. In Scott, D. S. and Muller, G. H. Editors, Higher Set Theory, Volume 699 of Lecture Notes in Mathematics, Springer Verlag (1978), pp. 21–28. doi:10.1007/BFb0103100