A gentle introduction to Girard's Transcendental Syntax for the linear logician
Résumé
The Transcendental Syntax is about designing logics with a computational foundation. It suggests a new framework for proof theory where logic (proofs, formulas, truth, ...) is no more primitive but computation is. All the logical entities and activities will be presented as formatting on a given model of computation which should be as general, simple and natural as possible. The selected ground for logic in the Transcendental Syntax is a model of computation I call "stellar resolution" which is basically a reformulation logic-free Robinson's first order clausal resolution with a dynamics related to tiling models. An initial goal of the Transcendental Syntax is to retrieve linear logic from this new framework In particular, this model naturally encodes cut-elimination for proof-structures. By using ideas from realisability theory, it is possible to design formulas/types generalising the connectives of linear logic. Finally, generalising ideas from the theory of proof-nets, we able to express an idea unit testing: we can encode a computational object (typically the computational content of a proof) and some tests certifying its logical correctness (that it is indeed a valid proof of some formula).
Origine : Fichiers produits par l'(les) auteur(s)