About: Church's thesis (constructive mathematics)

In constructive mathematics, Church's thesis is an axiom stating that all total functions are computable functions. thus restricts the class of functions to computable ones and consequently is incompatible with classical logic in sufficiently strong systems. For example, Heyting arithmetic with as an addition axiom is able to disprove some instances of variants 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.