
Philosophe
et mathématicien, professeur dans de nombreuses universités américaines
dont Princeton et Los Angeles, Church fut un éminent
logicien qui 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 fit usage de certaines fonctions et relations récursives dite lambda-définissables (1941) conduisant au concept moderne d'un algorithme susceptible tant de décrire des énoncés mathématiques que de définir des langages de programmation.
A noter que son élève, contemporain et compatriote Stephen Cole Kleene (1909-1994), professeur à Princeton et à Madison (université du Wisconin) et précédemment Alan Turing, travaillèrent sur le même sujet et apportèrent d'importants résultats exploités en informatique. On doit aussi à Kleene, partisan du constructivisme, la mise en place d'une logique refusant le tiers exclu.
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.
| Hypothèse de Church : |
Les fonctions numériques formelles (i.e. de N dans N) calculables sont les fonctions récursives
Pour
en savoir plus :