Game of grounds

TL;DR

The paper addresses bridging Prawitz's theory of grounds (ToG) with Girard's Ludics to enable a dialogical reading of grounding and deduction. It first compares the philosophical underpinnings and then provides an indicative formal translation of the implicational fragment, treating types as behaviours $G^A$ and grounds as dagger-free elements of $|G^A|$, with ground-derivations realized through interaction-closures $|A\rightarrow B|$. It also revisits Cozzo's ground-candidates, arguing that Ludics' notion of behaviours and incarnation can capture pseudo-grounds and their epistemic status, thereby addressing limitations of ToG. The work suggests that canonic grounds in ToG correspond to material designs in Ludics, while pseudo-grounds map to elements of a behaviour, enhancing the dialogical and computational interpretation of deduction. Overall, the paper proposes a promising, though preliminary, framework for unifying evidence-based grounding with interaction-based proof semantics, with further work needed to extend beyond the implicational fragment and to formalize intuitionistic modalities.

Abstract

In this paper, we propose to connect Prawitz's theory of grounds with Girard's Ludics. This connection is carried out on two levels. On a more philosophical one, we highlight some differences between Prawitz's and Girard's approaches, but we also argue that they share some basic ideas about proofs and deduction. On a more formal one, we sketch an indicative translation of Prawitz's theory grounds into Girard's Ludics relative to the implicational fragment of propositional intuitionistic logic. This may allow for a dialogical reading of Prawitz's ground-theoretic approach. Moreover, it becomes possible to provide a formal definition of a notion of ground-candidate introduced by Cozzo.