Towards an Understanding of Girard's Transcendental Syntax: Syntax by Testing

Abstract

Through his work in ludics and Geometry of Interaction, Jean-Yves Girard invites us to a change of paradigm in the study of logic: the quest for a transcendental syntax, some kind of idealized language that emerges from the rules of logic. Amongst these rules, "testing" plays a leading role in defining a duality for the interpretation of negation.

The present work focuses on a notion of polarity which is a central technique used throughout Girard's work to express linear negation. We describe some properties and illustrate them with examples with the purpose of getting acquainted with the technique. We also highlight how the classical connectives (conjunction and disjunction) arise from an interpretation based on testing. In a sense, this work is intended to provide an alternative introduction to Girard's ideas and we hope it can have some pedagogical value.