Accéder directement au contenu Accéder directement à la navigation
Pré-publication, Document de travail

A gentle introduction to Girard's Transcendental Syntax for the linear logician

Abstract : Girard's Transcendental Syntax suggests a new framework for proof theory where logic (proofs, formulas, truth, ...) is no more primitive but computation is. Logic is grounded on a model of computation I call "stellar resolution" which is basically logic-free Robinson's first-order clausal resolution with a dynamics related to tiling models. This model naturally encodes the cut-elimination for proof-structures. By using realisability techniques for linear logic, it is possible to reconstruct formulas/types and logical correctness in order to obtain models of linear logic. Girard's philosophical justification of these works comes from Kantian inspirations: the Transcendental Syntax appears as a way to talk about the "conditions of possibility of logic", that is the conditions from which logical constructions emerge out of the meaningless (computation). We illustrate this foundational project with a reconstruction of Intuitionistic MELL(+MIX) and describe few other novelties such as the treatment of second order and Girard's logical constants "fu" and "wo".
Type de document :
Pré-publication, Document de travail
Liste complète des métadonnées
Contributeur : Boris Eng <>
Soumis le : mardi 4 mai 2021 - 18:16:46
Dernière modification le : mercredi 2 juin 2021 - 03:28:29


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-02977750, version 5
  • ARXIV : 2012.04752


Boris Eng. A gentle introduction to Girard's Transcendental Syntax for the linear logician. 2021. ⟨hal-02977750v5⟩



Consultations de la notice


Téléchargements de fichiers