HOME

TheInfoList



OR:

In
mathematical logic Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal ...
, the Friedman translation is a certain transformation of
intuitionistic In the philosophy of mathematics, intuitionism, or neointuitionism (opposed to preintuitionism), is an approach where mathematics is considered to be purely the result of the constructive mental activity of humans rather than the discovery of ...
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 __NOTOC__ Harvey Friedman (born 23 September 1948)Handbook of Philosophical Logic, , p. 38 is an American mathematical logician at Ohio State University in Columbus, Ohio. He has worked on reverse mathematics, a project intended to derive the ax ...
.


Definition

Let ''A'' and ''B'' be intuitionistic formulas, where no
free variable In mathematics, and in other disciplines involving formal languages, including mathematical logic and computer science, a free variable is a notation (symbol) that specifies places in an expression where substitution may take place and is n ...
of ''B'' is quantified in ''A''. The translation ''AB'' is defined by replacing each atomic subformula ''C'' of ''A'' by . For purposes of the translation, ⊥ is considered to be an atomic formula as well, hence it is replaced with (which is equivalent to ''B''). Note that ¬''A'' is defined as an abbreviation for hence


Application

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 In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism.Troelstra 1973:18 It is named after Arend Heyting, who first proposed it. Axiomatization As with first-order Peano ...
(HA), then ''AB'' is also provable in HA.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. Moreover, if ''A'' is a Σ01-formula, then ''AB'' is in HA equivalent to . 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 In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly ...
is Π02-conservative over Heyting arithmetic: if Peano arithmetic proves a Π02-formula ''A'', then ''A'' is already provable in HA.


See also

* Gödel–Gentzen negative translation


Notes

{{reflist Proof theory Constructivism (mathematics)