Évènement

Pablo Donato
Istituto Grothendieck
https://www.lix.polytechnique.fr/Labo/Pablo.DONATO/

Date(s) : 27/02/2025   iCal
11h00 - 12h30

Traditionnellement, la théorie de la démonstration s’est établie comme une
branche de la logique symbolique: elle incarne par excellence l’idéal
hilbertien selon lequel tout concept mathématique peut être representé comme
une suite finie de symboles, le raisonnement se réduisant alors à la
manipulation séquentielle de ces symboles. Toutefois plusieurs évolutions
récentes tendent à démontrer qu’une analyse plus fine de la structure des
démonstrations est possible à l’aide de représentations graphiques ou
diagrammatiques : on peut citer les réseaux de preuves de Girard en logique
linéaire, les diagrammes de cordes en logique catégorique, ou encore les
combinatorial proofs de Hughes. L’idée est de s’abstraire de la séquentialité
arbitraire forcée par les symboles, en plongeant les preuves dans l’espace pour
mieux comprendre leur géométrie. Toutefois ces recherches se concentrent
essentiellement sur la structure des démonstrations terminées, en oubliant le
processus de manipulation séquentiel qui a permis leur construction. Cela pose
un obstacle à l’application de ces nouvelles méthodologies à la preuve assistée
par ordinateur, qui repose fondamentalement sur la manipulation de
démonstrations partielles.

Pour résoudre ce problème, nous explorons un formalisme diagrammatique oublié
des logiciens contemporains, probablement car il prédate l’existence de la
théorie de la démonstration : les graphes existentiels de C. S. Peirce.
Celui-ci repose sur une représentation purement diagrammatique et topologique
des constantes logiques telles que la conjonction, la négation et l’existence,
inspirée d’une compréhension dialogique du raisonnement un siècle avant
l’avènement de la sémantique des jeux. La démonstration est alors comprise
comme un processus dynamique de construction d’énoncés valides par réécriture
de graphes, à l’aide de quatre règles d’inférence élémentaires par insertions
et omissions de graphes arbitraires.

Nous commencerons par une présentation informelle des systèmes Alpha et Beta de
graphes existentiels pour la logique classique propositionnelle et du premier
ordre, tels qu’introduits par Peirce en 1896. Puis, motivés par notre objectif
d’application aux assistants de preuve, nous concevons le calcul floral, une
variante intuitionniste de Beta basée sur la notion de lieur où les graphes
apparaissent métaphoriquement sous forme de fleurs. Pour modéliser plus
fidèlement le processus de recherche de preuve « en arrière », nous inversons le
sens de lecture des règles d’inférence, ce qui nous permet d’identifier un
fragment analytique et entièrement réversible de règles via une sémantique de
préfaisceaux (structures de Kripke). Forts de ces avancées, nous nous éloignons
de la conception relationnelle de Peirce pour partir à la recherche d’une
interprétation computationnelle du calcul floral dans le style
fonctionnel/BHK/Curry-Howard. Nous finirons l’exposé par une esquisse du
nouveau territoire ainsi approché et baptisé « théorie des topes », au sein
duquel la distinction entre un terme et son type se trouve mise en défaut.

Emplacement
I2M Luminy - TPR2, Salle de Séminaire 304-306 (3ème étage)

Catégories

• Séminaire