Friedman Translation
   HOME

TheInfoList



OR:

In
mathematical logic Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
, 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 f ...
formula In science, a formula is a concise way of expressing information symbolically, as in a mathematical formula or a ''chemical formula''. The informal use of the term ''formula'' in science refers to the general construct of a relationship betwe ...
s. Among other things it can be used to show that the Π02-theorems of various first-order theories of
classical mathematics Classical may refer to: European antiquity *Classical antiquity, a period of history from roughly the 7th or 8th century B.C.E. to the 5th century C.E. centered on the Mediterranean Sea *Classical architecture, architecture derived from Greek and ...
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 In mathematics, and in other disciplines involving formal languages, including mathematical logic and computer science, a variable may be said to be either free or bound. Some older books use the terms real variable and apparent variable for f ...
of ''B'' is quantified in ''A''. The translation ''AB'' is defined by replacing each atomic
subformula In mathematical logic, propositional logic and predicate logic, a well-formed formula, abbreviated WFF or wff, often simply formula, is a finite sequence of symbol (formal), symbols from a given alphabet (computer science), alphabet that is part ...
''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. It is named after Arend Heyting, who first proposed it. Axiomatization Heyting arithmetic can be characterized jus ...
(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 . By setting ''B'' = ''A'', 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 nea ...
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 In proof theory, a discipline within mathematical logic, double-negation translation, sometimes called negative translation, is a general approach for embedding classical logic into intuitionistic logic. Typically it is done by translating formulas ...


Notes

{{reflist Proof theory Constructivism (mathematics)