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.