pith. sign in

arxiv: 1906.11742 · v1 · pith:AC7MEUTMnew · submitted 2019-06-27 · 💻 cs.LO

A Game Model for Proofs with Costs

Timo Lang , Carlos Olarte , Elaine Pimentel , Christian Fermuller This is my paper

Pith reviewed 2026-05-25 14:06 UTC · model grok-4.3

classification 💻 cs.LO
keywords game semanticssubstructural logicproof costslabelled calculussubexponential linear logicsemiring costssequent calculusresource conscious reasoning
0
0 comments X

The pith

Different proofs of the same sequent are strategies of different costs for player I defending the claim with a budget against player II.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper models substructural calculi as games where player I defends a single-conclusion sequent claim and player II tries to refute it. Additive connectives are modeled by choices made by II, while multiplicative connectives split the game into parallel subgames that I must all win. Adding cost labels to assumptions and a budget for I turns different proofs into more or less expensive winning strategies. This yields a labelled sequent calculus viewed as a fragment of subexponential linear logic, which is then generalized by replacing numeric costs with semiring operations.

Core claim

Different proofs of the same end-sequent are interpreted as more or less expensive strategies for player I to defend the corresponding 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 is extended by adding cost labels to assumptions and a corresponding budget. This leads to a new kind of labelled calculus, which can be seen as a fragment of SELL. Costs are generalized using a semiring structure.

What carries the argument

The cost-labelled game in which proofs correspond to winning strategies for player I within a given budget, with parallel subgames required for multiplicative rules.

If this is right

  • Proofs of one sequent can be ranked by the minimal cost of a winning strategy for I.
  • A labelled sequent calculus is obtained that explicitly tracks costs during derivation.
  • The model extends to semiring-valued costs for abstract resource accounting beyond numbers.
  • Proof-theoretical properties of the resulting labelled calculus can be investigated directly.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Proof search procedures could be guided to prefer low-cost winning strategies when several proofs exist.
  • The same game construction might be adapted to other resource-sensitive logics by defining costs for their connectives.
  • Quantifying proof expense this way could connect to optimization problems in automated reasoning systems.

Load-bearing premise

The game rules for costs and budgets correctly capture the semantics of additive and multiplicative connectives without breaking the correspondence to valid proofs in the underlying substructural calculus.

What would settle it

A specific sequent together with a cost assignment and budget where the existence of a winning strategy for I in the game does not match the existence of a valid proof in the substructural calculus.

Figures

Figures reproduced from arXiv: 1906.11742 by Carlos Olarte, Christian Fermuller, Elaine Pimentel, Timo Lang.

Figure 1
Figure 1. Figure 1: Sequent systems C and C(R +) 5, the challenge of extending the semantics to full subexponential linear logic is discussed. Section 6 concludes the paper. 2 A game model of branching Our starting point is a calculus for affine intuitionistic linear logic without ex￾ponentials (aIMALL) [11], whose calculus is also equivalent to FLew, the Full Lambek calculus with exchange and weakening. We denote this calcul… view at source ↗
Figure 2
Figure 2. Figure 2: Our aim is to prove that |=GC(R+) ({Γ −→ A}, b) iff ⊢Cℓ(R+) Γ −→b A. To this end, we need an analogue of Lemma 4 (independency of subgames in GC) for GC(R +). Note that crucially, the naive analogue |=GC(R+) ({S1, . . . , Sn}, b) iff for all i ≤ n, |=GC(R+) ({Si}, b) [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 2
Figure 2. Figure 2: The labelled sequent system C ℓ (R +) does not hold: Having a w.s. in ({S1, . . . , Sn}, b) is not the same as having w.s.’s in all ({Si}, b)’s, since the budget b is shared between the subgames in GC(R +). However, one can prove that there are strategies in GC(R +) which are independent up to a partition of the budget. More precisely, Lemma 11 (Quasi-independency of subgames in GC(R +)). |=GC(R+) ({S1, . … view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper develops a game-semantic model for single-conclusion substructural sequent calculi in which Player I defends a claim against Player II. Additive branching is interpreted as II's choice and multiplicative branching as parallel subgames that I must all win. Costs are attached to assumptions together with a budget; different proofs of the same sequent become strategies of different expense. The resulting labelled calculus is presented as a fragment of SELL and is further generalized by replacing numeric costs with semiring values. Examples are given and selected proof-theoretic properties are investigated.

Significance. If the correspondence between the game rules and the underlying substructural calculus is preserved under the addition of costs and budgets, the construction supplies a concrete, resource-sensitive interpretation of proofs that directly links game semantics with subexponential linear logic. The semiring generalization widens the framework to arbitrary cost structures while retaining the same game rules, which could be useful for complexity analyses or for modelling different notions of resource.

major comments (2)
  1. [Abstract / game definition and labelled calculus] The central claim that the labelled calculus is a fragment of SELL (and that the semiring version preserves the correspondence) rests on the assertion that the game rules correctly capture the semantics of the additive and multiplicative connectives once costs and budgets are added. No explicit embedding, soundness/completeness argument, or reduction to the unlabelled calculus is referenced in the abstract or described in sufficient detail to verify that the weakest assumption holds.
  2. [Abstract / examples] The manuscript states that different proofs become strategies of varying expense and that the construction yields a new labelled calculus. Without a concrete example showing how a specific sequent, its proofs, and the corresponding game plays with budgets are represented in the labelled system, it is impossible to check that the cost assignment is faithful to the game semantics.
minor comments (2)
  1. Notation for cost labels, budgets, and the semiring operations should be introduced with explicit definitions before the game rules are stated.
  2. The abstract mentions investigation of proof-theoretic properties; a short list of the properties proved (cut-elimination, admissibility of weakening, etc.) would help the reader assess the scope of the results.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments on our manuscript. Below we respond point by point to the major comments and indicate the revisions we will make.

read point-by-point responses

  1. Referee: [Abstract / game definition and labelled calculus] The central claim that the labelled calculus is a fragment of SELL (and that the semiring version preserves the correspondence) rests on the assertion that the game rules correctly capture the semantics of the additive and multiplicative connectives once costs and budgets are added. No explicit embedding, soundness/completeness argument, or reduction to the unlabelled calculus is referenced in the abstract or described in sufficient detail to verify that the weakest assumption holds.

    Authors: The game rules are introduced so that additive branching corresponds exactly to Player II's choice and multiplicative branching to parallel subgames that Player I must all win; costs and budgets are attached directly to assumptions and game positions. The labelled calculus is obtained by annotating sequents with the cost and budget information arising from these positions, and the fragment-of-SELL claim follows by matching the resulting rules to the subexponential rules that govern the cost labels. We agree, however, that the abstract and the surrounding exposition would benefit from an explicit embedding statement together with a self-contained soundness and completeness argument (including the reduction to the unlabelled case). We will add a dedicated subsection that states the embedding, proves soundness and completeness with respect to the game semantics, and records the reduction to the cost-free calculus. revision: yes

  2. Referee: [Abstract / examples] The manuscript states that different proofs become strategies of varying expense and that the construction yields a new labelled calculus. Without a concrete example showing how a specific sequent, its proofs, and the corresponding game plays with budgets are represented in the labelled system, it is impossible to check that the cost assignment is faithful to the game semantics.

    Authors: The paper already contains illustrative examples, yet we accept that they do not supply a complete end-to-end trace of one sequent through its proofs, the associated game plays (including budget updates), and the resulting labelled derivations. We will expand the examples section with a fully worked sequent that exhibits multiple proofs of different expense, records the corresponding game strategies and budget consumption, and shows the direct translation into the labelled calculus. revision: yes

Circularity Check

0 steps flagged

No significant circularity; construction is self-contained

full rationale

The paper defines a game interpretation for substructural sequents by assigning costs and budgets to assumptions, then explicitly constructs a labelled calculus whose rules mirror the game moves for additive and multiplicative branching. This labelled system is observed to be a fragment of SELL, but the derivation proceeds by direct translation of the game rules rather than by fitting parameters, renaming prior results, or relying on a load-bearing self-citation whose content is itself unverified. No equation or step reduces by construction to its own input; the semiring generalization is likewise introduced as an explicit extension. The central correspondence between proofs and strategies is therefore an independent definitional extension of existing game-semantic ideas.

Axiom & Free-Parameter Ledger

0 free parameters · 3 axioms · 0 invented entities

The model rests on domain assumptions from game semantics for linear logic and the algebraic properties of semirings. No free parameters or invented entities with independent evidence are described in the abstract.

axioms (3)
  • domain assumption Branching rules for additive connectives are modeled by choices of player II and for multiplicative connectives by splitting into parallel subgames all won by player I.
    Invoked when defining the base game before adding costs.
  • domain assumption Cost labels on assumptions and a corresponding budget can be added while preserving the game-to-proof correspondence.
    Central premise enabling the labelled calculus.
  • domain assumption Costs can be generalized using a semiring structure.
    Used to extend the cost model beyond specific numeric values.

pith-pipeline@v0.9.0 · 5712 in / 1385 out tokens · 38727 ms · 2026-05-25T14:06:38.755921+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

25 extracted references · 25 canonical work pages

  1. [1]

    Games and full comp leteness for mul- tiplicative linear logic

    Samson Abramsky and Radha Jagadeesan. Games and full comp leteness for mul- tiplicative linear logic. J. Symb. Log. , 59(2):543–574, 1994

    work page 1994

  2. [2]

    Tight typ- ings and split bounds

    Beniamino Accattoli, St´ ephane Graham-Lengrand, and De lia Kesner. Tight typ- ings and split bounds. PACMPL, 2(ICFP):94:1–94:30, 2018. Derivations with Costs 17

    work page 2018

  3. [3]

    Enhancing constr aints manipulation in semiring-based formalisms

    Stefano Bistarelli and Fabio Gadducci. Enhancing constr aints manipulation in semiring-based formalisms. In Gerhard Brewka, Silvia Cora deschi, Anna Perini, and Paolo Traverso, editors, ECAI 2006, 17th European Conference on Artificial Intelligence, Including Prestigious Applications of Inte lligent Systems (PAIS 2006), Proceedings, volume 141 of Frontiers...

    work page 2006

  4. [4]

    Semiring-based csps and val ued csps: Frameworks, properties, and comparison

    Stefano Bistarelli, Ugo Montanari, Francesca Rossi, Tho mas Schiex, G´ erard Ver- faillie, and H´ el` ene Fargier. Semiring-based csps and val ued csps: Frameworks, properties, and comparison. Constraints, 4(3):199–240, 1999

    work page 1999

  5. [5]

    A game semantics for linear logic

    Andreas Blass. A game semantics for linear logic. Ann. Pure Appl. Logic , 56(1- 3):183–220, 1992

    work page 1992

  6. [6]

    Some semantical aspects of linear logic

    Andreas Blass. Some semantical aspects of linear logic. Logic Journal of the IGPL , 5(4):487–503, 1997

    work page 1997

  7. [7]

    The structure of ex- ponentials: Uncovering the dynamics of linear logic proofs

    Vincent Danos, Jean-Baptiste Joinet, and Harold Schelli nx. The structure of ex- ponentials: Uncovering the dynamics of linear logic proofs . In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors, Kurt G¨ odel Colloquium, volume 713 of Lecture Notes in Computer Science , pages 159–171. Springer, 1993

    work page 1993

  8. [8]

    Proof an d refutation in MALL as a game

    Olivier Delande, Dale Miller, and Alexis Saurin. Proof an d refutation in MALL as a game. Ann. Pure Appl. Logic , 161(5):654–672, 2010

    work page 2010

  9. [9]

    Simmons, and Iliano Cervesato

    Yuxin Deng, Robert J. Simmons, and Iliano Cervesato. Rela ting reasoning method- ologies in linear logic and process algebra. Mathematical Structures in Computer Science, 26(5):868–906, 2016

    work page 2016

  10. [10]

    Ferm¨ uller and Timo Lang

    Christian G. Ferm¨ uller and Timo Lang. Interpreting sequent calculi as client-server games. In Renate A. Schmidt and Cl´ audia Nalon, editors, Automated Reason- ing with Analytic Tableaux and Related Methods - 26th Intern ational Conference, TABLEAUX 2017, Bras ´ ılia, Brazil, September 25-28, 2017, P roceedings, volume 10501 of Lecture Notes in Computer...

    work page 2017

  11. [11]

    Linear logic

    Jean-Yves Girard. Linear logic. Theor. Comput. Sci. , 50:1–102, 1987

    work page 1987

  12. [12]

    Hyland and C

    J.M.E. Hyland and C. h. L. Ong. Fair games and full complet eness for multiplica- tive linear logic without the mix-rule, 1993

    work page 1993

  13. [13]

    A constructive game semantics for the language of linear logic

    Giorgi Japaridze. A constructive game semantics for the language of linear logic. Ann. Pure Appl. Logic , 85(2):87–156, 1997

    work page 1997

  14. [14]

    Games semantics for full propositi onal linear logic

    Fran¸ cois Lamarche. Games semantics for full propositi onal linear logic. In Pro- ceedings, 10th Annual IEEE Symposium on Logic in Computer Sc ience, San Diego, California, USA, June 26-29, 1995 , pages 464–473. IEEE Computer Society, 1995

    work page 1995

  15. [15]

    Logik und agon

    Paul Lorenzen. Logik und agon. Atti Del XII Congresso Internazionale di Filosofia , 4:187–194, 1960

    work page 1960

  16. [16]

    Asynchronous games 4: A fully com plete model of proposi- tional linear logic

    Paul-Andr´ e Melli` es. Asynchronous games 4: A fully com plete model of proposi- tional linear logic. In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings , pages 386–395. IEEE Computer Society, 2005

    work page 2005

  17. [17]

    The pi-calculus as a theory in linear logic: Preliminary results

    Dale Miller. The pi-calculus as a theory in linear logic: Preliminary results. In Evelina Lamma and Paola Mello, editors, Extensions of Logic Programming, Third International Workshop, ELP’92, Bologna, Italy, February 26-28, 1992, Proceed- ings, volume 660 of Lecture Notes in Computer Science , pages 242–264. Springer, 1992

    work page 1992

  18. [18]

    Algorithmic specifications in linear logic with subex- ponentials

    Vivek Nigam and Dale Miller. Algorithmic specifications in linear logic with subex- ponentials. In Ant´ onio Porto and Francisco Javier L´ opez-Fraguas, editors, PPDP, pages 129–140. ACM, 2009

    work page 2009

  19. [19]

    Paradoxes and s tructural rules from a dialogue perspective

    Catarina Dutilh Novaes and Rohan French. Paradoxes and s tructural rules from a dialogue perspective. Philosophical Issues , 28:129–158, 2018. 18 Lang, Olarte, Pimentel and Ferm¨ uller

    work page 2018

  20. [20]

    A proof theoretic study of soft concurrent constraint programming

    Elaine Pimentel, Carlos Olarte, and Vivek Nigam. A proof theoretic study of soft concurrent constraint programming. TPLP, 14(4-5):649–663, 2014

    work page 2014

  21. [21]

    MELL in the calculus of structures

    Lutz Straßburger. MELL in the calculus of structures. Theor. Comput. Sci. , 309(1- 3):213–285, 2003

    work page 2003

  22. [22]

    worse costs

    Lutz Straßburger and Alessio Guglielmi. A system of inte raction and structure IV: the exponentials and decomposition. ACM Trans. Comput. Log. , 12(4):23:1–23:39, 2011. Derivations with Costs 19 A Appendix A.1 Cut elimination for CP ℓ(K) Consider the labelled sequent system CP ℓ(K) built from Cℓ(K) (see Def. 20) by dropping the restriction on occurrences ...

    work page 2011

  23. [23]

    ab +E cd = a + b + c + d

    work page

  24. [24]

    ab ≥ E ac (i.e., the ordering ≥ E ignores the subindices)

    work page

  25. [25]

    extra cost

    ab >E cd iff a > c . For any formula F ∈ CP ℓ(K), we define [F ]c as the formula that substitutes any modality ▼ab with ▼ab+c. Hence CP ℓ(K) can be slightly modified so that sequent labels belong to R∞ + , while modal labels belong to E. Due to the ordering above, the promotion of ▼a0 has the same effect/constraints that the promotion of ▼ab. However, the der...

    work page