Church's thesis (constructive mathematics)

Short description: Axiom

In constructive mathematics, Church's thesis [math]\displaystyle{ {\mathrm{CT}} }[/math] is the principle stating that all total functions are computable functions.

The similarly named Church–Turing thesis states that every effectively calculable function is a computable function, thus collapsing the former notion into the latter. [math]\displaystyle{ {\mathrm{CT}} }[/math] is stronger in the sense that with it every function is computable. The constructivist principle is however also given, in different theories and incarnations, as a fully formal axiom. The formalization depends on "function" and "computable" of the theory at hand. A common context is recursion theory as established since the 1930's.

Adopting [math]\displaystyle{ {\mathrm{CT}} }[/math] as a principle, then for a predicate of the form of a family of existence claims (e.g. [math]\displaystyle{ \exists! y. \varphi(x,y) }[/math] below) that is proven not to be validated for all [math]\displaystyle{ x }[/math] in a computable manner, the contrapositive of the axiom implies that this is then not validated by any total function (i.e. no mapping corresponding to [math]\displaystyle{ x\mapsto y }[/math]). It thus collapses the possible scope of the notion of function compared to the underlying theory, restricting it to the defined notion of computable function. In turn, the axiom is incompatible with systems that validate total functional value associations and evaluations that are also proven not to be computable. More concretely, it affects ones proof calculus in a way that it makes provable the negations of some common classically provable propositions.

For example, Peano arithmetic [math]\displaystyle{ {\mathsf{PA}} }[/math] is such a system. Instead of it, one may consider the constructive theory of Heyting arithmetic [math]\displaystyle{ {\mathsf{HA}} }[/math] with the thesis in its first-order formulation [math]\displaystyle{ {\mathrm{CT}}_0 }[/math] as an additional axiom, concerning associations between natural numbers. This theory disproves some universally closed variants of instances of the principle of the excluded middle. It is in this way that the axiom is shown incompatible with [math]\displaystyle{ {\mathsf{PA}} }[/math]. However, [math]\displaystyle{ {\mathsf{HA}} }[/math] is equiconsistent with both [math]\displaystyle{ {\mathsf{PA}} }[/math] as well as with the theory given by [math]\displaystyle{ {\mathsf{HA}} }[/math] plus [math]\displaystyle{ {\mathrm{CT}}_0 }[/math]. 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

This principle has formalizations in various mathematical frameworks. Let [math]\displaystyle{ T_1 }[/math] denote Kleene's T predicate, so that e.g. validity of the predicate [math]\displaystyle{ \forall x\,\exists w\,T_1(e, x, w) }[/math] expresses that [math]\displaystyle{ e }[/math] is the index of a total computable function. Note that there are also variations on [math]\displaystyle{ T_1 }[/math] and the value extracting [math]\displaystyle{ U }[/math], as functions with return values. Here they are expressed as primitive recursive predicates. Write [math]\displaystyle{ TU(e, x, w, y) }[/math] to abbreviate [math]\displaystyle{ T_1(e, x, w)\land U(w, y) }[/math], as the values [math]\displaystyle{ y }[/math] plays a role in the principle's formulations. So the computable function with index [math]\displaystyle{ e }[/math] terminates on [math]\displaystyle{ x }[/math] with value [math]\displaystyle{ y }[/math] iff [math]\displaystyle{ \exists w\,TU(e, x, w, y) }[/math]. This [math]\displaystyle{ \Sigma_1^0 }[/math]-predicate of on triples [math]\displaystyle{ e, x, y }[/math] may be expressed by [math]\displaystyle{ \{e\}(x)=y }[/math], at the cost of introducing abbreviating notation involving the sign already used for arithmetic equality. In first-order theories such as [math]\displaystyle{ {\mathsf{HA}} }[/math], which cannot quantify over relations and function directly, [math]\displaystyle{ {\mathrm{CT}} }[/math] may be stated as an axiom schema saying that for any definable total relation, which comprises a family of valid existence claims [math]\displaystyle{ \exists y }[/math], the latter are computable in the sense of [math]\displaystyle{ TU }[/math]. For each formula [math]\displaystyle{ \varphi(x,y) }[/math] of two variables, the schema [math]\displaystyle{ {\mathrm{CT}}_0 }[/math] includes the axiom

[math]\displaystyle{ \big(\forall x \; \exists y \; \varphi(x,y)\big)\; \to\; \exists e\,\big(\forall x \; \exists y\; \exists w \; TU(e, x, w, y) \wedge \varphi(x, y)\big) }[/math]

In words: If for every [math]\displaystyle{ x }[/math] there is a [math]\displaystyle{ y }[/math] satisfying [math]\displaystyle{ \varphi }[/math], then there is in fact an [math]\displaystyle{ e }[/math] that is the Gödel number of a partial recursive function that will, for every [math]\displaystyle{ x }[/math], produce such a [math]\displaystyle{ y }[/math] satisfying the formula - and with some [math]\displaystyle{ w }[/math] being a Gödel number encoding a verifiable computation bearing witness to the fact that [math]\displaystyle{ y }[/math] is in fact the value of that function at [math]\displaystyle{ x }[/math].

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 [math]\displaystyle{ \to }[/math]), but the existence of [math]\displaystyle{ e }[/math] is meta-logically validated. A theory is then said to be closed under the rule.

Variants

Extended Church's thesis

The statement [math]\displaystyle{ {\mathrm{ECT_0}} }[/math] extends the claim to relations which are defined and total 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:

[math]\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 w \; TU(e, x, w, y) \wedge \varphi(x,y)\big) }[/math]

In the above, [math]\displaystyle{ \psi }[/math] is restricted to be almost-negative. For first-order arithmetic (where the schema is designated [math]\displaystyle{ {\mathrm{ECT_0}} }[/math]), this means [math]\displaystyle{ \psi }[/math] cannot contain any disjunction, and existential quantifiers can only appear in front of [math]\displaystyle{ \Delta^0_0 }[/math] (decidable) formulas. In the presence of Markov's principle [math]\displaystyle{ {\mathrm{MP}} }[/math], the syntactical restrictions may be somewhat loosened.

When considering the domain of all numbers (e.g. when taking [math]\displaystyle{ \psi(x) }[/math] to be the trivial [math]\displaystyle{ x=x }[/math]), the above reduces to the previous form of Church's thesis.

These first-order formulations are fairly strong in that they also constitute a form of function choice: Total relations contain total recursive functions.

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

Functional premise

[math]\displaystyle{ {\mathrm{CT}}_0! }[/math] denotes the weaker variant of the principle in which the premise demands unique existence (of [math]\displaystyle{ y }[/math]), i.e. the return value already has to be determined.

Higher order formulation

The first formulation of the thesis above is also called the arithmetical form of the principle, since only quantifier over numbers appear in its formulation. It uses a general relation [math]\displaystyle{ \varphi }[/math] in its antecedent. In a framework like recursion theory, a functions may be representable as a functional relation, granting a unique output value for every input.

In higher-order systems that can quantify over (total) functions directly, a form of [math]\displaystyle{ {\mathrm{CT}} }[/math] can be stated as a single axiom, saying that every function from the natural numbers to the natural numbers is computable. In terms of the primitive recursive predicates,

[math]\displaystyle{ \forall f\;\exists e\,\big(\forall x\;\exists w\;TU(e, x, w, f(x))\big) }[/math]

This postulates that all functions [math]\displaystyle{ f }[/math] are computable, in the Kleene sense, with an index [math]\displaystyle{ e }[/math] in the theory. Thus, so are all values [math]\displaystyle{ y = f(x) }[/math]. One may write [math]\displaystyle{ \forall f\;\exists e\, f\cong \{e\} }[/math] with [math]\displaystyle{ f\cong g }[/math] denoting extensional equality [math]\displaystyle{ \forall x. f(x)=g(x) }[/math].

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 [math]\displaystyle{ {\mathbb N}^{\mathbb N} }[/math] with the collection of total recursive functions. In realzability topoi, this exponential object of the natural numbers object can also be identified with less restrictive collections of maps.

Weaker statements

There are weaker forms of the thesis, variously called [math]\displaystyle{ {\mathrm {WCT}} }[/math].

By inserting a double negation before the index existence claim in the higher order version, it is asserted that there are no non-recursive functions. This still restricts the space of functions while not constituting a function choice axiom.

A related statement is that any decidable subset of naturals cannot ruled out to be computable in the sense that

[math]\displaystyle{ \big(\forall x\ \chi(x)\lor\neg\chi(x)\big)\; \to\; \neg\neg\exists e\,\big(\forall x\, \big(\exists w \; T_1(e, x, w)\big) \leftrightarrow \chi(x)\big) }[/math]

The contrapositive of this puts any non-computable predicate in violation to excluded middle, so this is still generally anti-classical. Unlike [math]\displaystyle{ \mathrm {CT}_0 }[/math], as a principle this is compatible with formulations of the fan theorem.

Variants for related premises [math]\displaystyle{ \forall x\ \psi_\mathrm{left}(x)\lor \psi_\mathrm{right}(x) }[/math] may be defined. E.g. a principle always granting existence of a total recursive function [math]\displaystyle{ {\mathbb N}\to\{\mathrm{left},\mathrm{right}\} }[/math] into some discrete binary set that validates one of the disjuncts. Without the double negation, this may be denoted [math]\displaystyle{ \mathrm {CT}_0^\lor }[/math].

Relationship to classical logic

The schema [math]\displaystyle{ {\mathrm{CT}}_0 }[/math], when added to constructive systems such as [math]\displaystyle{ {\mathsf{HA}} }[/math], 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 slightly more detail: In sufficiently strong systems, such as [math]\displaystyle{ {\mathsf{HA}} }[/math], it is possible to express the relation [math]\displaystyle{ h }[/math] associated with the halting question, relating any code from an enumeration of Turing machines and values from [math]\displaystyle{ \{0,1\} }[/math]. Assuming the classical tautology above, this relation can be proven total, i.e. it constitutes a function that returns [math]\displaystyle{ 1 }[/math] if the machine halts and [math]\displaystyle{ 0 }[/math] if it does not halt. But [math]\displaystyle{ {\mathsf{HA}} }[/math] plus [math]\displaystyle{ {\mathrm{CT}}_0 }[/math] disproves this consequence of the law of the excluded middle, for example. 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 [math]\displaystyle{ {\mathrm{CT}} }[/math] with [math]\displaystyle{ \forall f }[/math] above is consistent with some weak classical systems that do not have the strength to form functions such as the function of the previous paragraph. For example, the classical weak second-order arithmetic [math]\displaystyle{ {\mathsf{RCA_0}} }[/math] is consistent with this single axiom, because [math]\displaystyle{ {\mathsf{RCA_0}} }[/math] 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 [math]\displaystyle{ h }[/math]. E.g., adoption of variants of countable choice, such as unique choice for the numerical quantifiers,

[math]\displaystyle{ \forall n\;\exists! m\;\phi(n, m)\to \exists a\;\forall k\;\phi(k, a_k), }[/math]

where [math]\displaystyle{ a }[/math] denotes a sequence, spoil this consistency.

The first-order formulation [math]\displaystyle{ {\mathrm{CT}}_0 }[/math] already subsumes the power of such a function comprehension principle via enumerated functions.

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

Realizers and metalogic

This above thesis can be characterized as saying that a sentence is true iff it is computably realisable. This is captured by the following metatheoretic equivalences:

[math]\displaystyle{ {\mathsf{HA}} + {\mathrm{ECT_0}} \vdash \varphi \leftrightarrow \exists n \, (n \Vdash \varphi) }[/math]

and

[math]\displaystyle{ {\mathsf{HA}} + {\mathrm{ECT_0}} \vdash \varphi \;\iff\; {\mathsf{HA}} \vdash \exists n \, (n \Vdash \varphi) }[/math]

Here "[math]\displaystyle{ \leftrightarrow }[/math]" is just the equivalence in the arithmetic theory, while "[math]\displaystyle{ \iff }[/math]" denotes the metatheoretical equivalence. For given [math]\displaystyle{ \varphi }[/math], the predicate [math]\displaystyle{ n \Vdash \varphi }[/math] is read as "[math]\displaystyle{ n \text{ realises } \varphi }[/math]". In words, the first result above states that it is provable in [math]\displaystyle{ {\mathsf{HA}} }[/math] plus [math]\displaystyle{ {\mathrm{ECT_0}} }[/math] that a sentence is true iff it is realisable. But also, the second result above states that [math]\displaystyle{ \varphi }[/math] is provable in [math]\displaystyle{ {\mathsf{HA}} }[/math] plus [math]\displaystyle{ {\mathrm{ECT_0}} }[/math] iff [math]\displaystyle{ \varphi }[/math] is provably realisable in just [math]\displaystyle{ {\mathsf{HA}} }[/math].

For the next metalogical theorem, recall that [math]\displaystyle{ {\mathsf{PA}} }[/math] is non-constructive and lacks then existence property, whereas Heyting arithmetic exhibits it:

[math]\displaystyle{ {\mathsf{HA}}\vdash\exists n.\phi(n)\implies\text{exists}\;{\mathrm n}\ {\mathsf{HA}}\vdash\phi({\underline{\mathrm n}}) }[/math]

The second equivalence above can be extended with [math]\displaystyle{ {\mathrm{MP}} }[/math] as follows:

[math]\displaystyle{ {\mathsf{HA}} + {\mathrm{ECT_0}} + {\mathrm{MP}} \vdash \varphi \;\iff\; \text{exists}\; {\mathrm n}\ {\mathsf{PA}} \vdash ({\underline{\mathrm n}} \Vdash \varphi) }[/math]

The existential quantifier needs to be outside [math]\displaystyle{ {\mathsf{PA}} }[/math] in this case. In words, [math]\displaystyle{ \varphi }[/math] is provable in [math]\displaystyle{ {\mathsf{HA}} }[/math] plus [math]\displaystyle{ {\mathrm{ECT_0}} }[/math] as well as [math]\displaystyle{ {\mathrm{MP}} }[/math] iff one can metatheoretically establish that there is some number [math]\displaystyle{ {\mathrm n} }[/math] such that the corresponding standard numeral in [math]\displaystyle{ {\mathsf{PA}} }[/math], denoted [math]\displaystyle{ {\underline{\mathrm n}} }[/math], provably realises [math]\displaystyle{ \varphi }[/math]. Assuming [math]\displaystyle{ {\mathrm{MP}} }[/math] together with alternative variants of Church's thesis, more such metalogical existence statements have been obtained.

See also

• Computable function
• Disjunction and existence properties
• Realizability

References

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