Seminaire Philmath du 18 avril 2023
Mardi 18 avril 2023, 14h-16h, salle des conférences de l’IHPST, 13, rue du Four, 75006 PARIS
Titre : What is the cost of cut?
Various kinds of game semantics have been introduced to characterize computational features of substructural logics, in particular fragments and variants of linear logic (LL). Our particular view of game semantics is that it is not just a technical tool for characterizing provability in certain calculi, but rather a playground for illuminating specific semantic intuitions underlying certain proof systems. Especially, we aim at a better understanding of resource conscious reasoning, which is often cited as a motivation for substructural logics. In this talk, we will look at substructural calculi from a game semantic point of view, guided by certain intuitions about resource conscious and, more specifically, cost conscious reasoning. In particular, we will show a game where cost labels are added to assumptions, and games are played under the correspondent budget. This will lead to a new kind of labelled calculus, which can be seen as a fragment of subexponential linear logic, and allows for an elegant interpretation of the dereliction rule. We will show, using examples, how this concept of costs in proofs can be generalised by using a semiring structure. We will finish with a discussion on the proof theoretical effect of costs in the cut-elimination process.
This is a joint work with Timo Lang, Carlos Olarte and Chris Fehrmuller.
Lien Zoom : https://pantheonsorbonne.zoom.us/j/93958699353?pwd=YnBMSjIzaFg5VGxGSUR3OE1pcys5QT09
ID réunion : 939 5869 9353
Passcode : 436868