# A Game Model for Proofs with Costs

## TL;DR

This paper introduces a game-theoretic framework for resource-aware and cost-sensitive proof systems, modeling proofs as strategies with associated costs using labelled calculi and semiring structures.

## Contribution

It develops a novel game semantics for substructural logics incorporating costs, leading to a new labelled calculus and generalizing proof costs via semirings.

## Key findings

- Proofs are interpreted as costed strategies in a game setting.
- A new labelled calculus for cost-aware proofs is introduced.
- The framework is exemplified and some proof-theoretical properties are analyzed.

## 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 I defends a claim corresponding to a (single-conclusion) sequent, while player II tries to refute that claim. Branching rules for additive connectives are modeled by choices of II, while branching for multiplicative connectives leads to splitting the game into parallel subgames, all of which have to be won by player I 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 I to defend the corresponding claim. This leads to a new kind of labelled calculus, which can be seen as a fragment of SELL (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.