Proof nets, rings, and ideals
William Troiani
LIPN, Université Sorbonne Paris Nord
https://williamtroiani.github.io/
Date(s) : 24/03/2022 iCal
11h00 - 12h30
What is cut elimination? When Gentzen wrote down the rewriting processes associated with his logical systems, what seemingly external mathematical structure was he also encapsulating? This question is at the heart of Girard’s Geometry of Interaction program. The recent work of Daniel Murfet and myself have laid down the foundations for a new approach to Girard’s idea, where proofs (here, MLL proof structures) are interpreted as suitable quotients of polynomial rings, where the number of variables depends on the size of the formulas of the proof, and the quotient ideal depends on the links of the proof. Cut elimination is then interpreted as suitable isomorphisms between these rings. Moreover, elimination theory can be used to give an interpretation of “plugging” of formulas. This is the first work of a series of papers which will eventually give models of various fragments of linear logic inside a category of quantum error correction codes, and later, more exotic algebraic-geometric settings. Our current target is a model inside the bicategory of Landau-Ginzburg models.
L’exposé sera retransmis ici : https://greenlight.lal.cloud.math.cnrs.fr/b/lio-hdc-jef
Emplacement
I2M Luminy - Ancienne BU, Salle Séminaire2 (RdC)
Catégories
