Proof theory and computer science: from typographical engineering towards geometry

Yves Lafont

What is a proof? Is it a number (Gödel), a text (Hilbert), or a tree (Gentzen)?

• Numbers are old and respectable mathematical objects, but Gödel’s numbering is arbitrary. It is just a tool for the proof of the incompleteness theorem.

• Texts are closer to the material reality of mathematical proofs, but they are more typographical objects than mathematical ones. Furthermore, there are many arbitrary choices in the textual representation.

• The structure of proofs is better shown by trees, and this representation is used indeed by systems for interactive proof search, but trees are still not the good objects !

Linear logic suggests a more geometrical viewpoint, with the notion of proof net and its avatars, interaction nets and geometry of interaction. In a related area, namely symbolic computation and rewriting, geometrical notions also appear, such as Penrose diagrams and homological invariants. A symbiosis between logic and geometry could be as fruitful as the one which already exists between algebra and geometry.

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

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