Church's thesis (constructive mathematics)

In constructive mathematics, Church's thesis (CT) is an axiom which states 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 axiom CT 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 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.

Formal statement

In first-order theories such as HA, which cannot quantify over functions directly, CT is stated as an axiom schema which says that any definable function is computable, using Kleene's T predicate to define computability. For each formula φ(x,y) of two variables, the schema includes the axiom

$(\forall x\;\exists y\;\phi (x,y))\to (\exists e\;\forall x\;\exists y,u\;{\mathbf {T} }(e,x,y,u)\wedge \phi (x,y))$

This axiom asserts that, if for every x there is a y satisfying φ then there is in fact an e which is the Gödel number of a general recursive function that will, for every x, produce such a y satisfying the formula, with some u being a Gödel number encoding a verifiable computation bearing witness to the fact that y is in fact the value of that function at x.

In higher-order systems that can quantify over functions directly, CT can be stated as a single axiom which says that every function from the natural numbers to the natural numbers is computable.

Relationship to classical logic

The schema form of CT shown above, when added to constructive systems such as HA, implies the negation of the law of the excluded middle. As an example, it is a classical tautology that every Turing machine either halts or does not halt on a given input. Assuming this tautology, in sufficiently strong systems such as HA it is possible to form a function h that takes a code for a Turing machine and returns 1 if the machine halts and 0 if it does not halt. Then, from Church's Thesis one would conclude that this function is itself computable, but this is known to be false, because the Halting problem is not computably solvable. Thus HA and CT disproves some consequence of the law of the excluded middle.

The "single axiom" form of CT mentioned above,

$(\forall f)(\exists e)(\forall n)(\exists u)[\mathbf {T} (e,n,f(n),u)]$,

quantifies over functions and says that every function f is computable (with an index e). This axiom is consistent with some weak classical systems that do not have the strength to form functions such as the function f of the previous paragraph. For example, the weak classical system ${\mathsf {RCA}}_{0}$ is consistent with this single axiom, because ${\mathsf {RCA}}_{0}$ has a model in which every function is computable. However, the single-axiom form becomes inconsistent with the law of the excluded middle in any system that has sufficient axioms to construct functions such as the function h in the previous paragraph.

Extended Church's thesis

Extended Church's thesis (ECT) extends the claim to functions which are totally defined over a certain type of domain. It is used by the school of constructive mathematics founded by Andrey Markov Jr. It can be formally stated by the schema:

$(\forall x\;\psi (x)\to \exists y\;\phi (x,y))\to \exists f(\forall x\;\psi (x)\to \exists y,u\;{\mathbf {T}}(f,x,y,u)\wedge \phi (x,y))$

In the above, $\psi$ is restricted to be almost-negative. For first-order arithmetic (where the schema is designated $ECT_{0}$), this means $\psi$ cannot contain any disjunction, and existential quantifiers can only appear in front of $\Delta _{0}^{0}$ (decidable) formulas.

This thesis can be characterised as saying that a sentence is true if and only if it is computably realisable. In fact this is captured by the following meta-theoretic equivalences:

$HA+ECT_{0}\vdash (\phi \leftrightarrow (\exists n\;n\Vdash \phi ))$

$(HA+ECT_{0}\vdash \phi )\leftrightarrow (HA\vdash \exists n\;(n\Vdash \phi ))$

Here, $n\Vdash \phi$ stands for "$n{\text{ realises }}\phi$". So, it is provable in $HA$ with $ECT_{0}$ that a sentence is true iff it is realisable. But also, $\phi$ is provably true in $HA$ with $ECT_{0}$ iff $\phi$ is provably realisable in $HA$ without $ECT_{0}$.

The second equivalence can be extended with Markov's principle (M) as follows:

$(HA+ECT_{0}+M\vdash \phi )\leftrightarrow (\exists n\;PA\vdash ({\bar {n}}\Vdash \phi ))$

So, $\phi$ is provably true in $HA$ with $ECT_{0}$ and $M$ iff there is a number n which provably realises $\phi$ in $PA$. The existential quantifier has to be outside $PA$ in this case, because PA is non-constructive and lacks the existence property.