Church's thesis (constructive mathematics)

From Wikipedia, the free encyclopedia

In constructive mathematics, Church's thesis refers to 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

$(\forall x \exist y \; \phi(x,y)) \to (\exist f \; \forall x \exist y,u \; \bold{T}(f,x,y,u) \wedge \phi(x,y))$

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 Godel 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 Godel-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.