Church's thesis (constructive mathematics)

This principle has formalizations in various mathematical frameworks. Note that there are also more common variants of the Kleene's T predicate ${\displaystyle \mathbf {T} }$.

In first-order theories such as ${\displaystyle {\mathsf {HA}}}$, which cannot quantify over functions directly, ${\displaystyle {\mathrm {CT} }}$ is stated as an axiom schema saying that any definable function is computable in the sense of ${\displaystyle \mathbf {T} }$. For each formula ${\displaystyle \varphi (x,y)}$ of two variables, the schema ${\displaystyle {\mathrm {CT} }_{0}}$ includes the axiom

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

This axiom states that a functional assignment, i.e. a family of valid existence claims ${\displaystyle \exists y}$, can then always be asserted in a computable manner: If for every ${\displaystyle x}$ there is a ${\displaystyle y}$ satisfying ${\displaystyle \varphi }$, then there is in fact an ${\displaystyle e}$ that is the Gödel number of a general recursive function that will, for every ${\displaystyle x}$, produce such a ${\displaystyle y}$ satisfying the formula - and with some ${\displaystyle u}$ being a Gödel number encoding a verifiable computation bearing witness to the fact that ${\displaystyle y}$ is in fact the value of that function at ${\displaystyle x}$.

Relatedly, implications of this form may instead also be established as constructive meta-theoretical properties of theories. I.e. the theory need not necessarily prove the implication (a formula with ${\displaystyle \to }$), but the existence of ${\displaystyle e}$ is meta-logically validated. A theory is then said to be closed under the rule.

The above is also called the arithmetical form of the principle, since only quantifier over numbers appear in its formulation. In higher-order systems that can quantify over functions directly, a form of ${\displaystyle {\mathrm {CT} }}$ can be stated as a single axiom saying that every function, from the natural numbers to the natural numbers, is computable.

$${\displaystyle \forall f\;\exists e\,{\big (}\forall n\;\exists u\;\mathbf {T} (e,n,f(n),u){\big )}}$$

This postulates that all functions ${\displaystyle f}$ are computable, in the Kleene sense, with an index ${\displaystyle e}$. Thus, so are all values ${\displaystyle y=f(x)}$.

For example, in set theory functions are elements of function spaces and total functional by definition. A total function has a unique return value for every input in its domain. Being sets, set theory has quantifiers that range over functions.

The principle can be regarded as the identification of the space ${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$ with the collection of total recursive functions.

The schema ${\displaystyle {\mathrm {CT} }_{0}}$, when added to constructive systems such as ${\displaystyle {\mathsf {HA}}}$, implies the negation of the universally quantified version of the law of the excluded middle for some predicates. As an example, the Halting problem provenly not computably decidable, but assuming classical logic it is a tautology that every Turing machine either halts or does not halt on a given input. Further assuming Church's thesis one in turn concludes that this is computable - a contradiction. In more detail: In sufficiently strong systems, such as ${\displaystyle {\mathsf {HA}}}$, it is possible to express the relation ${\displaystyle h}$ associated with the halting question, relating any code from an enumeration of Turing machines and values from ${\displaystyle \{0,1\}}$. Assuming the classical tautology above, this relation can be proven total, i.e. it constitutes a function that returns ${\displaystyle 1}$ if the machine halts and ${\displaystyle 0}$ if it does not halt. Thus ${\displaystyle {\mathsf {HA}}}$ and ${\displaystyle {\mathrm {CT} }_{0}}$ disproves some consequence of the law of the excluded middle. Principles like the double negation shift (commutativity of universal quantification with a double negation) are also rejected by the principle.

The single axiom form of ${\displaystyle {\mathrm {CT} }}$ with ${\displaystyle \forall f}$ above is consistent with some weak classical systems that do not have the strength to form functions such as the function ${\displaystyle f}$ of the previous paragraph. For example, the classical weak second-order arithmetic ${\displaystyle {\mathsf {RCA_{0}}}}$ is consistent with this single axiom, because ${\displaystyle {\mathsf {RCA_{0}}}}$ has a model in which every function is computable. However, the single-axiom form becomes inconsistent with excluded middle in any system that has axioms sufficient to prove existence of functions such as the function ${\displaystyle h}$. E.g., adoption of variants of countable choice, such as unique choice for the numerical quantifiers,

$${\displaystyle \forall n\;\exists !m\;\phi (n,m)\to \exists a\;\forall k\;\phi (k,a_{k}),}$$

where ${\displaystyle a}$ denotes a sequence, spoil this consistency.

The first-order formulation ${\displaystyle {\mathrm {CT} }_{0}}$ already subsumes the power of such a function comprehension principle via enumerated functions.

Constructively formulated subtheories of ${\displaystyle {\mathsf {ZF}}}$ can typically be shown to be closed under a Church's rule and the corresponding principle is thus compatible. But as an implication (${\displaystyle \to }$) it cannot be proven by such theories, as that would render the stronger, classical theory inconsistent.

Extended Church's thesis ${\displaystyle {\mathrm {ECT_{0}} }}$ extends the claim to functions which are totally defined over a certain type of domain. This may be achieved by allowing to narrowing the scope of the universal quantifier and so can be formally stated by the schema:

$${\displaystyle {\big (}\forall x\;\psi (x)\to \exists y\;\varphi (x,y){\big )}\;\to \;\exists e\,{\big (}\forall x\;\psi (x)\to \exists y\;\exists u\;\mathbf {T} (e,x,y,u)\wedge \varphi (x,y){\big )}}$$

In the above, ${\displaystyle \psi }$ is restricted to be almost-negative. For first-order arithmetic (where the schema is designated ${\displaystyle {\mathrm {ECT_{0}} }}$), this means ${\displaystyle \psi }$ cannot contain any disjunction, and existential quantifiers can only appear in front of ${\displaystyle \Delta _{0}^{0}}$ (decidable) formulas. When considering the domain of all numbers (e.g. when taking ${\displaystyle \psi (x)}$ to be the trivial ${\displaystyle x=x}$), the above reduces to the previous form of Church's thesis.

The extended Church's thesis is used by the school of constructive mathematics founded by Andrey Markov Jr.

This above thesis can be characterized as saying that a sentence is true iff it is computably realisable. This is captured by the following meta-theoretic equivalences:[1]

$${\displaystyle {\mathsf {HA}}+{\mathrm {ECT_{0}} }\vdash {\big (}\varphi \leftrightarrow \exists n\,(n\Vdash \varphi ){\big )}}$$

and

$${\displaystyle {\mathsf {HA}}+{\mathrm {ECT_{0}} }\vdash \varphi \;\iff \;{\big (}{\mathsf {HA}}\vdash \exists n\,(n\Vdash \varphi ){\big )}}$$

Here, ${\displaystyle n\Vdash \varphi }$ stands for "${\displaystyle n{\text{ realises }}\varphi }$" and "${\displaystyle \iff }$" denotes the metatheoretical equivalence. So, it is provable in ${\displaystyle {\mathsf {HA}}}$ with ${\displaystyle {\mathrm {ECT_{0}} }}$ that a sentence is true iff it is realisable. But also, ${\displaystyle \varphi }$ is provably true in ${\displaystyle {\mathsf {HA}}}$ with ${\displaystyle {\mathrm {ECT_{0}} }}$ iff ${\displaystyle \varphi }$ is provably realisable in ${\displaystyle {\mathsf {HA}}}$ without ${\displaystyle {\mathrm {ECT_{0}} }}$.

The second equivalence can be extended with Markov's principle ${\displaystyle {\mathrm {MP} }}$ as follows:

$${\displaystyle {\mathsf {HA}}+{\mathrm {ECT_{0}} }+{\mathrm {MP} }\vdash \varphi \;\iff \;{\text{exists}}\;n\,{\big (}{\mathsf {PA}}\vdash ({\bar {n}}\Vdash \varphi ){\big )}}$$

So, ${\displaystyle \varphi }$ is provably true in ${\displaystyle {\mathsf {HA}}}$ with ${\displaystyle {\mathrm {ECT_{0}} }}$ and ${\displaystyle {\mathrm {MP} }}$ iff one can metatheoretically establish that there is a number ${\displaystyle n}$ which provably realises ${\displaystyle \varphi }$ in ${\displaystyle {\mathsf {PA}}}$. The existential quantifier has to be outside ${\displaystyle {\mathsf {PA}}}$ in this case, because ${\displaystyle {\mathsf {PA}}}$ is non-constructive and lacks the existence property.

• Computable function
• Disjunction and existence properties
• Realizability

• Elliott Mendelson (1990) "Second Thoughts About Church's Thesis and Mathematical Proofs", Journal of Philosophy 87(5): 225–233.