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".
翻译:Girard的跨世代语法提出了一个新的证据理论框架,其中逻辑(证据、公式、真理,......)不再更原始,而是计算。逻辑基于一种我称之为“星理解析”的计算模型,它基本上是无逻辑的鲁滨逊的第一阶单词解析,其动态与平铺模型相关。这个模型自然地将证据结构的切除编码成编码。通过对线性逻辑使用可变技术,有可能重建公式/类型和逻辑正确性,以获得线性逻辑模型。Girard对这些作品的哲学解释来自Kantian的灵感:跨世纪语法是谈论“逻辑可能性的条件”的一种方式,这是无意义的(推断)逻辑构造产生出来的条件。我们用一个重建无意义的 MELL(+MIX) 来说明这个基础项目,并描述很少其他新事物,例如对第二顺序的处理和Girard逻辑常数“fu”和“wo”的逻辑常数。