> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/600-toc/630-computability-theory/church-thesis.md).

# Church Thesis

<https://en.wikipedia.org/wiki/Church%27s\\_thesis\\_(constructive\\_mathematics)>

In constructive mathematics, Church's thesis (CT) is an axiom stating that all total functions are computable.

The axiom takes its name from the `Church-Turing thesis`, which states that every *effectively calculable function* is a *computable function*, but the constructivist version is much stronger, claiming that every function is computable.

The CT axiom is incompatible with classical logic in sufficiently strong systems. For example, *Heyting arithmetic* (HA) with CT as an addition axiom is able to disprove some instances of the law of the excluded middle. However, Heyting arithmetic is equiconsistent with *Peano arithmetic* (PA) as well as with Heyting arithmetic plus CT. That is, adding either the law of the excluded middle or CT does not make HA inconsistent, but adding both does.

* Formal statement
* Relationship to classical logic
* Extended Church's thesis