# 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
