A Game Model for Proofs with Costs

Abstract

We look at substructural calculi from a game semantic point of view, guided by certain intuitions about resource conscious and, more specifically, cost conscious reasoning. To this aim, we start with a game, where player defends a claim corresponding to a (single-conclusion) sequent, while player tries to refute that claim. Branching rules for additive connectives are modeled by choices of, while branching for multiplicative connectives leads to splitting the game into parallel subgames, all of which have to be won by player to succeed. The game comes into full swing by adding cost labels to assumptions, and a corresponding budget. Different proofs of the same end-sequent are interpreted as more or less expensive strategies for to defend the corresponding claim. This leads to a new kind of labelled calculus, which can be seen as a fragment of (subexponential linear logic). Finally, we generalize the concept of costs in proofs by using a semiring structure, illustrate our interpretation by examples and investigate some proof-theoretical properties.