Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Church's thesis (constructive mathematics)
Résumé
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.
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.