ChronoMath, une chronologie des MATHÉMATIQUES
à l'usage des professeurs de mathématiques, des étudiants et des élèves des lycées & collèges

CHURCH Alonzo, américain, 1903-1995 

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.

»  Frege , Peano , Turing


    Pour en savoir plus :

  1. ABRÉGÉ D'HISTOIRE DES MATHÉMATIQUES, 1700-1900, Jean Dieudonné, Ch.11, par Marcel Guillaume. Éd. Hermann, Paris, 1978-1992.
  2. Logique mathématique, tome 1 : Calcul propositionnel, algèbre de Boole, calcul des prédicats, théorèmes de complétude
    par René Cori, Daniel Lascar. Éd. Dunod, Paris, 2003
  3. Histoire d'algorithmes : Du caillou à la puce, par une équipe d'enseignants (IREM, IUFM, CNRS).
    Éd. Belin - Collection Regards sur la science - 1993
  4. Le λ-calcul (lambda calcul ) de Church : cours de Jean Betrema : http://www.labri.fr/perso/betrema/MC/MC6.html
  5. Lambda-calcul, un article de Wikipedia : http://fr.wikipedia.org/wiki/Thèse de Church
  6. Hypothèse de Church :
    i/    http://fr.wikipedia.org/wiki/Lambda-calcul
    ii/  Théorèmes de non décidabilité, par D. Lacombe (Séminaire Bourbaki, 1962-64) :
      http://www.numdam.org/article/SB_1962-1964__8__323_0.pdf
  7. La théorie des fonctions récursives et ses applications, par D. Lacombe (Bulletin de la SMF,1960)
    http://archive.numdam.org/article/BSMF_1960__88__393_0.pdf
  8. Algorithmes polynomiaux de classes P et NP et problème de la décision :
    http://www.labri.fr/perso/betrema/MC/MC8.html

Brelot  Delsarte
© Serge Mehl - www.chronomath.com