Théorie de la démonstration et informatique : de l’ingénierie typographique à la géometrie

Yves Lafont

Qu’est-ce qu’une preuve ? Est-ce un nombre (Gödel), un texte (Hilbert), ou encore un arbre (Gentzen) ?

• Les nombres sont des objets mathématiques anciens et respectables, mais l’énumération de Gödel est arbitraire. C’est seulement un outil pour la démonstration du théorème d’imcomplétude.

• Les textes sont plus proches de la réalité matérielle des preuves mathématiques, mais ce sont plutt des objets typographiques que des objets mathématiques. De plus, il y a beaucoup de choix arbitraires dans la représentation textuelle.

• Les arbres font mieux apparatre la structure des preuves, et cette représentation est d’ailleurs utilisée par les systèmes de recherche interactive de preuves, mais les arbres ne sont toujours pas les bons objets !

La logique linéaire propose un point de vue plus géométrique, avec la notion de réseau de preuve et ses avatars, les réseaux d’interaction et la géométrie de l’interaction. Dans un domaine apparenté, à savoir le calcul symbolique et la réécriture, on voit aussi apparatre des notions géométriques telles que les diagrammes de Penrose et les invariants homologiques. Une symbiose entre la logique et la géométrie pourrait devenir aussi fructueuse que celle qui existe déjà entre l’algèbre et la géométrie.

Address: CNRS - INSTITUT DE MATHEMATIQUES DE LUMINY 163 avenue de Luminy, Case 907, 13288 Marseille Cedex 9

E-mail: lafont@iml.univ-mrs.fr