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