Church's thesis (constructive mathematics)

In constructive mathematics, Church's thesis is an axiom 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. is stronger in the sense that with it every function is computable. The constructivist principle is fully formalizable, using formalizations of "function" and "computable" that depend on the theory considered. A common context is recursion theory as established since the 1930's. Adopting as a principle, then for a predicate of the form of a family of existence claims (e.g. below) that is proven not to be validated for all 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 ). 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. The axiom in turn affects ones proof calculus, negating some common classical propositions. The axiom is incompatible with systems that validate total functional value associations and evaluations that are also proven not to be computable. For example, Peano arithmetic is such a system. Concretely, the constructive Heyting arithmetic with the thesis in its first-order formulation, , as an additional axiom is able to disprove 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 . 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. This principle has formalizations in various mathematical frameworks. Let denote Kleene's T predicate, so that e.g. validity of the predicate expresses that is the index of a total computable function.

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related concepts (4)

Realizability

In mathematical logic, realizability is a collection of methods in proof theory used to study constructive proofs and extract additional information from them. Formulas from a formal theory are "realized" by objects, known as "realizers", in a way that knowledge of the realizer gives knowledge about the truth of the formula. There are many variations of realizability; exactly which class of formulas is studied and which objects are realizers differ from one variation to another.

Effective topos

In mathematics, the effective topos introduced by captures the mathematical idea of effectivity within the framework. The topos is based on the partial combinatory algebra given by Kleene's first algebra . In Kleene's notion of recursive realizability, any predicate is assigned realizing numbers, i.e. a subset of . The extremal propositions are and , realized by and . However in general, this process assigns more data to a proposition than just a binary truth value.

Constructive set theory

Axiomatic constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same first-order language with "" and "" of classical set theory is usually used, so this is not to be confused with a constructive types approach. On the other hand, some constructive theories are indeed motivated by their interpretability in type theories. In addition to rejecting the principle of excluded middle (), constructive set theories often require some logical quantifiers in their axioms to be set bounded, motivated by results tied to impredicativity.