Game of grounds
Davide Catta, Antonio Piccolomini d'Aragona

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsPhilosophy and Theoretical Science · Logic, programming, and type systems · Historical Philosophy and Science
