11/05/1989. Exposé de Daniel Lacombe (logique mathématique)

Professeur à l'Université Paris VII

Le théorème de Gödel peut-il aider à penser les limites de l'informatique ?

cf. "Le problème du fondement depuis Gödel", in "Les études philosophiques", oct-déc 1969.

Comment construit-on un modèle mathématique ? On découpe un ensemble d'éléments D. extraits du monde. On définit une structure S (en général préexistante) et on essaie d'établir une correspondance entre S et D. Tout ce qu'on fera ensuit sera valide dans les limites de l'adéquation de cette correspondance. S peut avoir des indéterminations qu'on précise par des observations en D : ça fonctionne tant que ça marche, jamais indéfiniment, si on observe quelque chose qui ne marche pas :

- en général on est content parce qu'on découvre quelque chose, une propriété inconnue ;
- ou bien c'est tellement étonnant qu'on change le découpage, supposé mal construit ;
- ou bien on change la structure.

L'adéquation entre S et D ne se démontre pars : on ne peut qu'en donner des arguments.

Ne pas confondre les mathématiques avec la méta-mathématique : la formalisation, c'est remplacer une formulation méta-mathématique (démonstration) par un objet mathématique (formulation combinatoire). Frege a cherché une langue universelle ; son application la plus simple aurait été en mathématique : mais toute tentative en ce sens a échoué (cf. théorie des ensembles).

Hilbert posé le problème de façon non mathématique. Etant donnée une équation à X inconnues, avec des coefficients >0 et <0, existe-t-il des entiers N qui vérifient cette équation ? Existe-t-il un algorithme qui permette de trouver X,Y,Z... ? Il pensait que "oui", on a découvert que "non" ; si c'est oui, on trouve la solution, on donne la démonstration (ce que tout mathématicien sait reconnaître); si c'est non, le calcul est infini : c'est indécidable, on a donc besoin de la formalisation.

Le premier théorème d'incomplétude de Gödel : il existe une (donc une infinité de) formule(s) indécidable(s). Il ne faut pas confondre : Gödel ne dit pas qu'une théorie est incapable d'exprimer la non-contradiction de cette théorie, mais de la démontrer. C'est tout autre chose.

Le théorème de Gödel fut un rude coup pour les hilbertiens attardés qui pendaient que tout ce qui est énonçable était démontrable ou réfutable. Mais il a été utilisé à tort contre les systèmes formels : un système formel est fait pour formalise une pratique démonstrative, mais n'est jamais universel. Le théorème de Gödel n'a jamais remis en cause S ou D.

Ceci reste vrai sur le plan théorique car si on regarde les choses de façon concrète, on ne peut plus considérer qu'une toute petite sous-classe de problèmes démontrables. Par exemple, pour les polygones, la progression des temps-machine et des volumes-mémoire est exponentielle avec le nombre de variables.

La méthamathématique se développant, le système formel doit toujours se développer, disent les critiques du formalisme ; c'est faux, pour DL, si on considère l'arithmétique de Péano (P), la théorie des types (T), la théorie des ensembles (Z), chacune englobant la précédente, dans un système de plus en plus puissant. Or les mathématiciens ne savent même pas utiliser toute la puissance de P, encore moins celle de T que seuls les logiciens ont exploitée. C'est plus intéressant de se limiter au système restreint et de regarder vraiment comment ça fonctionne.

Pour aborder les limites de l'informatique, réintégrer les limites du temps-machine ou du volume-mémoire : obligés de tenir compte des limites physiques, les informaticiens sont plus réducteurs que les hilbertiens attardés.

Compte-rendu rédigé par C. Hoffsaes