Church's Thesis (constructive Mathematics)

In constructive mathematics, Church's thesis $$ is an axiom stating that all total functions are computable functions. This principle has formalizations in various mathematical frameworks.

The similarly named Church–Turing thesis states that every effectively calculable function is a computable function. The constructivist variant $$ is stronger in the sense that with it any function is computable.
For any property $\exists y. \varphi(x,y)$ proven not to be validated for all $x$ in a computable manner, the contrapositive of the axiom implies that this then not validated by a total functional at all. So adopting $$ restricts the notion of ''function'' to that of ''computable function''.

The axiom is clearly incompatible with systems that prove the existence of functions also proven not to be computable. For example, Peano arithmetic $$ is such a system. Concretely, the constructive Heyting arithmetic $$ with $$ as an additional axiom is able to disprove some instances of variants of the principle of the excluded middle from classical logic, and it is in this way that the axiom is shown incompatible with $$. However, $$ is equiconsistent with both $$ as well as with the theory given by $$ plus $$. 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 $$, which cannot quantify over functions directly, $$ is stated as an axiom schema saying that any definable function is computable, using Kleene's T predicate to define computability. For each formula $\varphi(x,y)$ of two variables, the schema includes the axiom
$\big(\forall x \; \exist y \; \varphi(x,y)\big)\; \to\; \big(\exist e \; \forall x \; \exist y\; \exist u \; \mathbf(e,x,y,u) \wedge \varphi(x,y)\big)$
This axiom states that a valid functional existence claim $\exists y$ can always be asserted in a computable manner: if for every ''x'' there is a ''y'' satisfying φ then there is in fact an ''e'' that 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''.

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 $\to$), but the existence of $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 $$ can be stated as a single axiom saying that every function, from the natural numbers to the natural numbers, is computable.
$\forall f\;\exists e\;\forall n\;\exists u\;\mathbf(e,n,f(n),u)$
This quantifies over functions and says that every function ''f'' is computable (with an index ''e'').
For example, in set theory functions are elements of function spaces and total functional by definition. In particular, a total function has a unique return value for every input in its domain.

Relationship to classical logic

The schema form of $$ shown above, when added to constructive systems such as $$, implies the negation of the universally quantified version of the law of the excluded middle for some predicates. As an example, it is a classical tautology that every Turing machine either halts or does not halt on a given input. Assuming this classically tautology in sufficiently strong systems such as $$, it is then possible to express a mapping ''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 $$ and $$ disproves some consequence of the law of the excluded middle. Principles like the double negation shift are rejected by the principle.

The "single axiom" form of $$ with $\forall f$ above 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 classical weak second-order arithmetic $$ is consistent with this single axiom, because $$ 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 ''h''. E.g., adoption of variants of countable choice in an arithmetic theory, such as
$\forall n\;\exists! m\;\phi(n, m)\to \exists a\;\forall k\;\phi(k, a_k)$
where $a$ denotes a sequence, spoil this consistency.

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

Extended Church's thesis

Extended Church's thesis $$ 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:

$\big(\forall x \; \psi(x) \to \exist y \; \varphi(x,y)\big)\; \to\; \exist f\, \big(\forall x \; \psi(x) \to \exist y\; \exist u \; \mathbf(f,x,y,u) \wedge \varphi(x,y)\big)$

In the above, $\psi$ is restricted to be ''almost-negative''. For first-order arithmetic (where the schema is designated $$), this means $\psi$ cannot contain any disjunction, and existential quantifiers can only appear in front of $\Delta^0_0$ (decidable) formulas.
When considering the domain of all numbers (e.g. when taking $\psi(x)$ to be the trivial $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.

Realizers and meta-logic

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:Troelstra, A. S. ''Metamathematical investigation of intuitionistic arithmetic and analysis''. Vol 344 of Lecture Notes in Mathematics; Springer, 1973
$+ \vdash \big(\varphi \leftrightarrow \exist n \, (n \Vdash \varphi)\big)$
and
$+ \vdash \varphi \;\iff\; \big( \vdash \exist n \, (n \Vdash \varphi) \big)$
Here, $n \Vdash \varphi$ stands for "$n \text \varphi$". So, it is provable in $$ with $$ that a sentence is true iff it is realisable. But also, $\varphi$ is true in $$ with $$ iff $\varphi$ is realisable in $$ without $$.

The second equivalence can be extended with Markov's principle $$ as follows:
$+ + \vdash \varphi \;\iff\; \big(\exist n \; \vdash (\bar \Vdash \varphi)\big)$
So, $\varphi$ is true in $$ with $$ and $$ iff there is a number ''n'' which realises $\varphi$ in $$. The existential quantifier has to be outside $$ in this case, because $$ is non-constructive and lacks the existence property.

See also

* Computable function
* Disjunction and existence properties
* Realizability

References

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

Constructivism (mathematics)