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 ''A
B'' 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
-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 ''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 . By setting ''B'' = ''A'', 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 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)