In constructive mathematics, Church's thesis is the mathematical assertion that all total functions are recursive. It gets its name after the informal Church–Turing thesis, which states that every algorithm is in fact a recursive function, but the two are different. One way it can be formally stated is the schema
for any predicate φ, and the variables range over the natural numbers. This schema asserts that, if for every x there is a y satisfying some predicate, then there is in fact an f which is the Gödel number of a general recursive function which will, for every x, produce such a y satisfying that predicate. (T is some universal predicate which decodes the Gödel-numbering used.)
The thesis is incompatible with classical logic, since adding it to Heyting arithmetic allows one to disprove instances of the law of the excluded middle. However, Heyting arithmetic is equiconsistent with Peano arithmetic as well as with Heyting arithmetic plus Church's thesis. That is, adding either the law of the excluded middle or Church's thesis does not make Heyting arithmetic inconsistent, but adding both does.
An extended version of Church's thesis makes the same assertion for total functions whose domain are certain subsets of the natural numbers. It is used by the school of constructive mathematics founded by Andrey Markov Jr.
See also
 |
This mathematical logic-related article is a stub. You can help Wikipedia by expanding it. |
This entry is from Wikipedia, the leading user-contributed encyclopedia. It may not have been reviewed by professional editors (see full disclaimer)
