In a recent work, we looked at substructural calculi from a game semantic point of view, guided by certain intuitions about resource conscious and, more specifically, cost conscious reasoning. This culminated in labelled extensions of (intuitionistic, affine) linear logic with multimodalities (subexponentials), which allowed for an elegant interpretation of the dereliction rule. In this talk, I will talk about the proof theoretical effect of costs in the cut-elimination process.
This is a joint work with Timo Land, Carlos Olarte and Chris Fermüller