CHURCH ALONZO (1903-1995)

Mathématicien et logicien, philosophe et historien de la logique, Alonzo Church est né le 14 juin 1903 à Washington et mort le 11 août 1995 à Hudson (Ohio). Professeur de mathématiques à l'université de Princeton, directeur du Journal of Symbolic Logic, il est selon Kneale « le plus fidèle des disciples de Frege ». Réputé « platonisant », il défend une conception délibérément réaliste de la proposition. Critique minutieux et exigeant, il apporte une formulation rigoureuse des conditions auxquelles doit satisfaire un critère d'assomption ontologique ; à Quine revient d'avoir ensuite fourni ce critère. Mais Church est surtout connu pour ses travaux sur la décidabilité dans les systèmes formels.

Le symbolisme arithmétique nous permet de formuler des propositions dont on ne peut déterminer la valeur de vérité par aucune technique connue de calcul ou de raisonnement. Ainsi la conjecture de Goldbach, certaines propositions élémentaires de l'arithmétique n'ont jusqu'ici reçu aucune preuve. Pourrait-on imaginer une technique générale pour déterminer la vérité ou la probabilité de ce genre de propositions ? Church démontre par la méthode de diagonalisation qu'il n'en est rien. Non seulement une technique générale est introuvable, mais la supposition de son existence entraînerait une absurdité. En cela, l'arithmétique diffère du calcul propositionnel, décidable par tables de vérité, mais non du calcul des prédicats dans son ensemble. C'est tout le projet qu'avait formé Hilbert d'introduire des démonstrations effectives en mathématiques qui devient irréalisable. Tel est en substance le « théorème de Church » (1936), qu'on ne doit pas confondre avec la « thèse de Church », encore que les deux soient liés.

Pour démontrer son théorème, en effet, l'auteur devait apporter la contrepartie formelle, autant que faire se peut, de la notion intuitive de calculabilité effective. La thèse de Church est constituée par l'affirmation qu'il existe une traduction fidèle en termes de fonctions récursives générales (f.r.g.). Elle consiste à définir la notion de procédé effectif au moyen du concept de récursivité. La théorie des f.r.g. permet d'établir le théorème de Church, ainsi que le théorème de Gödel. La notion de fonction récursive (d'entiers positifs) avait été introduite par Gödel à partir d'une suggestion de Herbrand. S. C. Kleene l'avait analysée en détail ; une fonction est récursive générale si sa valeur pour un argument donné peut être calculée à partir d'un ensemble d'équations au moyen de deux règles seulement : remplacement des variables par des nombres, substitution des identiques. La classe des f.r.g. et la classe des fonctions calculables au sens de Turing, d'une part, et la classe des fonctions définissables au sens de Church, d'autre part, ont même extension. Cela constitue un argument de poids pour la thèse de Church selon laquelle la notion de f.r.g. traduit fidèlement dans le langage mathématique la notion intuitive de fonction calculable. Le statut intuitif de la calculabilité effective exclut toute justification complète de la thèse, mais l'identification que celle-ci opère est très plausible.

Néanmoins, la thèse de Church fut discutée. Elliot Mendelsohn a résumé et critiqué les principales objections dans son article « On Some Recent Criticism of Church's Thesis », in Notre Dame Journal of Formal Logic, vol. IV, 1963, p. 201.

— Françoise ARMENGAUD