L'identité des preuves : normalisation, réseaux et séparation

Résumé 0

La théorie de la démonstration présente divers systèmes formels de preuve permettant de représenter des démonstrations à l’aide d’objets rigoureusement définis, et dont la manipulation revêt divers intérêts. Nous nous proposons ici d’étudier la question — très débattue — de savoir à quelles conditions deux dérivations de ces systèmes représentent, décrivent, la même démonstration. Nous étudions en particulier deux propositions de réponses, avant de mettre chacune en perspective pour une meilleure compréhension des concepts et appareils sollicités. Ces deux solutions correspondent respectivement à une relation d’équivalence induite par le processus de normalisation des dérivations défini par Gentzen dans les années 1930, et à un quotient par une représentation graphique des dérivations due à Girard (dans les années 1980) que sont les réseaux de preuve.