In
mathematical logic
Mathematical logic is the study of logic, 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 for ...
, 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 fu ...
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 betwee ...
s. Among other things it can be used to show that the
Π02-theorems of various
first-order theories of
classical mathematics In the foundations of mathematics, classical mathematics refers generally to the mainstream approach to mathematics, which is based on classical logic and ZFC set theory. It stands in contrast to other types of mathematics such as constructive m ...
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 axi ...
.
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 not ...
of ''B'' is
quantified in ''A''. The translation ''A
B'' 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
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 a ...
(HA), then ''A
B'' 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 ''A
B'' is in HA equivalent to . This implies that:
*Heyting arithmetic is closed under the primitive recursive Markov rule (MP
PR): 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 u ...
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 by translating formulas to formulas ...
Notes
{{reflist
Proof theory
Constructivism (mathematics)