Concept
In constructive mathematics, Church's thesis is an axiom stating that all total functions are computable functions. The similarly named Church–Turing thesis states that every effectively calculable function is a computable function, thus collapsing the former notion into the latter. is stronger in the sense that with it every function is computable. The constructivist principle is fully formalizable, using formalizations of "function" and "computable" that depend on the theory considered. A common context is recursion theory as established since the 1930's. Adopting as a principle, then for a predicate of the form of a family of existence claims (e.g. below) that is proven not to be validated for all in a computable manner, the contrapositive of the axiom implies that this is then not validated by any total function (i.e. no mapping corresponding to ). It thus collapses the possible scope of the notion of function compared to the underlying theory, restricting it to the defined notion of computable function. The axiom in turn affects ones proof calculus, negating some common classical propositions. The axiom is incompatible with systems that validate total functional value associations and evaluations that are also proven not to be computable. For example, Peano arithmetic is such a system. Concretely, the constructive Heyting arithmetic with the thesis in its first-order formulation, , as an additional axiom is able to disprove some universally closed variants of instances of the principle of the excluded middle. It is in this way that the axiom is shown incompatible with . However, is equiconsistent with both as well as with the theory given by plus . That is, adding either the law of the excluded middle or Church's thesis does not make Heyting arithmetic inconsistent, but adding both does. This principle has formalizations in various mathematical frameworks. Let denote Kleene's T predicate, so that e.g. validity of the predicate expresses that is the index of a total computable function.