A gentle introduction to Girard's Transcendental Syntax for the linear logician - Université Sorbonne Paris Nord Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2021

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

Boris Eng

Résumé

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".
Fichier principal
Vignette du fichier
main.pdf (301.59 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-02977750 , version 1 (25-10-2020)
hal-02977750 , version 2 (04-12-2020)
hal-02977750 , version 3 (25-01-2021)
hal-02977750 , version 4 (23-03-2021)
hal-02977750 , version 5 (04-05-2021)
hal-02977750 , version 6 (29-11-2021)
hal-02977750 , version 7 (03-04-2022)

Identifiants

Citer

Boris Eng. A gentle introduction to Girard's Transcendental Syntax for the linear logician. 2021. ⟨hal-02977750v5⟩
915 Consultations
930 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More