Game of grounds

TL;DR

This paper explores the connection between Prawitz's theory of grounds and Girard's Ludics, offering philosophical insights and a formal translation that enables a dialogical interpretation of proof grounds.

Contribution

It introduces a formal translation of Prawitz's grounds into Girard's Ludics for the implicational fragment, bridging philosophical and formal aspects.

Findings

Identifies philosophical similarities and differences between Prawitz and Girard.

Provides a formal translation framework for grounds in Ludics.

Enables a dialogical reading of ground-theoretic approaches.

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.