![]() |
Philosophe
et mathématicien, professeur dans de nombreuses universités américaines
dont Princeton et Los Angeles, Alonzo Church étudia à Princeton et se pencha sur les
fondements des mathématiques : on est à une époque cruciale pour les
mathématiques suite au bouleversement occasionné par la
théorie des ensembles de Cantor et les contradictions qu'elle engendra.
Il obtint son doctorat (Alternatives Zermelo's assumption, 1927) sous la direction d'Oscar Veblen et complète ses études durant deux années à Harvard puis à Göttingen (en Allemagne). Cet éminent logicien compléta les travaux de Gödel relatifs à l'indécidabilité de propositions au sein d'une théorie, voire l'indécidabilité d'une théorie elle-même, en développant les fondements du langage mathématique formel.
Les propositions indécidables : »
Pour ce faire, il développe (1936) une logique basée sur le seul concept de fonction conduisant à construire des algorithmes susceptibles tant de décrire des énoncés mathématiques que de définir des langages de programmation (tels que Lisp en particulier en 1960) : le λ-calcul. Par ce biais il retrouve certaines fonctions et relations récursives baptisées λ-définissables qui s'avérèrent être les fonctions récursives (générales) de Gödel, également dites calculables.
Son élève et compatriote Stephen C. Kleene aboutissait au même résultat par une logique semblable basée sur une autre classe de fonctions dites μ-récursives. Il est aujourd'hui reconnu que le λ-calcul permet de construire tout énoncé mathématique : formules, fonctions, raisonnement.
La notion de fonction récursive en logique et informatique : » » Turing , Skolem
Son approche du langage mathématique est très complexe. Elle touche à ce que Hilbert appela la métamathématique (théorie de la démonstration), avec ce que l'on nomme aujourd'hui la théorie des modèles que développeront Tarski et Robinson dont l'objectif est d'écarter du raisonnement toute contradiction potentielle.
Mais Church a prouvé, en (très) résumé, que pour tout système axiomatique (ZF, ZFC, NGB) pour lequel une démonstration est en cause, on aboutit inéluctablement à l'indécidabilité de cette dernière vis à vis d'un autre. La démonstration absolue, voulue par Hilbert, n'existe pas.
» Zermelo , Bernays , Ackermann
Hypothèse (ou thèse) de Church (1936) : |
Il s'agit du résultat suivant, appelé thèse de Church par Kleene et également avancé par Post :
Les fonctions
numériques formelles (de Np
dans N) effectivement calculables
sont les fonctions récursives (générales)
Les notions de fonction récursive et de fonction calculable en logique et en informatique : »
Théorème de Church (1936) : |
Relatif au problème de la décision posé par Hilbert en 1918 :
Aucune
théorie fondée sur la logique des prédicats du premier ordre ne permet d'exhiber
un algorithme général
permettant
d'établir qu'une formule de la théorie est vraie ou fausse.
➔ Pour en savoir plus :